Tarski's axiom A, MK set theory and the Global Choice axiom

Question

In a message of the 29 th March 2008 edited on the FOM list "AC and strongly inaccessible cardinals", Robert Solovay shows that the so-called Tarski-Grothendieckset set theory can be equivalently axiomatized as: (1) ZFC + "There exists a proper class of strongly inaccessible ordinals" (2) ZFC + "Every set is member of a Grothendieck universe U" (3) ZFC + "Every set is member of some Tarski class" Moreover, in the case (3), it is possible to show that the added Tarski's axiom A allows to dispense with the three ZFC axioms of Power set, of Infinity and of Choice, so that the Tarski-Grothendieck set theory can be axiomatized using only the following list of axioms: Extensionality, Foundation, Null set, Pair set, Replacement, Union and Axiom A:

First question: Would it be possible to dispense with the Pair set axiom ?

Suppose now that we change our basic set theory from ZFC to MK (Morse-Kelley) set theory. In this context a more natural choice axiom is the Global Choice axiom ("There exists a set-like well-order on the universal class V"), so that:

Question 2: Is it possible to derive the Global Choice axiom from the set theory (4) MK + "There class of strongly inaccessible cardinals is a proper class", where we do not suppose the axiom of choice in MK ? Gérard Lang

Answer 1

Question (1) is answered by the observation that pairing follows easily from replacement, once a two-element set exists.

For question (2), the answer is negative. I claim that from a suitable consistency assumption, it is consistent that we have the version of KM without global choice, but with AC for sets, plus a proper class of inaccessible cardinals. You cannot get global choice for free this way just from a proper class of inaccessible cardinals.

The point is that basically all the methods for producing models of set theory without global choice work well with a proper class of inaccessible cardinals. One can start with a model of KM plus a proper class of inaccessible cardinals, and then perform a class iteration of Cohen forcing, and take what amounts to the symmetric extension by this construction.

For example, use the forcing in my answer to Asaf Karagila's question, Does ZFC prove the universe is linearly orderable? That argument produced a model of GB+AC in which global choice failed, and not only that, but the universe was not linearly orderable. If the ground model had inaccessible cardinals, these would continue to exist in the extension. This answers the Gödel-Bernays version of question (2).

But you asked about Kelley-Morse set theory without global choice. In this case, you can't just use the definable classes, but you can take all the classes that are first-order definable with a ground-model class parameter. This will satisfy KM without global choice (but with AC) in the extension, and still have a proper class of inaccessible cardinals.