$\sf MKCWO$ is the theory obtained by adding a new primitive binary relation $\prec$ to the signature of $\sf MK$ and axiomatize that $\prec$ is a well order on classes, that is:

  • $\textbf{Transitive:} X \prec Y \prec Z \to X \prec Z $
  • $ \textbf{ Connected:} X \neq Y \leftrightarrow [X \prec Y \lor Y \prec X]$
  • $\begin{align} \textbf{Well-Founded:}& \text { for each formula } \phi: \\ & \phi(X) \to \exists M: \phi(M) \land \forall Y \, (\phi(Y) \to \neg Y \prec M) \end{align} $

What is the choice principle that needs to be added to $\sf MK$ in order to get an equivalent theory?

I was thinking of something along those lines:

To the language of $\sf MK$ add a monadic symbol $\varepsilon$ that takes a formula as an argument, such that for any formula $\phi$ having one free variable [whether set or class variable], the string $\varepsilon\phi$ is a term of the language. Then axiomatize:

  • $[\phi \leftrightarrow \psi] \to \varepsilon\phi = \varepsilon\psi$
  • $(\exists X\phi) \to\exists Y: Y=\varepsilon\phi$
  • $\phi(\varepsilon\phi)$

However, it's not clear to me how the second formulation can interpret the first one?

Are these formulations equivalent?

If not, can we express a choice principle whose addition to $\sf MK$ would be equivalent to $\sf MKCWO$?

Note: to avoid confusion in comments, the notation $\varepsilon$ replaced the older notation $c$. Also $\sf CWO$ replaced the older notation $\sf WO$.

  • $\begingroup$ Probably you want to allow class parameters in your well-foundedness scheme. $\endgroup$ Dec 10, 2023 at 14:27
  • $\begingroup$ @JoelDavidHamkins, Yes, there is no restriction against that. $\endgroup$ Dec 10, 2023 at 14:38
  • $\begingroup$ I would recommend the notation $\varepsilon\phi$ in place of $c\phi$, since you are positing a selection operator. $\endgroup$ Dec 10, 2023 at 17:13
  • $\begingroup$ @JoelDavidHamkins, OK. I've done it. Thanks! You'll need to modify your answer accordingly. $\endgroup$ Dec 10, 2023 at 18:43

1 Answer 1


Usually the notation WO refers to the well-order principle for sets only, and this is usually taken as part of KM. So let me refer to your global-well-order principle as the class-well-order principle CWO, since your relation $\prec$ is placing a well-order on classes.

First, I claim that that CWO is not provable in KM, in the sense that we can have models of KM that have no second-order definable relation $\prec$ fulfilling CWO. One way to produce such a model is to start with an inaccessible cardinal $\kappa$ in ZFC and then force to add Cohen subsets to $\kappa$ and build a symmetric extension $V\subseteq W$ such that the axiom of choice fails in $W$ for subsets of $\kappa$. But since no sets were added below $\kappa$, we still have KM in the structure $\langle V_\kappa,\in,P(V_\kappa)^W\rangle$. In this model, we have KM, including global choice, but no definable well-ordering of the classes, since there isn't even such a well-order in $W$, and so definable CWO fails. Furthermore, inside $W$ there is no way to place a relation $\prec$ on this KM model so as to satisfy CWO. I believe that one can omit the need for the inaccessible with a more careful argument over KM itself.

