[FOM] What if ~Con(PA)?

[A.P. Hazen]

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