[FOM] Re: PA with a few symbols

[Ali Enayat]

This is a response to W. Taylor's query (July 18) concerning the possibility
of using finitely many quantifiers in the axiomatization of PA.

1. Ryll-Narzewski proved in 1952 that PA cannot be finitely axiomatized.
2. Later, Rabin (1961) proved that PA cannot be even axiomatized with an
infinite set of formulas of "bounded complexity" (in the arithmetical
hierarchy).

In contrast:

3. By a general theorem of Vaught (1967), for every recursively
axiomatizable theory T (such as PA, or ZF) there is a finitely axiomatizable
theory T*, in a richer language, such that T* is finitely axiomatizable and
T* is a conservative extension of T (i.e., if T* proves a statement S in the
language of T, T already proves S).

4. There are two distinguished finitely axiomatizable conservative
extensions of PA:

(a) The subsystem ACA_0 of second order arithmetic [This is classical, its
proof is a variant of the proof establishing the conservativity of
Gödel-Bernays class theory GB over ZF, going back to Gödel's use of finitely
many operations to simulate the comprehension scheme].

(b) The unorthodox system of set theory S = NFU + there is no infinite set +
"every cantorian set is strongly cantorian". [Solovay-Enayat 2002,
unpublished].

[Here NFU is Jensen's variant of Quine's NF system of set theory with a
universal class, where the extensionality axiom of NF is relaxed to allow
urelements; a set X is cantorian if there is a one-to-one correspondence
between X and the set of its singletons S(X) = {{v}: v in X}; X  is
*strongly cantorian* if the map sending v to {v} (as v varies in X) exists.
Of course in "normal set theory" every set is strongly cantorian, but in NF
and NFU this is no more true, e.g., the universal set V if not even
cantorian, and there are models of NFU + "there is an infinite set" + the
axiom of choice in which the set of natural numbers is cantorian, but not
strongly cantorian]