Give a deduction of existential generalization: $\varphi_t^x\rightarrow (\exists x\varphi)$

I have to give a deduction of the existential generalization axiom without using the axiom itself. I'm given universal instantiation and the quantifier rules $(\psi\rightarrow \varphi, \psi\rightarrow (\forall x\varphi))$ and $(\varphi\rightarrow\psi,(\exists x\varphi)\rightarrow \psi)$ but that's about it. My first step I think should be to assume $\forall x\varphi$ which will allow me to use instantiation. After that I feel I should use the quantifier rules but can't find a valid application of the rules. A hint would be appreciated. Thanks.

Recall that (page 32 of the 2nd edition) the existential quantifier is not primitive; it is defined as an abbreviation for $\lnot ((\forall x) (\lnot \alpha))$.

Thus, from the first quantifier axiom:

$(\forall x) \lnot \varphi \to \lnot \varphi^x_t$

by propositional consequence :

$\lnot \lnot \varphi^x_t \to \lnot ((\forall x) \lnot \varphi)$

and by propositional consequence again and abbreviation:

$\varphi^x_t \to (\exists x) \varphi$.

• Thank you! So basically I just have to assume $\forall x\neg\varphi$ and $\neg\neg\varphi_t^x$. Commented Mar 16, 2017 at 16:09
• @JeffM. - No; this is not a correct instance of axiom : you must have only one $\lnot$. Commented Mar 16, 2017 at 16:22
• I'm getting there, but I'm still confused as to what assumptions I need to make. If I assume $\forall x\neg\varphi$, don't I need to assume $\neg\neg\varphi_t^x$ in order to get the propositional consequence on the second line? But at the same time if I assume both of these, then I also have $\neg((\forall)\neg\varphi)$ which means both the assumption and its negative are true, a contradiction... Commented Mar 16, 2017 at 16:27
• @JeffM.- not necessarily; see Denition 2.4.5 Rule of inference of type (PC) page 53. I'm using $(P \to Q) \vDash (\lnot Q \to \lnot P)$ for the 1st to 2nd line and $P \to \lnot \lnot P, \lnot \lnot P \to Q \vdash P \to Q$ for the 2nd to 3rd line. Commented Mar 16, 2017 at 16:52