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