I've come across several references to MK (Morse-Kelley set theory), which includes the idea of a proper class, a limitation of size, includes the axiom schema of comprehension across class variables (so for any $\phi(x,\overline y)$ with $x$ restricted to sets, there a class $X=(x : \phi(x,\overline y))$).

I have seen various statements about MK and how it proves the consistency of various things, including $Con(ZF)$, $Con(ZFC)$, $Con(NBG)$, and in fact, for any $T\subset MK$ finitely axiomatized, it proves $Con(T)$.

However, and quite frustratingly, I don't see any references to back up these claims, except occasionally links to other places where the claim was made, but not proven (or even proof-sketched). I would really appreciate a reference where I can see a proof of these claims, or (if it's easier) a quick sketch of why it should be true.

It's not obvious to me at all why quantifying across proper classes should allow this sort of thing, since all relevant sets (sets of proofs, or sets of statements, or whatever) should be contained in some subset of $\omega$, so should be able to be constructed in $ZF$.


5 Answers 5


Let me give an easier (sketch of an) answer to the part of the question about proving Con(ZFC) in MK. Unlike Emil's answer, the following does not cover the case of arbitrary finitely axiomatized subtheories of MK. Intuitively, there's an "obvious" argument for the consistency of ZFC: All its axioms are true when the variables are interpreted as ranging over arbitrary sets. (The universe is a model of ZFC, except that it isn't a set.) And anything deducible from true axioms is true, so you can't deduce contradictions from ZFC. The trouble with this argument is that it relies on a notion of "truth in the universe" that can't be defined in ZFC. What goes wrong if you try to define, in the language of ZFC, this notion of truth (or satisfaction) in the universe? Just as in the definition of truth in a (set-sized) model, you'd proceed by induction on formulas, and there's no problem with atomic formulas and propositional connectives. Quantifiers, though, give the following problem: The truth value of $\exists x\ \phi(x)$ depends on the truth values of all the instances $\phi(a)$, and there are a proper class of these. In showing that definitions by recursion actually define functions, one has to reformulate the recursion in terms of partial functions that give enough evidence for particular values of the function being defined. (For example, the usual definition of the factorial can be made into an explicit definition by saying $n!=z$ iff there is a sequence $s$ of length $n$ with $s_1=1$ and $s_k=ks_{k-1}$ for $2\leq k\leq n$ and $s_n=z$.) If you use the same method to make the definition of "truth in the universe" explicit, you find that the "evidence" (analogous to $s$ for the factorial) needs to be a proper class. So ZFC can't handle that (and it's a good thing it can't, because otherwise it would prove its own consistency). But MK can; it's designed to deal nicely with quantification of proper classes. So in MK, one can define what it means for a formula to be true in the ZFC universe. Then one can prove that all the ZFC axioms are true in this sense and truth is preserved by logical deduction (here one uses induction over the number of steps in the deduction). Therefore deduction from ZFC axioms can never lead to contradictions.

  • $\begingroup$ I believe that all the details of this approach to proving Con(ZFC) in MK are in Mostowski's book "Constructible Sets With Applications". $\endgroup$ Commented Feb 1, 2012 at 19:47
  • $\begingroup$ Not quite, one also needs to prove that contradictions are not true in the ZFC universe $\hspace{.6 in}$ (which can easily be done). $\:$ $\endgroup$
    – user5810
    Commented Feb 1, 2012 at 21:09
  • 1
    $\begingroup$ @Ricky: You're right. The non-truth of contradictions is, fortunately, covered by the "no problem with ... propositional connectives" in my answer. Once you define what truth means for conjunctions and for negations, it is immediate that $\phi\land\neg\phi$ is never true. $\endgroup$ Commented Feb 1, 2012 at 23:43

This is an instance of a much more general result. (See Visser [2] for an overview of various related principles.) A theory is called sequential if it supports encoding of sequences of its objects with some basic properties. As a part of the definition (which I omit here as it is technical and not particularly relevant, it can be found in Pudlák [1]; see Visser [3] for more discussion), a sequential theory has some designated natural numbers (which serve as lengths of sequences) defined by a predicate $N(x)$. Usual theories of sets or classes are sequential, with $N(x)$ being $x\in\omega$.

Theorem: For any sequential theory $T$, the following are equivalent:

  1. $T$ proves full induction: the schema $$\forall\bar y\,[\varphi(0,\bar y)\land\forall x\,(N(x)\land\varphi(x,\bar y)\to\varphi(x+1,\bar y))\to\forall x\,(N(x)\to\varphi(x,\bar y))]$$ for all formulas $\varphi$.

  2. $T$ is uniformly essentially reflexive: for every formula $\varphi(x)$ and a finite subtheory $S\subseteq T$, $T$ proves $N(x)\land\Pr_S(\left\ulcorner\varphi(\dot x)\right\urcorner)\to\varphi(x)$, where $\Pr_S$ denotes the provability predicate for $S$, and $\dot x$ the numeral for $x$.

MK proves full induction, since it has induction for subsets of $\omega$, and the full comprehension schema guarantees that any property of natural numbers defined by a formula actually defines a subset of $\omega$. (Notice that this fails for NBG: due to the restrictions on its comprehension schema, NBG in general cannot prove induction for formulas with class quantifiers.) Thus, MK is uniformly essentially reflexive. In particular, if we take $0\ne0$ (with no occurrence of $x$) for $\varphi$, we see that MK proves $\neg\Pr_S(\left\ulcorner0\ne0\right\urcorner)$, i.e., $\mathrm{Con}_S$, for every its finite subtheory $S$, such as $S=\mathrm{NBG}$.

The main idea of the proof of $1\to2$ (which goes back to Montague) is that using sequence encoding, one can give partial truth definitions (i.e., truth definitions for any finite set of formulas including their substitution instances). Reasoning within the theory, if $S$ proves $\varphi$, then by the cut-elimination theorem, it has a sequent proof where each formula is a subformula of something in $S$ or $\varphi$. Using a partial truth definition for this finite set of formulas, one proves by induction on the length of proof that all sequents in the proof are true, hence also $\varphi$ holds.


[1] Pavel Pudlák: Cuts, consistency statements and interpretations, Journal of Symbolic Logic 50 (1985), no. 2, pp. 423–441, doi: 10.2307/2274231.

[2] Albert Visser: An overview of interpretability logic, Logic Group Preprint Series vol. 174.

[3] Albert Visser: Pairs, sets and sequences in first order theories, Logic Group Preprint Series vol. 251.

  • $\begingroup$ Apologies, but I'm sure I'm missing something here. This is saying that $T$ proves that if its subtheory $S$ proves $\phi(x)$ (for $x$ natural) then $\phi(x)$ is an actual consequence of $T$. Right? I'm not sure what this gets us. I'm also not sure why ZFC (or NBG) wouldn't get full induction as well, or if they do, I'm still not sure why MK would be special. $\endgroup$ Commented Feb 1, 2012 at 16:52
  • 6
    $\begingroup$ No, it is saying much more: $T$ proves the implication that provability of $\varphi$ in $S$ implies $\varphi$, no matter whether $\varphi$ is actually provable or not. For example, if you take for $\varphi$ a contradiction, then this implication is exactly $\mathrm{Con}_S$. As for induction, ZFC does prove full induction and it is, duly, essentially reflexive. NBG, on the other hand, only proves induction for formulas without class quantifiers. In order to get full induction in an NBG-like theory, you need comprehension for all formulas of the form $x\in\omega\land\varphi(x)$. $\endgroup$ Commented Feb 1, 2012 at 17:02
  • 3
    $\begingroup$ It might sound confusing that ZFC proves full induction, and its extension NBG does not. The point is that there are more formulas in NBG than in ZFC, hence the induction schema is also stronger. $\endgroup$ Commented Feb 1, 2012 at 17:08
  • $\begingroup$ So, if I take $\phi$ to be a contradiction, then there aren't any free variables in $\phi$, and the schema instance states that $T$ proves that $Pr_S(\phi)\rightarrow \phi$; then since $T$ proves $\lnot\phi$, we have $T$ proving $\lnot Pr_S(\phi)$ by contrapositive, which is $T$ proving $Con(S)$. And since NBG is a finitely axiomatizable subtheory of MK, we have MK proving $Con(NBG)$, which then proves $Con(ZFC)$ and $Con(ZF)$, since they are subtheories. Is that the argument? (Again, apologies; I'm new to this branch of logic and it keeps turning me around) $\endgroup$ Commented Feb 1, 2012 at 17:36
  • $\begingroup$ Yes, exactly. I’m sorry if I was too terse, unfortunately I often take for granted things that people with different backgrounds are not familiar with. $\endgroup$ Commented Feb 1, 2012 at 18:02

