This is a follow up to an earlier questionquestion 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)]$