Take the 2-minute tour ×
Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.

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.

share|improve this question

1 Answer 1

up vote 2 down vote accepted

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.

share|improve this answer
    
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

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.