2
$\begingroup$

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 Answers 1

2

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.

  • 0
    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).2011-11-05