[FOM] Re: Disaster?

[Matthew Frank]

In response to Tim Chow's post:
I don't find it so hard to imagine the inconsistency of PA.

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.

In that case, we would use something like elementary function arithmetic.
This is also known as I_Delta_0(exp), where the I stands for induction,
Delta_0 refers to the complexity of the induction formulas, and exp
indicates that the language of the theory goes beyond that of Peano
arithmetic to include an exponential function.

If elementary function arithmetic turned out to be inconsistent, we would
remove exp from the language, concluding that the infeasibility of
computing exponentials was indicative of the impossibility of any total
function with the properties of exponentiation.  And so on down....

Discoveries of such inconsistencies might well ignite wide interest in
non-classical logics, such as intuitionist logic.  However,
double-negations convert inconsistencies in classical arithmetics to
inconsistencies in intutionist arithmetics.  So switching to an
intuitionist logic wouldn't help in the above scenarios.

--Matt