# Is there a formalisation of set theory where unions can be taken over some classes that are not a priori known to be sets?

Of course, fully unrestricted unions in ZFC will immediately lead to inconsistency, but is there a variation where restrictions on allowed classes are given explicitly at least, in terms of the logical structure of the formula that defines the class? A particular class I have in mind is that of accessible cardinals, so Gödel-Bernays can't work since it is equivalent to ZFC.

In his original paper on ordinals Cantor asserts three "generation principles" for them. The third principle in rough translation is "if already generated ordinals share a property then they can be grouped together to form a new ordinal". He generates $\omega_1$ by using countability as the property on all ordinals generated after $\omega$. In ZFC this is justified by observing that countable ordinals can be a priori proved to form a set using the power set axiom.

There can't be such a justification for accessible cardinals of course, but the logical structure of countability doesn't seem to be much different from that of accessibility. Just postulating inaccessibles seems very ad hoc, from Cantor's original point of view they exist as much as $\aleph_1$.

• If I recall correctly Cantor's point of view was that the universe is some $V_\kappa$ for an $\aleph$-fixed point. Allow me to remind you that back at the day people didn't really work with axioms; and that Cantor had the real numbers at his disposal. More specifically, you don't need the power set axiom to prove that $\aleph_1$ exists -- you need the assumption that the real numbers is a set, and sufficient axioms to prove that $2^\omega=|\Bbb R|$. But this formulation is really just the power set axiom, stripped down to its necessary use in the proof. – Asaf Karagila May 25 '14 at 4:12
• Also, the third principle as you write it is surely inconsistent. Consider the property of being a set, then grouping all the ordinals which are sets give you a proper class. – Asaf Karagila May 25 '14 at 5:30
• In the 1883 paper Cantor dispenses with real numbers and doesn't stop at $\aleph_1$, he generates alephs indexed by arbitrary ordinals, and power sets would be out of place in his line of thought there. When he learned of 'ordinal of all ordinals' paradox in 1895 he got more careful and started distinguishing between sets and classes, but based on logical consistency only. – Conifold May 26 '14 at 23:17
• I'm not quite clear why you want to base your intuition on something which was ultimately noted as inconsistent and required correction. Instead you should base your intuition on something which was corrected and was not yet found inconsistent. – Asaf Karagila May 26 '14 at 23:18
• I have no idea what you're talking about in your last comment. – Asaf Karagila May 26 '14 at 23:28

Russell's type theory allows some unions over classes. Roughly speaking, sets are assigned types, unions can be taken over classes but only of sets of the same type. The union formed is assigned higher type than its constituents, thus avoiding the possibility of the "set of all sets".

Some modern category theorists are considering using type theory much more broadly than just taking unions over classes, more as a foundational alternative to set theory. Here is an excerpt from 2009 interview with Pierre Cartier (see discussion here):

"If category theory can easily be formulated within a framework of first-order logic (and this led to Lawvere formulation of set theory in this spirit), and if set theory received a proper axiomatization as the Zermelo-Frenkel system, the combination of both proved explosive. Some cures were attempted, like the use of universes by Grothendieck and Gabriel-Demazure. But this is highly artificial, like all methods using a universal domain, and brings us to the difficult (and irrelevant) problems of large cardinals in set theory.

The new approach should be based on a comprehension scheme. That is, a set is described by the characteristic property of its elements: the set of cats is defined by the property of being a cat, described as accurately as possible, without any claim about the totality of existing cats. This is a standard practice in typed languages in computer science... Such a language embodies rules to create new types out of old types... Usually, there is also available an abstraction principle, in the form of a $\lambda$-operation $\lambda x.t$ to describe a function associating to $x$ the value $t$ (described by a formula containing $x$). So the framework is a typed $\lambda$-calculus.

Of course, the implicit strategy is the one of Russell when he invented type theory to cure the diseases of set theory, like the set of all sets... I would also like to mention that the inner logic of a topos looks very similar, so we could perhaps formalize large segments of category theory within a syntactically defined universal topos."