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
    Quick question...the Deduction Theorem only lets you assume $\phi \to \psi$ and $\phi$ if they are sentences.2011-11-04
  • 0
    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.2011-11-04
  • 0
    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.2011-11-05
  • 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