Two questions in the predicate calculus system

Question

I am reading A.G.Hamilton's Logic for MathematiciansI am stuck at proposition 4.25 :Let A and B be wfs. of L

(i)If $x_i$ does not occur free in A ，then $$\vdash ((\forall x_i)(A \to B)\leftrightarrow (A\to (\forall x_i)B))$$ and $$\vdash ((\exists x_i)(A \to B)\leftrightarrow (A \to (\exists x_i)B))$$

(ii) if $x_i$ does not occur free in B, then $$\vdash ((\forall x_i)(A\to B)\leftrightarrow ((\exists x_i)A \to B))$$ and $$\vdash ((\exists x_i)(A \to B) \leftrightarrow ((\forall x_i)A \to B))$$

I am confused with the second and the fourth.

The system's axioms are as follows:

(K1) $(A \to (B \to A))$

(K2)$(A \to (B\to C))\to ((A\to B)\to (A \to C))$

(K3)$(\neg A \to \neg B)\to (B\to A)$

(K4)$((\forall x_i) A\to A)$,if $x_i$ does not occur free in A

(K5)$((\forall x_i)A(x_i) \to A(t))$,if $A(x_i)$is a wf. of L and t is a term in L which is free for $x_i$ in $A(x_i)$

(K6) $(\forall x_i)(A\to B)\to (A\to (\forall x_i)B)$,if A contains no free occurrence of the variable $x_i$ Additionally, we have MP(Modus ponens) and Generalisation.

Perhaps this result can be helpful(casue the author mentioned it):$$\vdash ((\forall x_i)(A \to B)\to ((\exists x_i) A \to (\exists x_i)B))$$

I would appreciate it very much if you could help me.:)

Answer 1

Regarding the second formula of (ii):

(1) $\exists x(\alpha \rightarrow \beta)$ --- premise

(2) $\lnot \exists x \beta \to \exists x(\alpha \rightarrow \beta)$ --- from Axiom (K1) and (1) by MP

(3) $\alpha$ --- assumed

(4) $\lnot \exists x \beta$ --- assumed

(5) $\lnot \lnot \forall x \lnot \beta$ --- abbreviation for $\exists$

(6) $\forall x \lnot \beta$ --- by Double Negation (page 36)

(7) $\lnot \beta$ --- from (6) and Axiom (K4) by MP

(8) $\lnot (\alpha \rightarrow \beta)$ --- from (3) and (7), using the tautology $\alpha \rightarrow (\lnot \beta \rightarrow \lnot (\alpha \rightarrow \beta))$ and MP

(9) $\forall x \lnot (\alpha \rightarrow \beta)$ --- by Gen Th ($x \notin FV(\alpha)$)

(10) $\lnot \exists x (\alpha \rightarrow \beta)$ --- abbreviation

(11) $\lnot \exists x \beta \to \lnot \exists x (\alpha \rightarrow \beta)$ --- from (4) and (10) by DT

(12) $\lnot \lnot \exists x \beta$ --- using (2) and (11) and tautology page 39

(13) $\exists x \beta$ --- by Double Negation (page 36)

(14) $\alpha \rightarrow \exists x \beta$ --- from (2) by Deduction Theorem.

In conclusion we have:

$\exists x (\alpha \rightarrow \beta) \vdash (\alpha \rightarrow \exists x \beta)$.

---

(1) $\alpha \rightarrow \exists x \beta$ --- assumed

(2) $\forall x \lnot (\alpha \rightarrow \beta)$ --- assumed

(3) $\alpha \land \lnot \beta$ --- from (2) and Axiom (K4) and using tautological equivalence

(4) $\lnot \beta$ --- from (3)

(5) $\forall x \lnot \beta$ --- by the Generalization Theorem, because $x$ is not free in assumptions (1) and (2)

(6) $\lnot \exists x \beta$ --- abbreviation

(7) $\alpha$ --- from (3)

(8) $\exists x \beta$ --- from (1) by MP.

Having derived the contradiction [with (6) and (8)], we apply again the schema above (page 39) for managing contradiction to get :

(9) $\lnot \forall x \lnot (\alpha \rightarrow \beta)$, that is : $\exists x (\alpha \rightarrow \beta)$.

In conclusion we have :

$(\alpha \rightarrow \exists x \beta) \vdash \exists x (\alpha \rightarrow \beta)$.

---

---

The other formula must be treated similarly.