Natural deduction: predicate logic proof (Prenex form)

Question

I'm pretty familiar with proofs in propositional logic, but not so much with predicate logic.

I'm trying to prove the following (which can be used during construction of prenex normal form).

If $x$ is not free in $\psi$, then: $\forall x\phi\rightarrow \psi $ if and only if $\exists x(\phi \rightarrow \psi)$

I personally use tree proofs, but any notation is fine. I don't really know how to start this one to be honest.

Answer 1

Here's a proof sketch for the "if" direction, where the proof more or less writes itself. Obviously you have to use $\exists$-Elim, since you have an $\exists$ premiss which you need to make use of. So you already know the proof has to look like this (Fitch style --re-arrange for a tree!)

$\exists x(\phi(x) \to \psi)\\ \quad\quad |\quad \phi(a) \to \psi\\ \quad\quad |\quad \vdots\\ \quad\quad |\quad \forall x\phi(x) \to \psi\\ \forall x\varphi(x) \to \psi$

Then how to fill in the dots is pretty obvious since you'll have to use Conditional Proof -- i.e. assume the antecedent of the conditional you want to prove and aim for the consequent. Easy!

$\exists x(\phi(x) \to \psi)\\ \quad\quad |\quad \phi(a) \to \psi\\ \quad\quad |\quad \quad |\quad \forall x\phi(x)\\ \quad\quad |\quad \quad |\quad \phi(a)\\ \quad\quad |\quad \quad |\quad \psi\\ \quad\quad |\quad \forall x\phi(x) \to \psi\\ \forall x\varphi(x) \to \psi$

The other direction is trickier. But try using reductio (always a good plan if nothing else looks an obvious move) so the overall shape of the proof will look like this:

$\forall x\varphi(x) \to \psi\\ \quad\quad |\quad \neg\exists x(\phi(x) \to \psi)\\ \quad\quad |\quad \vdots\\ \quad\quad |\quad \bot\\ \neg\neg\exists x(\phi(x) \to \psi)\\ \exists x(\phi(x) \to \psi)$

You can complete the proof like this (think through why this is now an obvious way, and what justifies each step).

$\forall x\varphi(x) \to \psi\\ \quad\quad |\quad \neg\exists x(\phi(x) \to \psi)\\ \quad\quad |\quad \quad |\quad \phi(a) \to \psi\\ \quad\quad |\quad \quad |\quad \exists x(\phi(x) \to \psi)\\ \quad\quad |\quad \quad |\quad \bot\\ \quad\quad |\quad \neg(\phi(a) \to \psi)\\ \quad\quad |\quad \vdots\\ \quad\quad |\quad \phi(a)\\ \quad\quad |\quad \neg\psi\\ \quad\quad |\quad \forall x\phi(x)\\ \quad\quad |\quad \psi\\ \quad\quad |\quad \bot\\ \neg\neg\exists x(\phi(x) \to \psi)\\ \exists x(\phi(x) \to \psi)$

Fill in the dots by propositional calculus reasoning. $\forall$ intro is justified from $\phi(a)$ since $a$ appears in no undischarged assumption on which $\phi(a)$ depends.

Answer 2

Here's an informal deduction.   Express it in your own formal system.

• Take the premise: $\forall x~\phi ~\to~\psi$
• Derive the contraposition: $\lnot\psi\to\lnot\forall x~\phi$
• Assuming $\lnot\psi$, derive that there is some $x$ where $\lnot\phi$.
• Deduce then that, there is some $x$ where $\lnot\psi\to\lnot\phi$, which is to say $\phi\to\psi$
• Therefore $\exists x~(\phi\to\psi)$ is derived from the premise

---

• Take the premise: $\exists x~(\phi\to\psi)$
• Thence there is some witness $x$ where $\phi\to\psi$ holds
• Assuming $\forall x~\phi$, derive that for the witness, $\phi$ holds, and apply modus ponens.
• Thus deduce that $\forall x~\phi ~\to~\psi$ is derivable from the premise.