[FOM] Re: Disaster?

[Timothy Y. Chow]

Martin Davis wrote (regarding the inconsistency of PA):
>There are now two threads going on FOM contemplating this possibility. No 
>one has mentioned that we possess proofs that PA is consistent.

Of course, that's true; I assume that the reason nobody mentioned it is
that everybody has been taking it for granted.  Every commonly used
axiomatic system can be proved consistent if you use sufficiently strong
axioms.  But one of the things implicitly under discussion is whether we
should necessarily believe something just because there's a proof of it.

Matthew Frank wrote:
>We usually use the induction axioms
>(phi(0) & (forall x)(phi(x)->phi(x+1)) -> (forall x)phi(x)
>only when phi is decidable or quantifier-free.  So if more complex
>induction axioms turned out inconsistent, we would abandon them, probably 
>with mutterings of impredicativity.

Good point.  Let me try to rephrase my concern.  What bothers me when
I imagine staring at a list of induction axioms that are mutually 
inconsistent is that I'm not sure how to answer the question, "Which
one of these is false of the standard integers?"  Or, "How exactly
should I try to modify my mental picture of the standard integers?"

Another way to put it is, if an explicit PA-proof of 0=1 were found, how
much of *infinitary* mathematics---by which I mean [informal] theorems
whose *statement* inherently involves infinitary objects---can still be
salvaged?  Moving to I_Delta_0(exp) might salvage most *finitary* theorems
of interest, but would it still salvage most *infinitary* mathematics?

For comparison, suppose ZF were found to be inconsistent.  Our concept of
the cumulative hierarchy, although pretty clear, seems to have enough
"wiggle room" that we can envisage perturbing it slightly (so as to avoid
the inconsistency) without destroying its essence.  But is that true of
the natural numbers?  If an explicit PA-proof of 0=1 were found, surely we
would not point to some (nonstandard) model of I_Delta_0(exp) and say,
"Oh yeah, *that's* what we've been thinking about all along, and it's 
obviously a more coherent concept than the standard integers, which we
have been forced to reject"?

Tim


P.S. In case it wasn't clear, I would be interested in a concrete answer 
to the following question: Are there any foundations for infinitary 
mathematics that might still be viable even in the presence of an explicit
PA-proof of 0=1?