[FOM] Are the proofs of con(PA) circular?
dmehkeri at gmail.com
Thu May 19 22:34:18 EDT 2011
Timothy Chow writes:
> If we offer up Gentzen's proof, we have to explain what epsilon-0
> induction is. This is even less familiar. Is it going to give the
> mathematician warm fuzzies? Probably not. The validity of epsilon-0
> induction is not likely to seem more "self-evident" than the existence
> of N.
Well, here's why I think it could do just that.
The point that statements like "Gentzen proved induction over omega
using induction over epsilon_0" ignore is that we don't need full
epsilon-0 induction, just a restricted form of it. In fact it can be
stated without induction, or talk of well-foundedness, ordinals, or
Specifically, to prove the 1-consistency of PA, it is sufficient to
believe that, for some structure of order type epsilon-0 (and see what
Vaughan Pratt has written about these), every elementary recursive
descending sequence terminates.
I say that's a hugely important distinction. Consider:
(1) If a certain collection contains 0, and for each n it contains, it
also contains n+1, then that collection contains all the natural numbers.
Even though this is usually called the "second-order" induction axiom,
it actually doesn't imply the first-order induction axiom scheme of PA
or HA. You also need something like:
(2) every predicate of first-order arithmetic actually defines a
If what you are in doubt of is (2), then Gentzen's proof could be
immensely valuable. In fact it can be proved without even propositional
logic. (Wikipedia's article on PRA discusses Goodstein's logic-free
system. Add to this system function definition by descent recursion.)
More information about the FOM