[FOM] Finite axiomatisation

[Stephen G Simpson]

Alasdair Urquhart writes:
 > 
 > > Also, there is some independent interest, I would think, in knowing
 > > the shortest, or close to the shortest, finite axiomatisation of PA.
 > >
 > > Does anyone have any ideas on how it would look?  Does anyone
 > > want to try it?
 > 
 > Perhaps the simplest way would be to apply the same trick that
 > generates NBG set theory from ZFC, that is to say, add a set of
 > axioms defining first-order properties.  It could be that this
 > has been already done in the literature.

Yes, this is very much in the literature.  See for instance my book
"Subsystems of Second Order Arithmetic," where the significance of
ACA_0 in reverse mathematics and foundations of mathematics generally
is discussed.  There it is pointed out that ACA_0 is a finitely
axiomatizable conservative extension of PA, analogously to how NBGC is
a finitely axiomatizable conservative extension of ZFC.  I have not
tried to write a short axiomatization of ACA_0, but clearly this could
be done along the lines suggested by Alasdair.

-- Steve

Name: Stephen G. Simpson

Affiliation: Professor of Mathematics, Pennsylvania State University

Research Interests: mathematical logic, foundations of mathematics

Web page: http://www.math.psu.edu/simpson/.