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

Question

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.

Answer 1

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$.