# Derive Alonzo Church's axioms from Tarski-Bernay-Wajsberg axioms

In Ex.12.7 of Introduction to mathematical logic by Alonzo Church, Readers are asked to prove the following in order as theorems of the Tarski-Bernay-Wajsberg axiom system :

$1. (p \rightarrow (p \rightarrow q)) \rightarrow (p \rightarrow q)$

$2. (p \rightarrow ((p \rightarrow q) \rightarrow q))$

$3. (p \rightarrow (q \rightarrow r)) \rightarrow (q \rightarrow (p \rightarrow r))$

$4. (q \rightarrow r) \rightarrow ((p \rightarrow q) \rightarrow (p \rightarrow r))$

$5. (s \rightarrow (p \rightarrow q)) \rightarrow ((s \rightarrow p) \rightarrow (s \rightarrow q))$

$6. ((p \rightarrow f) \rightarrow f) \rightarrow p$

The exercise calms that except the 6th proposition $((p \rightarrow f) \rightarrow f) \rightarrow p$ , the remaining can be proved without using the axiom $f → p$. The Deduction Theorem cannot be applied to derive all the propositions above.

Alonzo shown how to derive Tarski-Bernay-Wajsberg axioms from his own axiom system, $P_1$, in the book. Since the propositions $(p \rightarrow (q \rightarrow p))$ is the axiom of both Alonzo Church’s axiom system and Tarski-Bernay-Wajsberg axiom system, both of them are therefore equivalent if the 5th proposition $(s \rightarrow (p \rightarrow q)) \rightarrow ((s \rightarrow p) \rightarrow (s \rightarrow q))$ and the 6th proposition $((p \rightarrow f) \rightarrow f) \rightarrow p$ above are proved, which are the axioms of Alonzo Church’s axiom system.

Unlike Ex.12.4 to Ex.12.6 , no hints (or answers) are given in Ex.12.7 , can you show me how to prove the 6 propositions of the above?