[FOM] Are the proofs of con(PA) circular?

[Daniel Mehkeri]

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 
arbitrary sequences.

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 
coherent collection.

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.)

Daniel Mehkeri