[FOM] Finite Axiomatizations

[Peter Aczel]

+++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
Harvey wrote

It is well known that BZ = bounded Zermelo set theory, and NBG = von
Neumman Bernay's Goedel class theory, are finitely axiomatizable. I
want to give a memorable formulation of this that I haven't seen
mentioned in the literature. Perhaps readers can refer me to a place
where this has been done?

...

THEOREM 2. Comprehension and 4 quantifier 2 parameter Comprehension
are equivalent over M Extensionality, M pairing, M Pairwise Union, M
Power Set.
​++++++++++++++++++++++++++++++++++++++++++++++++++++​


Curiously, the number 4 also crops up in the somewhat similar situation of
Quine's NF (New Foundations).

Theorem: NF is equiconsistent with the finitely axiomatisable subtheory NF_4

Peter A
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20150811/d75d398f/attachment.html>