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).
- ├ (x)(Fx ⊃Gx) ⊃(x) ¬ (Fx • ¬ Gx)
- * (x)(Fx ⊃Gx) / ACP
- * * Fx / ACP
- * * Fx ⊃Gx / 2UI x/x
- * * Gx / 3,4MP
- * Fx ⊃Gx / 3-5CP
- * ¬ Fx ∨Gx / 6MI
- * ¬ (Fx • ¬ Gx) / 7DeM
- * (x) ¬ (Fx • ¬ Gx) / 8UG
- (x)(Fx ⊃Gx) ⊃(x) ¬ (Fx • ¬ Gx) / 2-9CP
No comments:
Post a Comment