4 comments

[ 2.5 ms ] story [ 20.9 ms ] thread
Here is a summary for those who do not know much set theory.

Thanks to Gödel, we know that the Peano axioms for arithmetic cannot prove themselves to be consistent. The question is how much more do you have to add to that to prove that it is?

The answer turns out to be rather cute.

Consider the set of finite tuples of non-negative integers with a comparison that in Python looks like first comparing the length, and then comparing them in lexicographic order. That is, () < (0) < (1) < (2) < ... < (0, 0) < (0,1) < (0,2) < ... < (1, 0) < (1, 1) < (1, 2) < ... (0, 0, 0) < (0, 0, 1) < ... and so on. If this set is well-ordered, then PA is consistent. What well-ordered means is that a sequence of elements has to hit bottom in a finite number of steps. It may take a lot of steps, but it has to be finite.

Why would we expect that? Well bottom here is the empty tuple, (). There is only 1 so there is only one descending sequence and it hits bottom. (Well, duh.)

It is easy to write induction on a single variable to show that the tuples of length at most 1, that is () or (n), will hit bottom in a finite number of steps. In fact in no more than n+1 steps.

But what happens when we add tuples of length 2? Now it gets interesting. Consider the tuples of the form (n, m). Assuming that we've proven well-orderedness up to (n-1, _) we can do an induction proof to prove well-orderedness for (n, m). But then that is the induction step in a double induction proof of well-orderedness for (n, m).

Similarly well-orderedness for length 3 requires a triple induction.

And for length k requires a k-fold induction proof.

And so the full proof of well-orderedness cannot be written out in PA. Because it requires an infinite series of induction proofs. But they are all exactly of the same, very believable, form. And if you believe that k-fold induction is valid for every arbitrary k, then you can prove that any crazy arithmetic results that can be proven by the Peano Axioms will never create a contradiction.

I do so believe. :-)

Author here :-)

There's two layers to it, and you've described the first one. The argument you give about tuples of non-negative integers is what implies the consistency of PRA or Primitive Recursive Arithmetic (roughly: the finitary, computable part of arithmetic). This argument is done in a system that is the weakest that Gödel's theorem applies to, but you really have to start assuming a small amount of consistency somewhere. With consistency of PRA under your belt, you can then trust the proof that induction over the set of finite trees implies the consistency of Peano Arithmetic, which is done in PRA.

At that point you then need to make a second leap intuitive, non-formal argument for being able to do induction over the set of finite trees (there is a canonical ordering on these). So no only does one have to worry about height induction, but also induction over width at each level of the trees, so it's genuinely more complicated. Chow gives an argument (to which I link) in terms of Turing machines outputting descending sequences of trees as to why you should think this reasonable.

So it's all very interesting.

What is the canonical ordering on the set of trees?

Given how quickly the Goodstein sequence explodes, the "finite" in these cases may be very, very large...

"An order on the set of finite rooted trees is defined recursively: we first order the subtrees joined to the root in decreasing order, and then use lexicographic order on these ordered sequences of subtrees. In this way the set of all finite rooted trees becomes a well-ordered set which is order-isomorphic to ε0." (https://en.wikipedia.org/wiki/Epsilon_numbers_(mathematics)#...)

and yes, growth rates of fast-growing functions are an important facet of this analysis.

EDIT: you should think of a rooted tree as coding an ordinal written in Cantor normal form (https://en.wikipedia.org/wiki/Ordinal_arithmetic#Cantor_norm...) using only ordinals less than or equal to omega.

In fact, here's a nice thesis that sets it out: https://folk.uio.no/alfredb/Masteroppgave%20Alfred%20Bratter...