2

I have to provide a natural deduction derivation for:

¬∀xFx ⊢ ∃x¬Fx

That´s what I got so far:

1.¬∀xFx

2.‖ ¬∃x¬Fx (Indirect proof hypothesis)

3.‖‖ ¬¬Fy (Indirect proof hypothesis 2)

4.‖‖ Fy (from 3)

5.‖‖ ∀xFx (from 4)

Am I correct in assuming that I cannot derive ∀xFx (line 5) from Fy (line 4) because the indirect proof in line 3 is not finished (and y is not bound in line 3)?

  • Correct; you cannot "generalize" in 5 because y is free in the assumption 3. (still open at step 5). – Mauro ALLEGRANZA Jun 16 '17 at 11:02
4

1) ¬∀xFx --- premise

2) ¬∃x¬Fx --- assumed [a]

3) ¬Fy --- assumed [b]

4) ∃x¬Fx --- from 3)

5) --- contradiction: from 2) and 3)

6) Fy --- from 3) and 5) by Double Negation, discharging [b]

7) ∀xFx --- from 7): no y free in "open" assumptions (i.e. [a])

8) --- contradiction: from 1) and 7)

9) ∃x¬Fx --- from 2) and 8) by Double Negation, discharging [a]

  • Thank you very much! After I had realised that my original idea didn´t work, I couldn´t see that the solution is so simple! Last question: Is it necessary to end the assumptions with a double negation (make an seperate line with double negation and then eliminate it)? Or can I simply write Fy in line 6 like you did? – LittleD Jun 16 '17 at 11:28
  • @LittleD - it depends on the way the rules are written. – Mauro ALLEGRANZA Jun 16 '17 at 11:30
  • Ok, that´s what I suspected, just wanted to ask to be sure. – LittleD Jun 16 '17 at 11:33

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.