When adding choice to Zermelo–Fraenkel (ZF) set theory, one can go further than ZFC, by first adding classes, then adding global choice, and then proving that the resulting von Neumann–Bernays–Gödel (NBG) set theory is still a conservative extension of ZF. Now modifying the axiom schema of class comprehension to let the bound variables range over proper classes instead of just sets, one gets a proper extension of ZF, namely Morse–Kelley (MK) set theory.
So in a certain sense, MK looks like a "very natural" proper extension of ZF. The gospel sung by people like Roger Penrose and Ron Maimon somehow lead me to expect that it should be possible to prove the consistency of ZF in MK. However, I'm not even sure what is exactly mean by this.
- Is this meant in the laborious way of first formalizing the deduction system of ZF inside of MK? And then one had to prove that it is a theorem of MK that in the formalized deduction system $\phi$ and $\lnot\phi$ cannot both be proved simulateously?
- Is this just something straightforward? For example, take some part (or the whole) of the MK universe as model of ZF, find a suitable class/set interpretation for $\in$ (that's important, because $\in$ can't be represented as a set in ZF), translate $\land$, $\lor$, $\lnot$ as binary intersection, binary union and complement, $\forall$ and $\exists$ as arbitrary union and arbitrary intersection, and then show that everything works out fine, and all ZF axioms are satisfied?
- Or is the expectation that the consistency of ZF can be proved in MK simply wrong?