Would strengthening Foundation and Choice in NBG, make it equi-consistent with MK?

Question

This is a follow up to an earlier question about strengthening of foundation in relation to proving the consistency of ZFC. It was shown that it would achieve that, but it may fail short of MK. Here, the question is about whether additional strengthening of choice can achieve that goal?

If we replace Foundation and Choice axioms of $\sf NBG$ (as in Mendelson's Introduction to Mathematical Logic) by the Foundation schema "$\sf FS$", and the following Class Well-ordering schema "$\sf CWO$", would the resulting theory be equi-consistent with $\sf MK$?

We add $\prec$ as a new primitive binary relation to the language of $\sf NBG$.

From hereafter $\Phi(X)$ is a formula in which "$X$" occurs free and only free, where "$Y$" doesn't occur, and whose free variables are among "$X,\vec{P}$". While $\Phi(X/Y)$ is the result of replacing every occurrence of "$X$" by "$Y$" in $\Phi(X)$.

Now, Axiomatize:

• Foundation schema: $\forall \vec{P}[\exists X (\Phi(X)) \to \exists X: \Phi(X) \land \forall Y (\Phi(X/Y) \to Y \not \in X)]$
• Class Well-Ordering: $\prec$ is transitive, connected and well-founded:

Transitive: $X \prec Y \prec Z \to X \prec Z$

Connected: $X = Y \lor X \prec Y \lor Y \prec X$

Well-Founded: $\forall \vec{P}[\exists X( \Phi(X)) \to \exists X: \Phi(X) \land \forall Y ( \Phi(X/Y) \to Y \not \prec X)]$

Answer 1

The answer is no.

This follows from a modification of Kameryn's answer at your other question. Namely, KM implies the existence of a transitive model of NBG, and transitive models will always satisfy the $\in$-induction scheme. But further, by taking the $L$ of that model, you will get $V=L$ as well, and this implies that there is a definable global well order of all the sets, giving us global choice. This by itself does not imply what you call class well order (well-ordering the classes), but since we have a transitive model of $\text{ZFC}+\text{V=L}$, we can also apply the $L$-order to the classes themselves, thereby providing an interpretation of $\prec$ that fulfills your theory.

Putting it all together, it follows that your theory cannot be provably equiconsistent with KM, since KM implies the consistency of it.

The argument is related to how one can realize a certain ambiguity in what V=L should mean in the class context. It is possible in a model of KM that every set is in L, but this is weaker than asserting that every class is constructible in the suitable sense, since one can force over the model to add generic classes, without adding any sets, but these generic classes will not be realized as constructible. However, in any KM model one can go to the inner model $L$ of all constructible sets, and also take as classes only those $X\subseteq L$ that are themselves witnessed as constructible in the (class encoded) constructible hierarchy that proceeds beyond Ord, using classes $\Gamma$ that encode well orderings beyond Ord. In this way, one produces a model of the class choice principle CC, showing that KM is equiconsistent with KMCC. Meanwhile, CC is known not to be provable in KM.