Sample proof that A implies A

Recollect that in our sample formal system we have the following postulates:

  • Axiom schema A1: \(A \to (B \to A)\)
  • Axiom schema A2: \((B \to (C \to D)) \to ((B \to C) \to (B \to D))\)
  • Rule of inference MP: \(A, A \to B \over B\)

Note that we’ll only use the postulates above, in particular note that we won’t use the axiom schema A3 for propositional calculus.

The proof schema goes as follows:

  1. \((A \to ((A \to A) \to A)) \to ((A \to (A \to A)) \to (A \to A))\) : by axiom schema A2 with \(B\) and \(D\) both being \(A\) while \(C\) is “\(A \to A\)”
  2. \(A \to ((A \to A) \to A)\) : by axiom schema A1 with \(A\) being \(A\) and \(B\) being “\(A \to A\)”
  3. \((A \to (A \to A)) \to (A \to A)\) : by MP using 2 and 1 as premises
  4. \(A \to (A \to A)\) : by axiom schema A1 with \(A\) and \(B\) being \(A\)
  5. \(A \to A\) : by MP using 4 and 3 as premises

So we say that we have shown that \(\vdash A \to A\), that is there is a deduction that \(A \to A\) without using any assumptions, only the postulates.

Note that above we have a proof schema where we can take any formula for A (similar to axiom schemas). Taking \(0 = 0\) as \(A\) we can use the proof schema above to prove \((0 = 0) \to (0 = 0)\). Taking \(\lnot(0 = 0)\) as \(A\) we can do the same for \(\lnot(0 = 0) \to \lnot(0 = 0)\).