FOM: Finitely axiomatizable fragments of set theory

[Harvey Friedman]

It has been known for a very long time 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.
This might well be due to Kriesel and Takeuti (joint paper), or even
earlier. Hence any such system must not be finitely axiomatizable. This
applies to PA and Z.

One can ask, for example, if there is a consistent extension of ZFC which
is finitely axiomatized over Z. Once again, the answer is no. Any extension
of ZFC proves the consistency of any subtheory finitely axiomatized over Z.