[FOM] Re: Disaster?

[Timothy Y. Chow]

>inconsistency of PA or ZF would not be a full disaster for mathematics
[...]
>(v) all "normal" mathematicians would someway (may be very strongly)
>change their style of work when new foundations will be suggested
>(like it was in the previous century when set theory became the
>current foundation);

I also don't think that the inconsistency of PA would be a "disaster";
rather, it would be an extraordinary achievement.  While I'm confident
PA is consistent, it's interesting to conduct a thought experiment,
imagining the sociological effect such a proof of inconsistency would 
have.

The first step in the thought experiment is to consider whether the proof
of a contradiction would be of a feasible length.  If the PA-proof of a
contradiction were not explicit and concrete but were infeasibly large,
then it could be more easily ignored.  The more interesting case is
thus the case in which it would be explicit.

It's pretty much beyond my powers of imagination to conceive of, say,
someone explicitly exhibiting two integers in ordinary decimal notation
whose product is still feasibly small, but which reliably comes out having
different values depending on the algorithm used to compute them.  So I
don't think the PA-proof of 0=1 would be of a form that could be converted
to such a pair of explicit integers; indeed, the fact that the consistency
of PA has no finitistic proof more or less says that there's no finitistic
method of converting an arbitrary PA-proof of 0=1 into such a thing.

On the other hand, we *could* in principle systematically convert any
explicit PA-proof of 0=1 into a human-readable proof of 0=1 (or, for
fun, some other number-theoretic statement such as "There are finitely
many primes") that uses only universally accepted, mathematically rigorous 
arguments.  Again there might be a feasibility problem; a few terabytes
might be a "feasible-sized" proof for a machine, but it might not be
feasible to convert it into something *truly* "human-readable."  Let's
suppose again, though, that the proof is sufficiently small.

In that case, I strongly suspect that the contradiction would *not* be
shrugged off by most mathematicians.  There would be only finitely many
instances of the first-order induction axiom used, and the arguments
would use standard principles of classical logic, leading to any desired
(first-order number-theoretic) conclusion whatsoever.  What would people
do?

There would presumably be some effort to push the idea behind the
contradiction as far as possible, to see just how few axioms and
logical principles were needed to get a contradiction.  Then, something
would have to be rejected.  Some might reject classical logic, but only
if some replacement logic were available that would avoid the problem.
The alternative would be to learn to avoid certain instances of the
induction schema, or to avoid using certain combinations of instances.

It's starting to get hard for me to imagine staring at a specific and
explicit finite set of instances of the induction schema and being told
that I can't have all of them---especially if all of them are needed for
the proof of some familiar theorem of number theory.  So it's hard for me 
to predict how I, or anyone else, would react.

Can anyone else's imagination pick up where I've left off?

Tim