I have to provide a natural deduction derivation for:
¬∀xFx ⊢ ∃x¬Fx
That´s what I got so far:
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)?