Sets and classes as many (Q5928926)

This is an unorthodox development of set theory, based on the idea that classes (and, in particular, sets) are not individuals. This idea is not new, but Bell's approach introduces some technical embellishments. The language is to be two-sorted, with lower-case letters for individuals and upper-case letters for classes, and a primitive membership relation \(x\in Y\). There is a labeling function \(\lambda\) that assigns an individual \(\lambda X\) to every class. It is assumed that there is a subdomain \(S\) of the domain of classes on which \(\lambda\) is one-one. The classes belonging to \(S\) are called sets and any individual that is the label of a set is called an identifier. There is also a colabeling operation that assigns a class \(x^*\) to every individual \(x\) in such a way that \(X= (\lambda(X))^*\) for every set \(X\). A pseudo-membership relation \(\varepsilon\) can be defined on individuals: \(x \varepsilon y\leftrightarrow x\in y^*\). (This makes it possible to get reasonable interpretations of nonwellfounded set theories. For example, although the formula \(a=\{a\}\) now is not meaningful, its equivalent formulation \(\forall x(x \varepsilon a\leftrightarrow x=a)\) becomes \(a^*=\{a\}\). Likewise, the meaningless \(a\in a\) becomes \(a \varepsilon a\), that is, \(a\in a^*\).) An axiomatic formal theory M is presented, with suitable axioms for the identity relations on individuals and on classes, an extensionality axiom for identity of classes, an axiom of comprehension, and axioms for the labeling and colabeling operations. Then various extensions ZM, ZFM, \(\text{ZM}^*\), and \(\text{ZFM}^*\) of M are defined and shown to be equiconsistent respectively with Zermelo set theory Z, Zermelo-Fraenkel set theory ZF, Z with an axiom of foundation, and ZF with an axiom of foundation. Extensions of M also can be defined that are equiconsistent with Gödel-Bernays and Morse-Kelley set theory. The author also presents an extension MA of M corresponding to Ackermann set theory and an extension suitable for nonwellfounded set theory. (For the latter, M is extended to a theory \(\text{M}^{(,)}\) obtained by adding primitive terms \((x,y)\) for ordered pairs, governed by the usual axiom characterizing ordered pairs.) A more unorthodox extension MP of M is defined by adding an axiom scheme asserting that, for every formula \(\varphi(x)\) not containing any of the symbols for the predicates for identifiers and sets or for the labeling and colabeling operations, the class \(\{x:\varphi(x)\}\) is a set. MP is shown to be interpretable in the standard model for second-order arithmetic SOA. Moreover, by adding a function symbol for the successor operation and the corresponding Peano axioms, one obtains an extension \(\text{MP}^+\) of M having SOA as a subtheory. Finally, the author shows that the results of his paper [J. Symb. Log. 60, 209-221 (1995; Zbl 0829.03004)] on type-reducing correspondences can be carried over to \(\text{M}^{(,)}\).