FOM: reflexivity of PA

[Michael Detlefsen]

Joe Shipman wrote:
_______________
ZC and ZFC are not finitely axiomatizable.  I know no consistent extension
of ZF is finitely axiomatizable, but is it also true that no consistent
extension of Z or ZC is finitely axiomatizable?

You can certainly replace Comprehension with "everything ZC proves about
sets of rank less than omega+omega is true", after using finitely many
instances of Replacement to define truth for V_(omega+omega), but this
won't extend ZC because you won't get ZC-theorems about sets of higher
rank.  (On the other hand, you will have gotten a finitely axiomatizable
theory that will suffice for 99+% of ordinary mathematics.)  If you try
instead to add an axiom of the form "there are no sets of rank omega+omega"
you won't be able to define truth for V_(omega+omega).

There are also the finitely axiomatizable subtheories ZF1, ZF2, ...where
ZFn contains the axiom "Every Pi_n theorem of ZFC is true" and the finitely
many instances of Replacement needed to define truth for Pi_n formulas.  Do
these theories have any mathematical or metamathematical significance, or
any nicer finite axiomatizations?

A final question: ZF proves the consistency of any finitely axiomatizable
subtheory of itself.  Do Z and PA also have this property?
_______________

As Richard Heck indicated, the answer to the 'final question' is 'yes' for
PA. This was proved in 1952 by Mostowski in 'On Models of Axiomatic
Systems', Fundamental Mathematicae 39 (1952): 133-158, Theorem XVIII. It
was used by Mostowski (and also Montague in 1957) to conclude the
non-finite axiomatizability of PA. In the same volume of FM in which
Mostowski's paper appeared, Ryll-Nardzewski ('The Role of the Axiom of
Induction in Elementary Arithmetic') gave a more 'direct' proof of the
non-finite axiomatizability of PA.

Mic Detlefsen