# Formal “Hilbert-Style” Proof of a relatively simple statement

I'm trying to prove that

$(\phi \to \psi) \to (\phi \to \exists v \psi)$

using a deduction from the formal Hilbert system, but I don't know how to proceed. Any help would be appreciated! Thanks.

-

Use the deduction theorem twice, once to assume $\phi\to\psi$ and then again to assume $\phi$. Modus ponens on these assumptions gives you $\psi$, and you probably have a pre-made sequence to deduce $\exists v.\psi$ from $\psi$ (the details of which differ according to your exact rules of inference).
Quick question...the Deduction Theorem only lets you assume $\phi \to \psi$ and $\phi$ if they are sentences. – Isaac Solomon Nov 4 '11 at 20:29
My main reference (Mendelson, Introduction to Mathematical Logic) states the deduction theorem as: "Assume that, in some deduction showing that $\Gamma, \mathscr B\vdash \mathscr C$, no application of Gen to a wf that depends upon $\mathscr B$ has as its quantified variable a free variable of $\mathscr B$. Then $\Gamma\vdash \mathscr B\Rightarrow \mathscr C$." And $\psi\vdash\exists v.\psi$ can be proved without Gen at all. – Henning Makholm Nov 5 '11 at 4:20
However if your deduction theorem is weaker, we can do without it, depending on your logical axioms for $\exists$. In Mendelson's system, $(\forall x.\mathscr B(x))\Rightarrow \mathscr B(t)$ is an axiom; with $\mathscr B(t)\equiv\neg\psi(t)$ and $t\equiv x\equiv v$ we get $(\neg\exists v.\psi(v))\Rightarrow \neg\psi(v)$. Then just combine this with the propositional tautology $$\vdash ((\neg\exists v.\psi)\to\neg\psi)\to((\phi\to\psi)\to(\phi\to\exists v.\psi))$$ (which can be proved treating $\exists v.\psi$ as a black box). – Henning Makholm Nov 5 '11 at 4:30