FOM: finite axiomatization of an extension of PA

[M. Randall Holmes]

Matt Insall asked:


PS:  I know I should look it up myself,
but I'll ask anyway.
Does anyone know af a conservative,
finitely axiomatizable extension of PA?
I ask this question,
because I find it interesting that Goedel's class-set theory
is a finitely axiomatizable conservative extension of Z(or ZF, depending on
what you mean by ``Class-Set Theory'') set theory.
Perhaps that is exactly what nonstandard analysis really is,
if one approaches it from a Nelsonesque perspective.

I comment:

NFU (Quine's New Foundations with urelements) + "the universe is
finite" + "every cantorian set is strongly cantorian" is precisely as
strong as PA (a result of Solovay and Enayat).  The cantorian natural
numbers of this theory satisfy PA.  The theory is finitely
axiomatizable, because the stratified comprehension scheme of NF
(shared by NFU) is equivalent to a finite set of its instances.  I
suspect that if one is willing to interpret "natural number" in PA's
sense as "cantorian natural number" in NFU's sense, that this theory
could be viewed as a finitely axiomatizable conservative extension of
PA.

                                      --Randall Holmes