[FOM] What if ~Con(PA)?
A.P. Hazen
a.hazen at philosophy.unimelb.edu.au
Sat May 15 00:09:53 EDT 2004
Matthew Frank, suggesting that mathematics could go on, but based on
more "cautious" foundational systems, 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.
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.
For what it's worth, this corresponds to a well-understood, and
historically prominent form of "set theory," reflecting an ...
understandable, if not plausible... philosophical viewpoint.
For logic/set-theory, take Russell's Ramified Theory of Types
(the "logic" of "Principia Mathematica" minus the axiom of
Reducibility), and add an axiom of Infinity saying there are
infinitely many objects of lowest type.
John P. Burgess and A.P. Hazen, "Predicative Logic and Formal
Arithmetic," in "Notre Dame Journal of Formal Logic" v. 39
(1998), pp. 1-17
shows that I_Delta_0(exp) is interpretable in this system (but, by an
argument turning on Gödel's second Incompleteness theorem, that
arithmètic systems much stronger than that probably aren't).
---
Allen Hazen
Philosophy Department
University of Melbourne
More information about the FOM
mailing list