Symbolic Logic, Dale Jacquette, Wadsworth, 2001, Chpt. 8, Ex. III, problem 12

Required: natural deduction proof for the following tautology. The number of steps could be cut down in my proof by simply instantiating the first assumption (line 2) by UI and applying DeMorgan's law straight away. Note that even though we have a free variable in our assumption on line 3, we are justified in applying UG on line 9 because we have discharged this assumption on line 6 (we are not applying UG within the scope of the innermost assumption).

1. ├ (x)(Fx ⊃Gx) ⊃(x) ¬ (Fx • ¬ Gx)
2. * (x)(Fx ⊃Gx) / ACP
3. * * Fx / ACP
4. * * Fx ⊃Gx / 2UI x/x
5. * * Gx / 3,4MP
6. * Fx ⊃Gx / 3-5CP
7. * ¬ Fx ∨Gx / 6MI
8. * ¬ (Fx • ¬ Gx) / 7DeM
9. * (x) ¬ (Fx • ¬ Gx) / 8UG
10. (x)(Fx ⊃Gx) ⊃(x) ¬ (Fx • ¬ Gx) / 2-9CP