In 1931, the mathematician Kurt Godel showed that any axiomatic system in natural number theory that is “complete” (can prove every postulate that is true) will not be “consistent” (it will prove a postulate that is false).  While having an impact in theoretical mathematics and computer science, it also has interesting implications on epistomology (the branch of philosophy that studies the nature of knowledge).  Godel’s proof may set limits on human knowledge: We cannot prove (or “know”) everything that is true with our current axiomatic techniques.

Because of the importance of Godel’s proof, in 1958 Ernest Nagel and James Newman published Godel’s Proof, a book that attempts to outline the steps of the proof and its conclusions in plain English.  While not exactly an easy read, it is a great book that has been in continuous print and had a revised edition published in 2001.

In chapter V, starting on page 45, they present an outline of a proof that an axiomatic system called “predicate logic” is consistent.  After presenting four axioms and two transformation rules, they state: “It happens that ‘p -> (~p -> q)’ is a theorem in this calculus (We shall accept this as a fact, without exhibiting the derivation.)”  They then use this statement in a proof that occupies the following 6 pages in the chapter and 5 pages on the Appendix.  Because this statement is pivotal to the discussion, I really wanted to prove it to myself.  As it turns out, it wasn’t trivial (and there was an important fact missing from the book’s text).  The following is the proof:

Definitions:

The following are “functions”: the letters ‘p’, ‘q’, ‘r’, and so on; and if the strings “S” and “T” are functions, then so are “~(S)”, “(S U T)”, and “(S -> T)”.

It is important to note that for the purposes of the proof, “functions”, “axioms”, and “theorems” can be considered pure strings with no underlying meaning, except that extra parentheses can be removed.  This leads to a great quote: “This is the point of Russell’s epigram: pure mathematics is the subject
in which we do not know what we are talking about, or whether what we are
saying is true.”

The following strings are “axioms” (the “axioms” are also “theorems”):
Axiom 1: (p U p) -> p
Axiom 2: p -> (p U q)
Axiom 3: (p U q) -> (q U p)
Axiom 4: (p -> q) -> ((r U p) -> (r U q))

We also have two “transformation rules” for making new “theorems”.
Substitution: You can form a new “theorem” by taking a known “theorem” and consistently substituting its variables with other functions.  For example, Axiom 2 can become a new theorem (~a -> (~a U (b -> c))) by substituting “p” with “~a” and “q” with “(b -> c)”.
Modus Ponens: If “A” is a “theorem” and “(A -> B)” is a “theorem”, then “B” is a “theorem”.

As it turns out, in order to prove “p -> (~p -> q)”, you need one more rule that isn’t stated in the book:
Definition of “->”: “(A -> B)” is identical to “(~A U B)”.  So you can do string replacement in either direction.
This definition can be shown to preserve the property of “Tautology” since they have identical truth matrices (please see the appendix).

It takes five steps (that I’ll call “Theorems” with a capital “T”) to show that “p -> (~p -> q)”:

Theorem 1: if “A->B” is a “theorem”, and “B->C” is a “theorem”, then “A->C” is a “theorem“
1. A->B     given
2. B->C     given
3. (B->C) -> ((~A U B) -> (~A U C))     Axiom 4, Substitution
4. ((~A U B) -> (~A U C))     2, 3, Modus Ponens
5. ((A->B) -> (A->C))     4. definition of “->“
6. (A->C)     1, 5, Modus Ponens

Theorem 2: (p -> ~q) -> (q -> ~p)
1. (~p U ~q) -> (~q U ~p)     Axiom 3, Substitution
2. (p -> ~q) -> (q -> ~p)     1, definition of “->”

Theorem 3: p -> p
1. p -> (p U p)   Axiom 2, Substitution
2. (p U p) -> p    Axiom 1
3. p->p    1, 2, Theorem 1

Theorem 4: p -> ~(~p)
1. (~p -> ~p) -> (p -> ~(~p))    Theorem 2, Substitution
2. (~p -> ~p)    Theorem 3, Substitution
3. p -> ~(~p)   1, 2, Modus Ponens

Theorem 5: p -> (~p -> q)
1. ~(~p) -> (~(~p) U q)    Axiom 2
2. p -> (~(~p) U q)    Theorem 4, 1, Theorem 1
3. p -> (~p -> q)    2, Definition of “->”

Whew.  Finally I can move on to the next chapter…