## Morse-Kelley set theory consistency strength

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$.

-

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.

-
I believe that all the details of this approach to proving Con(ZFC) in MK are in Mostowski's book "Constructible Sets With Applications". – Andreas Blass Feb 1 2012 at 19:47
Not quite, one also needs to prove that contradictions are not true in the ZFC universe $\hspace{.6 in}$ (which can easily be done). $\:$ – Ricky Demer Feb 1 2012 at 21:09
@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. – Andreas Blass Feb 1 2012 at 23:43

This is an instance of a much more general result. (See Visser 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, see Visser 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.

-
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. – Richard Rast Feb 1 2012 at 16:52
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)$. – Emil Jeřábek Feb 1 2012 at 17:02
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. – Emil Jeřábek Feb 1 2012 at 17:08
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) – Richard Rast Feb 1 2012 at 17:36
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. – Emil Jeřábek Feb 1 2012 at 18:02
show 1 more comment

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.

BobAlps@aol.com

-