Concerning the fact that Kelley-Morse set theory proves Con(ZFC) and much more, I wrote a post on my blog explaining one way to do it.

Kelley-Morse implies Con(ZFC) and much more

The basic outline of the proof is to show that KM proves the existence of a class truth predicate Tr for first-order truth (and this is what Andreas also suggests in his answer), and then to prove that this truth predicate decrees that each axiom of ZFC is true. It follows by reflection that there will be rank initial segments $V_\theta$ that has the same satisfaction relation, and so these are transitive models of ZFC, and indeed KM proves that the universe is the union of a closed unbounded elementary tower $$V_{\theta_0}\prec V_{\theta_1}\prec\cdots\prec V_\lambda\prec\cdots\prec V.$$ Alternatively, a more syntactic argument proceeds by observing that the truth predicate is closed under deduction, complete and contains no explicit contradictions, and so it provides a complete consistent extension of ZFC.

Follow the link for the details.

  • $\begingroup$ Joel, perhaps it would have been better to write a synopsis of the blog post, and let people visit your blog for the full detailed proofs? $\endgroup$
    – Asaf Karagila
    Commented Feb 15, 2014 at 6:55
  • $\begingroup$ @AsafKaragila, perhaps you are right. I have edited. $\endgroup$ Commented Feb 15, 2014 at 11:49
  • $\begingroup$ Good! This has the added value that if you decide to modify the proof on the blog, you don't need to edit this post (unless it's something substantial). $\endgroup$
    – Asaf Karagila
    Commented Feb 15, 2014 at 11:50

ZF can describe the set of formulas that are not provable in ZF, but, unless it's inconsistent, it can't prove that that set is non-empty. Mostowski proved that MKM can prove this set is non-empty:

@article{0039.27601, author="Mostowski, Andrzej", title="{Some impredicative definitions in the axiomatic set-theory.}", language="English", journal="Fundam. Math.", volume="37", pages="111-124", year="1950", keywords="{set theory}", }


I have recently constructed a proof of the relative consistency of ZFC with MK using an internal model. For this proof to work, MK is axiomatized over a free predicate logic with descriptions. The idea of the proof is to define within MK new "primitive" notions such as

((x in A) iff (x in A and A in U))

The next step is to prove in MK all of the aioms for ZFC but stated in the new notation.

I would be happy to send you a pdf of the proof.

[email protected]


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.