[FOM] ZFC with classes (ZFCC?)

[A.P. Hazen]

(((This is an expansion of Vladik Kreinovich's answer to Victo 
Makarov's query.)))
Victor Makarov asks about a system of set theory that would 
incorporate ZFC but also allow reference to (quantification over) 
proper classes.  He gives axioms, and asks whether the system is 
known in the literature.
    On a quick first perusal, his axiom 0 (x is in {y:Fy} iff Fx}) 
looks like the inconsistent "naive" comprehension principle for 
classes.  The systems mentioned below avoid Russell's paradox by 
restricting this: **provided x is a Set,** x is in {y:Fy} iff Fx.  In 
what follows, I assume Makarov intended this restriction, (so the 
theory of classes in effect amounts to full Second Order Logic, where 
individuals are the Sets).  (Please forgive me if I read too hastily 
and missed what he really intended!)  Some, but not necessarily all 
classes are Sets; the rest of his axioms mimic the axioms and axiom 
schemes of ZFC: if ZFC tells you therre is a set, Makarov's axioms 
tell you that the class of that sets members is a set.  One 
difference: the axiom schemes (Aussonderung, Replacement) of ZFC 
specify new sets by reference to formulas of the (first-order) 
language of ZFC; Makarov's corresponding axioms allow the use of 
formulas quantifying over classes.
    This system is known; Vladik Kreinovitch points out that it is the 
system of Kelly, known in the literature as "MK".  ("K" for Kelly, 
"M" because an apparently equivalent system, b7ut formulated in an 
idiosyncratic formal language rather than in standard First-Order 
logic, was presented by A.P. Morse in his "A Theory of Sets.")
    MK is described (briefly) by Quine in the later parts of "Set 
Theory and Its Logic" and by David Lewis in "Parts of Classes" (which 
argues for an even richer system: one essentially allowing 
hyperclasses as well as classes: if MK is thought of as a version of 
Second-Order ZFC, Lewis  argues for a Third-Order version).  It is 
used as the background metatheory in Mostowski's book "Constructible 
Sets with Applications."
    The history (alluded to by Kreinovich) is interesting.  Proper 
classes got into formalized set theories with Von Neuman, and are 
most familiarly used in the VonNeuman-Bernays-Gödel set theory (GB, 
NGB... probably other combinations of initials are used as well). 
This system, however, postulates classes only as defined by formulas 
of the First-Order language of ZFC: formulas of the language of GB in 
which proper classes are quantified over are not assumed to define 
classes.  (Thus, if MK is thought of as ZFC in **full** Second-Order 
logic, GB is ZFC in a Russellian "predicative" Second-Order logic: 
cf. sections 58,59 of Church's "Introduction to Mathematical Logic" 
for formalization of this logic in the "pure state," without thinking 
of the individuals as sets.)
    A theory formulated in Second-Order logic can replace the axiom 
schemata of the corresponding First-Order theory with single axioms. 
Because of the weakened Comprehension assumptions for classes, the 
resulting axioms of BG have exactly the strength of the axiom 
schemata of ZFC: GB is a conservative extension of (First-Order) ZFC.
    The use of a "Full," impredicative, theory of proper classes in 
the formalization of a set theory seems to be due to Quine, in his 
"Mathematical Logic" (first edition: 1940).  Unfortunately, in 
attempting to formulate a Second-Order version of his First-Order set 
theory NF, Quine produced an inconsistent theory.  Hao Wang showed 
how consistency could be restored by an appropriate restriction on an 
axiom *scheme* (note: an axiom scheme is used despite the 
Second-Order nature of the formal language) specifying which classes 
are sets: Wang proved that the resulting system is consistent if 
First-Order NF is, and it is used in the revised edition of Quine's 
book.
     Quine, in "Set Theory and its Logic," mentions a proposed system 
NQ which he describes as standing to ZFC in the relation in which 
Wang's revision of ML (= the system of Quine's "Mathematical Logic") 
stands to NF.  Wang's relative consistency proof would carry over: 
such a system is provably consistent relative to ZFC.
     MK -- the system Makarov asks about -- is properly stronger than 
this, because its Sethood axioms  do not incorporated Wang's 
restriction.  MK can prove the consistency of ZFC: formally one might 
say that it stands to ZFC as the original, inconsistent, version of 
ML stands to NF!
     MK has not been shown inconsistent; as far as I know most set 
theorists would be almost as surprised if it turned out to be 
inconsistent as they would if ZFC itself did.  (The consistency of MK 
follows from ZFC + "there exists a strong inaccessible.")  ... Which, 
to close with a philosophical remark, some would take as evidence 
that ZFC is based on a clearer "intuition" of the set-theoretic 
"universe" than NF.
---
Allen Hazen
Philosophy Department
University of Melbourne