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

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.