In her blog post Variants of Kelley-Morse set theory, Prof. Gitman proves that every model of the the common version of Kelley-Morse set theory ($\mathsf{KM}$) is a model of the Wikipedia version of $\mathsf{KM}$ and conversely. While this is an interesting result in its own right, her presentation of the "common version" of $\mathsf{KM}$ leads me to ask the following question:
Can $\mathsf{KM}$ set theory as it stands allow us to break through the $\mathsf{AC}$ barrier (the $\mathsf{AC}$ barrier—that is, $\mathsf{AC}$ itself—is what allegedly forbids the existence of Reinhardt cardinals to exist via the Kunen inconsistency theorem).
Clearly, $\mathsf{KM}$ set theory is important for the proof of the Kunen inconsistency; the Kunen inconsistency, as Kunen actually stated in his paper is
If $j$ is an elementary embedding from $V$ into $V$, $j$ is the identity.
As has been stated by the authors of Generalizations of the Kunen Inconsistency (Annals of Pure and Applied Logic, vol.163, No.12, pp.1872–1890, doi:10.1016/j.apal.2012.06.001, arXiv link) and The Role of the Foundation Axiom in the Kunen Inconsistency (arXiv link), $\mathsf{KM}$ is the only set theory in which the Kunen inconsistency can be properly stated, because it is only in $\mathsf{KM}$ that one can prove the existence of a full satisfaction class for first-order truth, making the assertion "$j$ is elementary" expressible in $\mathsf{KM}$.
With this in mind, let me restate the "common version" of $\mathsf{KM}$ as given in Prof. Gitman's blog post, for reference:
The axioms for sets are Extensionality, Pairing, Infinity, Union, Powerset, Regularity. The axioms for classes are:
- Extensionality
- Full Class Comprehension: If $\phi$(x) is any formula in the two-sorted language [one sort for sets, one sort for classes—my comment] with class parameters, then the collection of all those sets such that $\phi$(x) holds is a class.
- Replacement: If $F$ is a class function and $a$ is a set, then the range of $F|a$ is a set.
- Global well-order: there is a 1-1 and onto class function $\phi: \mathrm{ORD} \to V$. [Question: do class axioms (3) and (4) imply that every set can be well-ordered?]
The following question (at least to me) immediately presents itself:
Does class axiom (4) (provided it well-orders $V$) imply the Kunen inconsistency? If so, then it certainly does not provide a means for surmounting the $AC$ barrier.
In order to remedy that situation, one could always weaken (4) in the following fashion:
4'. There is a 1-1 class function $\phi : \mathrm{ORD} \to V$. Let there be a proper subclass $U$ of $V$ such that $\phi : \mathrm{ORD} \to U$ be 1-1 and onto, but there are no bijections from $ORD$ to $V$ .
Indeed, if one is a believer is the set-theoretic multiverse, there are models of $\mathsf{KM}{-}(4){+}(4')$ in which $U$ is countable. The question that remains, however, is whether (4) is needed to make "$j$ is elementary" expressible in $\mathsf{KM}$.
Something is not clear to me about your question.
Global choice implies the axiom of choice for sets. Of course it does. Every set is a subclass of $V$, and if $V$ can be well-ordered, then every set can be well-ordered.
Requiring that there is an injection from the class of ordinals into $V$ is provable in $\sf ZF$. This function is the identity function. If you wish for something less trivial, $\alpha\mapsto V_\alpha$ is also an option.
Expressing "elementary for sets" has nothing to do with the axiom of choice.