Second, I claim that your proposed axiom involving $\varepsilon\phi$ does not imply CWO, and indeed, your proposed axiom is already provable in KM. Your proposal is that $\varepsilon\phi$ chooses an element of the definable class $\{x\mid \phi(x)\}$. Thus, you have a global choice function that operates on classes, not just on sets. But this is equivalent to global choice, since if $F$ is a global choice function on sets, so that $F(x)\in x$ for every set $x$, then we can also choose from classes, since we just apply $F$ to the minimal-rank elements of any class. That is, we can define $\varepsilon\phi$ to be $F$ applied to the minimal-rank elements of $\{x\mid\phi(x)\}$. Thus, your axiom is true in every model of KM. (See my blog post [The global choice principle in Gödel-Bernays set theory](https://jdh.hamkins.org/the-global-choice-principle-in-godel-bernays-set-theory/) for further various equivalent formulations of global choice.)

[Update] You have clarified in the comments that you intended the proposed class-choice principle is picking classes from definable collections of classes. Thus, for any formula $\phi(X)$ with a class variable, if there is any class realizing it, then $\varepsilon\phi$ is a class realizing it.

This principle is of course a consequence of CWO, since one can take the $\prec$-least instance. And conversely, one might hope to prove from that axiom that CWO holds, by iteratively choosing classes along a meta-class order, in the same manner that Zermelo proves the well-order principle from the axiom of choice.

That method, however, will not work in all models of KM. For example, if $\kappa$ is inaccessible in ZFC and $2^\kappa=\kappa^{++}$, a situation one can arrange by forcing, we may consider the corresponding KM model $\langle V_\kappa,\in,P(V_\kappa)\rangle$. In this model, there are only $\kappa^+$ many meta-ordinals, but $\kappa^{++}$ many classes, and so the iteration will not succeed in placing all the classes in order.

We can certainly augment this model with an interpretation of $\varepsilon\phi$, choosing a class from every definable meta-class, so as to realize KM plus your proposed axiom, but it is not yet clear to me whether we can do so without having any class well-order $\prec$ definable from it. I believe this is possible.

Meanwhile, let me also point out that your proposed axiom implies the class-choice axiom CC [see article "Kelley-Morse set theory does not prove the class Fodor principle" end of page 4 and beginning of page 5], which asserts that if every set $a$ has a class $A$ with $\varphi(a,A,Z)$, then there is a class $X\subseteq V\times V$ for which $\forall a\ \varphi(a,X_a,Z)$, where $X_a$ is the $a$th section of $X$. This axiom is known not to be provable in KM, although KM+CC is interpretable in KM as I explain below. The point is that with your principle, we can form $X$ by using $\varepsilon\varphi(a,\cdot,Z)$ to place the chosen witness $A$ for which $\varphi(a,A,Z)$ on slice $a$.

Lastly, you ask about interpretation, and indeed KM can interpret a model of KM+CWO, in which $\prec$ is second-order definable. That is, we don't need any choice operation $\varepsilon\phi$ at all to interpret KM+CWO. The reason is that if KM holds in $V$, then we can interpret the constructible universe $L$, and furthermore, we can take as classes only those that are witnessed as constructible at a meta-ordinal stage represented by a class in $V$. That is, using the classes of $V$, we can represent "ordinals" beyond $\newcommand\Ord{\text{Ord}}\Ord$ by well-founded class relations on $\Ord$. And by the standard coding techniques using well-founded extensional binary relations on $\Ord$ to code "sets" of rank above $\Ord$, we can refer to the stages of the constructible universe above $\Ord$. Let us take the model $L$ as constructed in $V$, using classes those that are witnessed as constructible at some such meta-ordinal stage. One can show that this satisfies all the KM axioms, and furthermore, there will be a definable well-order of the classes in this model arising from the $L$ order on the meta-ordinal stages.

This method is the main method used to show that KM is equiconsistent with KM+CC. It has appeared in several papers, and there is a very nice account of this class-coding method in the dissertation of my student Kameryn Williams.

  • $\begingroup$ Just to clarify my intention behind defining $c\phi$, this is meant to choose a class [it might be proper] from a collection of all classes fulfilling $\phi$, notice that by collection it is not meant to be a class in the sense of MK. So, the chosen class might not be an element of any class. $\endgroup$ Dec 10, 2023 at 14:35
  • $\begingroup$ Ah, I suspected you might have meant that. In that case, you should use an upper-case letter in $\exists y\ y=c\phi$, since the convention is lower-case = first-order, upper-case = second-order for variables. $\endgroup$ Dec 10, 2023 at 14:46
  • $\begingroup$ Yes, Correct. I've corrected it. Thanks! $\endgroup$ Dec 10, 2023 at 14:55
  • $\begingroup$ I wonder if the CC principle is equivalent with the $\varepsilon$ choice principle? There is a superficial difference that of the latter being able to chose from collections of classes that can be strictly bigger than the class $V$ of all sets, while the CC principle on the face of it doesn't state this result. Yet, still I wonder if this superficial difference is a real one?! Can we have $\varepsilon$ choice fail while CC preserved? $\endgroup$ Dec 11, 2023 at 20:59
  • $\begingroup$ I've been speaking with Victoria Gitman, who has worked at length on many of these issues, particularly with the interpreted versions in $\text{ZFC}^-$ models, and there is a big spectrum of principles in this vicinity, with everything open about how they relate to one another or whether they are equivalent or inequivalent. There are some very hard questions in this neighborhood. $\endgroup$ Dec 11, 2023 at 21:47

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.