Proving $A \to \exists x B \Rightarrow \exists x (A\to B)$ if $x$ is not free in $A$

Question

Assume $A,B$ are first order formulas, with $x$ not free in $A$. I'd like to prove (in the two-sided sequent calculus for classical logic) that $$ A\to \exists x B \Rightarrow \exists x (A\to B) $$

By left introduction, it would suffice to find some $C$ such that the sequents

$$A\to \exists x B\Rightarrow C$$ and $$ A\to \exists x B,C\Rightarrow\exists x (A\to B)$$ are both derivable.

Any suggestions?

Answer 1

Here's a derivation (I hope you'll excuse my switching to $\vdash$, which is how I learned ;)

---

Hope this helps ^_^

Answer 2

This appears to be a nonconstructive statement. Specifically, $A \to \exists x .Bx$ is saying that, given all of the constructions of $A$, you are able to convert those into the construction of $x$. On the other hand $\exists x.A \to Bx$ is saying that you are able to construct an $x$ out of nothing. This is stronger than the first claim (at least in this case).

So you need to assume that $x$ can always be constructed, that is, that $\exists x.Bx \lor \lnot \exists x.Bx$, so try instead to prove both

$$\begin{array} {rccl} \exists x . Bx,& A \to \exists x . Bx &\vdash& \exists x . A \to Bx \\ \lnot \exists x . Bx,& A \to \exists x . Bx &\vdash& \exists x . A \to Bx \end{array}$$

then stitch those together.