Discord in the Axioms

You've all heard about Gödel's Second Incompleteness theorem, right?  If a theory with a finite list of axioms contains the basis for arithmetic, this theory cannot produce statements about its own consistency without contradicting itself.  So we can't ever prove such a theory's consistency; we can only take solace in the notion that we haven't found any contradictions yet.  Kind of a bummer.

Way back in September, the distinguished Ed Nelson, a math professor at Princeton, claimed to have found an inconsistency in Peano Axions--one of the most widely used formalizations of arithmetic--and distributed a sketch of his proof through a math mailing list.  It's hard to get more basic than this: these are axioms that establish the existence of zero, all the common rules for how the equals sign works, your ability to add one to a number that already exists, and (Nelson thought this last one was the culprit) the validity of proof-by-induction.  There might be some question about whether certain bits of modern set theory are inconsistent, but arithmetic?  Nelson was really going for the balls here.



Within a week, the sketch of the proof was shot down in the comments section of a blog post (over at the n-category cafe).  Some preliminary objections from the fields medalist Terence Tao (made earlier via Google+) were reposted in the comments, and soon both Tao and Nelson were locked in a debate.  Eventually, Tao's argument came through, and Nelson retracted his argument with considerable grace and humility.

Nelson's measured response seems to say a lot of nice things about the culture of modern math, and those things are analyzed very well over here.  The thing I want to harp on is what tripped Nelson up.   Tao's case against Nelson centered around the use of an argument by Kritchman and Raz in conjunction with Chaitin's Theorem.  And here is the deathblow:

The next step, as I understand your argument, is to try to run Chaitin’s argument to find an η for which 

(1) there is a bounded rank-and-level proof that K(η)≤ℓ; and 

(2) there is a bounded rank-and-level proof that K(η)>ℓ, 

thus contradicting (7) in your outline. Note that this η will likely be different from ξ. Now, how does Chaitin find this η? He builds a program to search for pairs (η,π) such that π is a proof that K(η)>ℓ, returning η when the first such pair is found. But here it becomes crucial to decide whether this program is going to use an unrestricted proof verifier (so that it accepts proofs of unbounded rank and level) or a restricted one (so that it only accepts proofs of rank at most ρ and level at most λ). If you use an unrestricted proof verifier, then one obtains (1), but does not obtain (2); instead, one only obtains 

(3) there is a proof (of unbounded rank and level) that K(η)>ℓ, 

and (1) and (3) do not lead to a contradiction unless one knows that the entire theory is consistent.

So then with Gödel's result, the theory $Q_0^*$ (some offspring of Peano they were working in) cannot be proven to be consistent, and Nelson's argument was shown to be dead in the water.  In a complete turnaround, the consistency of arithmetic found itself getting saved by that meanie of a Second Incompleteness Theorem.  Crazy, right?