[FOM] Are the proofs of con(PA) circular?
Timothy Y. Chow
tchow at alum.mit.edu
Wed May 18 23:21:19 EDT 2011
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
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.
More information about the FOM