Is the definition of the arbitrary union of proper classes valid in Morse-Kelley set theory?

I am recently studying Morse-Kelley set theory (MK). There is an axiom called the axiom of class comprehension, which states that, given a predicate $$\phi(x)$$ written in the language of first-order logic with the term class and $$\in$$, then there is a class $$C = \{x: \phi(x) \land \exists y\;(x \in y) \}$$. Formally, $$\exists C\; \forall x\; (x \in C \iff \phi(x) \land \exists y\; (x \in y)).$$

Then, I suspect that the definition of arbitrary union of classes (not necessarily sets) can be defined as:

Given a predicate $$\phi(x)$$ in the context of the theory, the union of all classes $$C$$ satisfying $$\phi(C)$$ is defined as:

$$\bigcup_{P(C)} C := \{x: \exists C\; (\phi(C) \land x \in C)\}.$$

For the sake of convenience, let's define the predicate $$P(x)$$ as "$$\exists C\; (\phi(C) \land x \in C)$$", then, for any class $$x$$, we have $$P(x) \iff P(x) \land \exists y\; (x \in y),$$ as $$x \in C$$ in the clause of the definition. So, by the axiom of class comprehension, this definition is valid.

1 Answer

The answer to your title question is yes, when interpreted as you indicate in the body of your text.

This kind of union of classes is definable in the second order theory, and you have in fact already given the formula that defines it:
$$\exists C\ (\phi(C)\wedge x\in C).$$ Thus, the union class exists by an instance of class comprehension.

Note that this is a second-order formula, and Kelley-Morse does include class comprehension for second-order formulas. This is precisely the difference between KM and Gödel-Bernays set theory GBC, which includes class comprehension only for first-order formulas.

Indeed, your conception of union-of-classes is exactly the meaning of the second order quantifier $$\exists C$$. The semantics you provided is exactly the meaning of $$\exists C$$ in a formula.

But let me add finally that your title question is naturally interpreted somewhat more broadly than the remarks in the body of your post. In the body of your post, you had a uniform definability requirement, namely, that we take the union of a definable family of classes $$C$$, those with $$\phi(C)$$ for some specific $$\phi$$.

But if we seek to take the union of a truly arbitrary family of classes, then this is not generally possible. The reason is that Kelley-Morse set theory can be true in a model that does not literally have as classes all subsets of its domain. That is, we use the Henkin semantics with KM rather than the full second-order semantics. Some possible classes may be missing. But every subset of the domain is the union of its singletons, and each singleton exists in the model.

In summary, in general, in Kelley-Morse we cannot always take the union of a truly arbitrary family of classes. But we can take the union of a uniformly definable family of classes.

• Thank you and happy to hear the answer is yes! I am self-teaching but I find it is difficult to find the answer for this although it is quite clear to me -- well, that is why I was worrying about it. Talking about the GBC, I did read the first 2 chapters of Gödel's paper about the AC and GCH, and I did remember he proved this axiom schema from the Group B axioms, but thanks to notice me that the system is indeed built upon first order logic only, I didn't notice the difference -- I thought the $\phi$ in the above axiom is just a "placeholder for predicates". Commented Feb 24 at 12:22
• Glad to help, and thanks for accepting. (By the way, did you know that you can also upvote my answer? Click on the up arrow. It is normal and encouraged to upvote answers that you find worthwhile.) Commented Feb 24 at 12:27
• Yeah, I noticed the up arrow, and I clicked several times but the system tells me: "Thanks for the feedback! You need at least 15 reputation to cast a vote, but your feedback has been recorded." X( Commented Feb 24 at 12:29
• Ah, you are new and have only 13 currently. Soon, you will have enough! Commented Feb 24 at 12:32
• Thank you! I subscribed your YouTube channel :))) Commented Feb 24 at 12:46