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

-

## 1 Answer

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

All the real work is then in the proof rewriting implied by the use of the deduction theorem. At least there is no need to be clever in this phase; just carry out the algorithm.

-
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
Hmm, I'm almost sure the version I'm familiar with instead restricts the use of generalization in the inner proof sequence, based on the free variables of the assumption. Will check my reference books later and then be back. – Henning Makholm Nov 4 '11 at 20:40
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