FOM: Finitely axiomatizable theories of sets

[JoeShipman@aol.com]

Thanks to the FOM respondents who confirmed that Zermelo Set Theory and Peano Arithmetic share with ZFC the "reflexive" property: they [and their extensions]prove the consistency of any finite axiomatized subtheory of themselves .

Friedman points out that ZFC has not only this property, but also this property relative to the non-finitely-axiomatizable subtheory Z -- so that not only finitely axiomatized subtheories of ZFC, but subtheories axiomatized by finite extensions of Z, are provably consistent.

However, though Friedman is correct that "in any finite language supporting a small amount of arithmetic, any system that contains full induction must prove the consistency of any finitely axiomatized subtheory", so one cannot embed PA in a finitely axiomatized system in the language of arithmetic, one CAN embed PA in a finitely axiomatized system in the language of set theory.  This is what I was asking about before, which no one picked up on -- are there interesting finitely axiomatizable theories of sets that allow one to do all or most of "ordinary mathematics"?

Of course it is possible to make a finitely axiomatizable theory by adding a proper class predicate (or its complement, the set predicate).  This is not even necessary -- since in VNBG sethood and proper classhood are definable (x is a set iff it is an element, x is a proper class iff it is not an element), we can just take the finitely many VNBG axioms, and substitute the definition of the predicate for the predicate.

This doesn't contradict the result that no extension of ZFC is finitely axiomatizable, because the theory is no longer about sets, it is about classes.  (Actually, BOTH ZFC and this version of VNBG are really about neither sets nor classes, they are about elementhood.)  The statement "there exists x for all y not (x /in y)" is true of classes but not of sets.

But the question remains, is there a finite set of axioms ABOUT SETS (not merely in the language of set theory, because the modified VNBG described above is in the language of set theory) which suffices to do "ordinary mathematics"?  

Here's one: 

ZC' : "ZFC without replacement, plus 'every theorem of ZC is true in V_(omega+omega)', plus the finitely many instances of replacement necessary to allow for a definition of "truth in V_(omega+omega)".  

This will allow proof of any theorem of ZC which only talks about "small" sets, because those theorems are provably equivalent to their relativized-to-V_(omega+omega) versions.

Is there a more natural version of this?  Well, if we look at the subtheories ZFC1, ZFC2, .... where ZFCn = 'ZFC with Replacement restricted to pi_n formulas', one of them certainly includes ZC'.  The theories ZFCi are not finitely axiomatized, but since pi_n truth is definable by a pi_(n+1) formula, each one of them has a finitely axiomatized extension by a similar trick.

Question 1:  do these finitely axiomatized theories of sets have any more natural equivalents that would make sense as alternatives to the infinitely axiomatized theories ZC and ZFC?

Question 2: what is the most natural-looking finite axiomatization of VNBG?  The standard ones look ugly to me, though I may just be prejudiced.  

-- Joe Shipman