Implicational propositional calculus

In mathematical logic, the implicational propositional calculus is a version of classical (two-valued) propositional calculus which uses only one connective, called implication or conditional. In formulas, this binary operation is indicated by "implies", "if ..., then ...", "→", " $\rightarrow$ , etc..

Axioms

Axiom schema 1 is P→(Q→P).
Axiom schema 2 is (P→(Q→R))→((P→Q)→(P→R)).
Axiom schema 3 (Peirce's law) is ((P→Q)→P)→P.
The one rule of inference (modus ponens) is: from P and P→Q infer Q.

Where in each case, P, Q, R may be replaced by any proposition which contains only "→" as a connective.

Deduction meta-theorem

The first task is to derive the deduction meta-theorem using axioms 1, 2, and modus ponens. One proves a lemma schema:

(A→((B→A)→A))→((A→(B→A))→(A→A)) 1. axiom 2

- P→Z 1. hypothesis
  - (P→Q)→Z 2. hypothesis
    - Z→Q 3. hypothesis
      - P 4. hypothesis
      - Z 5. modus ponens using steps 4 and 1
      - Q 6. modus ponens using steps 5 and 3
    - P→Q 7. deduction from 4 to 6
    - Z 8. modus ponens using steps 7 and 2
  - (Z→Q)→Z 9. deduction from 3 to 8
  - ((Z→Q)→Z)→Z 10. Peirce's law
  - Z 11. modus ponens using steps 9 and 10
- ((P→Q)→Z)→Z 12. deduction from 2 to 11
(P→Z)→((P→Q)→Z)→Z) 13. deduction from 1 to 12 QED