# Hilbert Calculus, Formal Proof Converse

I'm trying to find a proof of $\exists x\phi\rightarrow\exists y\phi^x_y$ in the Hilbert-calculus while working through a completeness proof for FOL on my own. Can anyone provide a proof of this theorem or hints for its construction? Important info: at most $x$ is free in $\phi$.

The book I'm using (Introduction to Mathematical Logic by Walicki) claims that the theorem has been proved in the exercises for an earlier chapter, but these exercises (which I've completed) only prove the converse. Consequently, there is still a gap in my understanding, and I'm turning here for help only after repeated failure to find a proof for the theorem in question.

The axioms of the system are:
A1: $\phi\rightarrow(\psi\rightarrow\phi)$
A2: $\phi\rightarrow(\psi\rightarrow\xi)\rightarrow((\phi\rightarrow\psi)\rightarrow(\phi\rightarrow\xi)$
A3: $(\neg\psi\rightarrow\neg\phi)\rightarrow(\phi\rightarrow\psi)$
A4: $\phi^x_t\rightarrow\exists\phi$

The rules of inference are Modus Ponens and $\exists I:\frac{\phi\rightarrow\psi}{\exists x\phi\rightarrow\psi}$, where $x\notin\mathcal{V}(\psi)$.

$\exists x.\phi \to \exists y.\phi^x_y$ is only true if $y$ is not free in $\phi$. Otherwise we would have, for example $\exists x.(x=y+1)\to\exists y.(y=y+1)$ which is definitely false in $\mathbb N$.
In this case, if you set $\psi=\phi^x_y$, then $\exists x.\phi\to\exists y.\phi^x_y$ is the same as $\exists x.\psi^y_x\to\exists y.\psi$, which is what you say you have already proved.
• Great! Yes, I forgot to add the condition on $y$. I never thought to return to using the substitution rules, but I see how it works now. So simple...Many thanks. – Poster234523 Jun 4 '15 at 12:16