The three axiom schemas below, together with the one rule of inference, constitute a complete set of axioms for sentential logic. The Greek letters stand for any sentence in the system.

Ax 1    ( ( ))

Ax 2    ((( (   )) (( ) (   )))

Ax 3    ((~   ~ ) ((~ ) )))

Rule of Inference (Modus Ponens): , ( )

---

(To make life a little easier I will omit outside parentheses below.)

T1. P P

1. P ((P P) P)                                                                                 Ax1
2. ((P ((P P)  P )) ((P  (P P)) (P  P ))                        Ax2
3. (P  (P P)) (P  P )                                                                   1, 2 MP
4. P (P P)                                                                                          Ax1
5. P  P                                                                                                  3, 4 MP

---

I. Proof that          (~P P) P

    1.    (~P ~P) ((~P P) P))                                                               Ax 3
    2.    ~P ~P                                                                                              Thm 1
    3.    (~P P) P                                                                                        1,2 MP

II. Proof that        {(P Q), (Q R)}  (P R)

    1.    (Q R) (P (Q R))                                                                   Ax 1
    2.     Q R                                                                                               Assumption
    3.     P (Q R)                                                                                      1,2 MP
    4.     ((P (Q R)) ((P Q) (P R))                                               Ax 2
    5.     (P Q) (P R)                                                                              3,4 MP
    6.     P Q                                                                                                Assumption
    7.     P R)                                                                                               5,6 MP

---

III. Proof that         {P, ~P}  Q   (i.e., that anything follows from a contradiction; sometimes called the principle of explosion))

    1.    (P (~Q P))                                                                                Ax 1
    2.    P                                                                                                     Assumption
    3.    (~Q P)                                                                                         1,2 MP
    4.    ~P (~Q ~P)                                                                              Ax 1
    5.    ~P                                                                                                   Assumption
    6.    ~Q ~P)                                                                                        4,5 MP
    7.    (~Q ~P) ((~Q P) Q))                                                         Ax 3
    8.    (~Q P) Q                                                                                   6, 7 MP
    9.    Q                                                                                                      3,8 MP

IV.  Proof that      ~ ~P P

    1.    (~P ~ ~P) [(~P ~P) P]                                                        Ax 3
    2.     ((~P ~ ~P) [(~P ~P) P])
    ([(~P ~ ~P) (~P ~P)] [(~P ~ ~P) P])                                   Ax 2
    3.    [(~P ~ ~P) (~P ~P)] [(~P ~ ~P) P]                              1,2 MP
    4.     (~P ~P) [(~P ~ ~P) (~P ~P)]                                          Ax 1
    5.    ~P ~P                                                                                            Thm 1
    6.    (~P ~ ~P) (~P ~P)                                                                   4, 5 MP
    7.    (~P ~ ~P) P                                                                                 3,6 MP
    8.    ~ ~P (~P ~ ~P)                                                                            Ax 1
    9.    ~ ~P P                                                                                             8,7 II (above)

Corollary of IV.    ~~P  P        (Double Negation, Part 1)

    Proof: Given ~~P, use that with  ~~P P and MP to infer P.

---

V.  Proof that        P Q, ~Q  ~P       (Modus Tollens)

    1.     ~ ~P P                                                                                        Thm (IV, above)
    2.    P Q                                                                                              Assumption
    3.    ~ ~P Q                                                                                         1,2 II (above)
    4.    (~ ~P ~Q) [(~ ~P Q) ~P]                                                   Ax 3
    5.    ~Q (~ ~P ~Q)                                                                           Ax 1
    6.    ~Q                                                                                                   Assumption
    7.    (~ ~P ~Q)                                                                                     5,6 MP
    8.    (~ ~P Q) ~P                                                                              4,7 MP
    9.    ~P                                                                                                    3,7 MP

VI.  Proof that        P  ~ ~P        (Double Negation, Part 2)

    1.     (~~~P ~P) [(~~~P P) ~~P]                                                 Ax 3
    2.    ~~~P ~P                                                                                         Thm IV (above)
    3.     (~~~P P) ~~P                                                                             1, 2 MP
    4.     P                                                                                                        Assumption
    5.     P (~~~P P)                                                                                  Ax 1
    6.     ~~~P P                                                                                           4, 5 MP
    7.     ~~P                                                                                                    3,6 MP

---

Thus the rules of MP, DN and MT all hold. If we had the resources for conditional proof we would have all the machinery for a natural deduction system. What we require is the following result.

(Weak) Deduction Theorem (Herbrand, 1930):   If     , then   ( ).
(It is not hard to show this by induction on the number of steps in the derivation of from .
See Mendelson, p. 32.)