# Can the consistency of ZF be proved in MK?

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?
• MK proves that the class $V$ is a model of ZF + global choice, in the internal sense. This is indeed because MK has class comprehension. – Zhen Lin May 2 '14 at 23:51
• The same thing was asked on MathOverflow: mathoverflow.net/questions/87238/… – Carl Mummert May 2 '14 at 23:57
• I didn't know about that question on MO. This certainly answers my question, even so I know from experience that it will take some time to digest the MO answers. However, there is no need to give simplified versions of the MO answers here, because I actually like digesting this sort of math. – Thomas Klimpel May 3 '14 at 0:17
• Are you expecting any other type of answer, then? – Asaf Karagila May 3 '14 at 5:30
• Joel David Hamkins wrote excellent blog post about this question. You can see it here. – Wojowu May 3 '14 at 13:44