Morse-Kelley set theory consistency strength

Question

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

Answer 1

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.

Answer 2

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.

References:

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

Answer 3

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.

Answer 4

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}", }

Answer 5

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]