[FOM] Finite axiomatisation

[Ali Enayat]

This note is a response to the following comment of Alasdair Urquhart
[in connection with finite axiomatizations of PA, Aug 20, 2008]

> 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, the above idea works, and leads to a finitely axiomatizable
system, let's call it FNBG (F for finitistic), in which the axiom of
infinity of NBG is replaced by its negation. FNBG was studied in the
1950's and 1960's; for example Rabin proved in 1958 that FNBG has no
recursive model (Rabin's theorem is one of the precursors of
Tennenbaum's theorem). Another prominent source of study of FNBG is a
1964 paper of Vopenka, in which he showed that both the power set
axiom and the axiom of choice (even global choice) can be proved from
the rest of the axioms of FNBG.

The recent joint work of Solovay and myself has unearthed a very
different finitely axiomatizable set theory (which has a universal
set) with the same "arithmetical content" as PA; it is a system
obtained from the Quine-Jensen system NFU of set theory by replacing
the axiom of infinity by its negation, and adding the statement "all
cantorian sets are strongly cantorian".

These days it is more popular to think of FNBG in the guise of the
subsystem ACA_0 of second order arithmetic (FNBG and ACA_0 are
bi-interpretable). It is worth noting, however, that even though FNBG
and ACA_0 manage to encapsulate, in finitely many axioms, the content
of PA, they end up producing failures of the induction scheme *in the
extended langauge*. This is the consequence of a general result about
the failure of finite axiomatizability of induction on natural
numbers, but in the case of ACA_0, there is even a combinatorial
incompleteness (foreshadowing the Paris-Harrington one), as described
below:

For each concrete natural number n, ACA_0 can prove Ramsey's theorem
for exponent n,  but ACA_0 is unable to prove the statement " for all
exponents n, Ramsey's theorem holds".  This was independently noted by
a number of people, including Harvey Friedman and Hao Wang ; e.g., see
p.25 of Wang's "Popular lectures on mathematical logic" (Dover
Publications), in which he establishes the above incompleteness, using
a result of Jockusch . By the way, Wang refers to ACA_0 as PPA
(Predicative Peano Arithmetic).

Best regards,

Ali Enayat