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

[Timothy Y. Chow]

Martin Davis wrote:

>Some of this on-going discussion has in effect 
>suggested that what Gentzen did amounts a proof 
>of con(PA) from PA +  epsilon-0 induction. 

I'm not sure where in the discussion you see that suggestion.  In case 
something I said gave this impression, let me clarify my narrative of the 
"ordinary mathematician."  The ordinary mathematician would normally 
regard the existence of the natural numbers as trivially establishing the 
consistency of PA, but has somehow been led to question this proof as 
"assuming [more than?] what it is trying to prove."  The mathematician may 
not be sure whether there is any actual circularity here, but figures that 
the matter can be settled by finding some other proof that *clearly* does 
not "assume what it is trying to prove."  But now things start to unravel; 
if assuming the existence of N as an infinite set is the cause of the 
discomfort, and the mathematician feels obliged to temporarily suspend 
that belief, then he is suddenly on unfamiliar territory.  He does not 
normally engage in any kind of reasoning where assuming the existence of N 
is taboo, and so now he is unsure what is O.K. and what isn't.

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.

Note that I'm being careful to avoid saying that the mathematician sees a 
definite circularity here, and I'm especially careful to avoid attributing 
any clear beliefs about provability in this or that formal system to the 
ordinary mathematician.  The ordinary mathematician doesn't know a lot 
about formal systems and probably can't even give a clear definition of 
what a "circular proof" is.  What he *can* see is that if he totally 
suspends his usual belief in N then he can't seem to get back to it, or 
even to the consistency of PA, without assuming something suspiciously 
similar in flavor to the assumption that he's temporarily denied himself.  
So the notion that the consistency of PA (or something stronger) simply 
must be *assumed* as an axiom gains some plausibility.

Tim