predicate logic proof about not free variable

Question

The question is

Prove that $\vdash (\forall x_i(A\to B)\to(\exists x_i A\to B)$ for any formulas A, B provided that the variable $x_i$ does not occur free in B.

Can someone help me sketch this proof?

Answer 1

We can prove it using Enderton's axiom system : see Herbert Enderton, A Mathematical Introduction to Logic (2nd - 2001)) [page 112] :

1. Tautologies(in the sense of propositional logic);
2. $∀ x α →α^x_ t $, where $t$ is substitutable for $x$ in $α$ ($α^x_ t$ is the formula derived from $\alpha$ by replacing $x$ by a term $t$);
3. $∀ x(α→β)→( ∀ x α→∀x β)$;
4. $α→∀x α$, where $x$ does not occur free in $α$.

modus ponens is the only rule of inference.

Proof

1) $\forall x (A \rightarrow B)$ --- assumed [a]

2) $A \rightarrow B$ --- from Ax.2 and 1), by modus ponens

3) $\lnot B \rightarrow \lnot A$ --- from 2) by tautological implication (with the tautology : $(p \rightarrow q) \leftrightarrow (\lnot q \rightarrow \lnot p)$)

4) $\lnot B$ --- assumed [b]

5) $\lnot A$ --- from 3) and 4) by mp

6) $\forall x \lnot A$ --- from 5) and GENERALIZATION THEOREM [page 117] ($x$ is not free in assumptions [a] nor in assumption [b], because $x \notin FV(B)$)

7) $\lnot \exists x A$ --- from 6) by abbreviation : $\exists$ stands for $\lnot \forall \lnot$, see page 68

8) $\lnot B \rightarrow \lnot \exists A$ --- from 4) and 7) by Deduction Theorem [see page 118], "discharging" assumption [b]

9) $\exists A \rightarrow B$ --- from 8) by tautological implication (see 3)

10) $\forall x (A \rightarrow B) \rightarrow (\exists A \rightarrow B)$ --- from 9) by Deduction Theorem.

---

The proof is a little bit shorter with Natural Deduction : with it we can avoid the two tautological implication steps, using $\exists$-elimination.