Show the validity of ¬∀x(F x → Gx) ⊢ ∃xFx using natural deduction

Question

I'm very much stuck on this annoying proof, any help would be much appreciated.

I'm assuming I'm using negation elimination on to get the conclusion, and Existential Elimination once I have transformed the premise into ∃x¬(Fx→Gx) - but can't for the life of me figure out how.

Cheers

Answer 1

$\def\fitch#1#2{\quad\begin{array}{|l}#1\\\hline#2\end{array}}$

I'm assuming I'm using negation elimination on to get the conclusion, and Existential Elimination once I have transformed the premise into ∃x¬(Fx→Gx)

  Yes, and no.  A reduction to absurdity proof is the way to go.  But what existence would you eliminate?

  Okay!  To begin that proof, you would take the premise and make the assumption you wish to negate.  Depending on your particular proof system, that should look something like this:

$$\fitch{\lnot\forall x~(Fx\to Gx)}{\fitch{\lnot\exists x~Fx}{~\vdots\\\bot}\\\lnot\lnot\exists x~Fx\\\exists x~Fx}$$

  Thus: you begin with two statements with which you hope to derive a contradiction.  So, you would need to derive either $\exists x~Fx$, or $\forall x~(Fx\to Gx)$.  Obviously, that indicates that existential introduction or universal introduction could be useful.  But which?

  Right now, you have nothing extant with which to introduce an existence.  So mayhap you should take an arbitrary term to see if you might derive the conditional statement?

$$\fitch{\lnot\forall x~(Fx\to Gx)}{\fitch{\lnot\exists x~Fx}{\fitch{\boxed a}{\fitch{Fa}{~\vdots\\Ga}\\ Fa\to Ga}\\\forall x~(Fx\to Gx)\\\bot}\\\lnot\lnot\exists x~Fx\\\exists x~Fx}$$   That looks promising.  However, how would you derive the consequent for that conditional?

  You should be able to complete the proof with no further assistance.