Xrfgtjtk

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

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)\
quadquad |quad phi(a) to psi\
quadquad |quad vdots\
quadquad |quad forall xphi(x) to psi\
forall xvarphi(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)\
quadquad |quad phi(a) to psi\
quadquad |quad quad |quad forall xphi(x)\
quadquad |quad quad |quad phi(a)\
quadquad |quad quad |quad psi\
quadquad |quad forall xphi(x) to psi\
forall xvarphi(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 xvarphi(x) to psi\
quadquad |quad negexists x(phi(x) to psi)\
quadquad |quad vdots\
quadquad |quad bot\
negnegexists 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 xvarphi(x) to psi\
quadquad |quad negexists x(phi(x) to psi)\
quadquad |quad quad |quad phi(a) to psi\
quadquad |quad quad |quad exists x(phi(x) to psi)\
quadquad |quad quad |quad bot\
quadquad |quad neg(phi(a) to psi)\
quadquad |quad vdots\
quadquad |quad phi(a)\
quadquad |quad negpsi\
quadquad |quad forall xphi(x)\
quadquad |quad psi\
quadquad |quad bot\
negnegexists 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.

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

• Take the premise: $forall x~phi ~to~psi$
  


• Derive the contraposition: $lnotpsitolnotforall x~phi$
  


• Assuming $lnotpsi$, derive that there is some $x$ where $lnotphi$.


• Deduce then that, there is some $x$ where $lnotpsitolnotphi$, which is to say $phitopsi$
  


• Therefore $exists x~(phitopsi)$ is derived from the premise

• Take the premise: $exists x~(phitopsi)$
  


• Thence there is some witness $x$ where $phitopsi$ 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.