FOM: Finitely axiomatizable fragments of set theory

[JoeShipman@aol.com]

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?

-- Joe Shipman