FOM: finite axiomatization of an extension of PA

[Robert M. Solovay]

Of course, the simple answer is that ACA_0 plays exactly the same role to
PA that GB does for ZF. In particular, it is a finitely aximatizable
conservative extension of PA [by the same proof as the analagous result
for the pair GB:ZF.

On Mon, 8 Jul 2002, M. Randall Holmes wrote:

>
> 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
>