# Quick logic deduction question

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

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