I should like to give a brief account of the argument that KM implies Con(ZFC) and much more. This argument is well-known classically, but unfortunately seems not to be covered in several of the common set-theoretic texts.
First, without giving a full formal axiomatization, let us review a little what KM is. (And please see Victoria Gitman’s post on variant axiomatizations of KM.) In contrast to Zermelo-Frankael (ZFC) set theory, which has a purely first-order axiomatization, both Kelley-Morse (KM) set theory and Gödel-Bernays (GBC) set theory are formalized in the second-order language of set theory, where we have two sorts of objects, namely sets and classes, in addition to the usual set membership relation $\in$. A model of KM will have the form $\langle M,{\in^M},S\rangle$, where $M$ is the collection of sets in the model, and $S$ is a collection of classes in the model; each class $A\in S$ is simply the subset of $M$. Both KM and GBC will imply that $\langle M,{\in^M}\rangle$ is a model of ZFC. Both GBC and KM assert the global choice principle, which asserts that there is a class that is a well-ordering of all the sets (or equivalently that there is a class bijection of all the sets with the class of ordinals). Beyond this, both GBC and KM have a class comprehension principle, asserting that for certain formulas $\varphi$, having finitely many set and class parameters, that $\{x \mid \varphi(x)\}$ forms a class. In the case of GBC, we have this axiom only for $\varphi$ having only set quantifiers, but in KM we also allow formulas $\varphi$ that have quantification over classes (which are interpreted in the model by quanfying over $S$). Both theories also assert that the intersection of a class with a set is a set (which amounts to the separation axiom, and this follows from replacement anyway). In addition, both GBC and KM have a replacement axiom, asserting that if $u$ is a set, and for every $a\in u$ there is a unique set $b$ for which $\varphi(a,b)$, where $\varphi$ has finitely many class and set parameters, then $\{ b\mid \exists a\in u\, \varphi(a,b)\}$ is a set. In the case of GBC, we have the replacement axiom only when all the quantifiers of $\varphi$ are first-order quantifiers only, quantifying only over sets, but in KM we allow $\varphi$ to have second-order quantifiers. Thus, both GBC and KM can be thought of as rather direct extensions of ZFC to the second-order class context, but KM goes a bit further by applying the ZFC axioms also in the case of the new second-order properties that become available in that context, while GBC does not.
The theorem I want to discuss is:
Theorem. KM proves Con(ZFC).
Indeed, ultimately we’ll show in KM that there is transitive model of ZFC, and furthermore that the universe $V$ is the union of an elementary chain of elementary rank initial segments $V_\theta\prec V$, each of which, in particular, is a transitive model of ZFC.
We’ll prove it in several steps, which will ultimately reveal stronger results and a general coherent method and idea.
KM has a truth predicate for first-order truth. The first step is to argue in KM that there is a truth predicate Tr for first-order truth, a class of pairs $(\varphi,a)$, where $\varphi$ is a first-order formula in the language of set theory and $a$ is an assignment of the free variabes of $\varphi$ to particular sets, such that the class Tr gets the right answer on the quantifier-free formulas and obeys the recursive Tarskian truth conditions for Boolean combinations and first-order quantification, that is, the conditions explaining how the truth of a formula is determined from the truth of its immediate subformulas.
To construct the truth predicate, begin with the observation that we may easily define, even in ZFC, a truth predicate for quantifier-free truth, and indeed, even first-order $\Sigma_n$ truth is $\Sigma_n$-definable, for any meta-theoretic natural number $n$. In KM, we may consider the set of natural numbers $n$ for which there is a partial truth predicate $T$, one which is defined only for first-order formulas of complexity at most $\Sigma_n$, but which gives the correct answers on the quantifier-free formulas and which obeys the Tarskian conditions up to complexity $\Sigma_n$. The set of such $n$ exists, by the separation axiom of KM, since we can define it by a property in the second-order language (this would not work in GBC, since there is a second-order quantifier asking for the existence of the partial truth predicate). But now we simply observe that the set contains $n=0$, and if it contains $n$, then it contains $n+1$, since from any $\Sigma_n$ partial truth predicate we can define one for $\Sigma_{n+1}$. So by induction, we must have such truth predicates for all natural numbers $n$. This inductive argument really used the power of KM, and cannot in general be carried out in GBC or in ZFC.
A similar argument shows by induction that all these truth predicates must agree with one another, since there can be no least complexity stage where they disagree, as the truth values at that stage are completely determined via the Tarski truth conditions from the earlier stage. So in KM, we have a unique truth predicate defined on all first-order assertions, which has the correct truth values for quantifier-free truth and which obeys the Tarskian truth conditions.
The truth predicate Tr agrees with actual truth on any particular assertion. Since the truth predicate Tr agrees with the actual truth of quantifier-free assertions and obeys the Tarskian truth conditions, it follows by induction in the meta-theory (and so this is a scheme of assertions) that the truth predicate that we have constructed agrees with actual truth for any meta-theoretically finite assertion.
The truth predicate Tr thinks that all the ZFC axioms are all true. Here, we refer not just to the truth of actual ZFC axioms (which Tr asserts as true by the previous paragraph), but to the possibly nonstandard formulas that exist inside our KM universe. We claim nevertheless that all such formulas the correspond to an axiom of ZFC are still decreed true by the predicate Tr. We get all the easy axioms by the previous paragraph, since those axioms are true under KM. It remains only to verify that Tr asserts as true all instances of the replacement axiom. For this, suppose that there is a set $u$, such that Tr thinks every $a\in u$ has a unique $b$ for which Tr thinks $\varphi(a,b)$. But now by KM (actually we need only GB here), we may apply the replacement axiom with Tr a predicate, to find that $\{ b\mid \exists a\in u\, \text{Tr thinks that} \varphi(a,b)\}$ is a set, whether or not $\varphi$ is an actual finite length formula in the metatheory. It follows that Tr will assert this instance of replacement, and so Tr will decree all instances of replacement as being true.
KM produces a closed unbounded tower of transitive models of ZFC. This is the semantic approach, which realizes the universe as the union of an elementary chain of elementary substructures $V_\theta$. Namely, by the reflection theorem, there is a closed unbounded class of ordinals $\theta$ such that $\langle V_\theta,{\in},\text{Tr}\cap V_\theta\rangle\prec_{\Sigma_1}\langle V,{\in},\text{Tr}\rangle$. (We could have used $\Sigma_2$ or $\Sigma_{17}$ here just as well.) It follows that $\text{Tr}\cap V_\theta$ fulfills the Tarskian truth conditions on the structure $\langle V_\theta,\in\rangle$, and therefore agrees with the satisfaction in that structure. It follows that $V_\theta\prec V$ for first-order truth, and since ZFC was part of what is asserted by Tr, we have produced here a transitive model of ZFC. More than this, what we have is a closed unbounded class of ordinals $\theta$, which form an elementary chain $$V_{\theta_0}\prec V_{\theta_1}\prec\cdots\prec V_\lambda\prec\cdots,$$ whose union is the entire universe. Each set in this chain is a transitive model of ZFC and much more.
An alternative syntactic approach. We could alternatively have reasoned directly with the truth predicate as follows. First, the truth predicate is complete, and contains no contradictions, simply because part of the Tarskian truth conditions are that $\neg\varphi$ is true according to Tr if and only if $\varphi$ is not true according to Tr, and this prevents explicit contradictions from ever becoming true in Tr, while also ensuring completeness. Secondly, the truth predicate is closed under deduction, by a simple induction on the length of the proof. One must verify that certain logical validities are decreed true by Tr, and then it follows easily from the truth conditions that Tr is closed under modus ponens. The conclusion is that the theory asserted by Tr contains ZFC and is consistent, so Con(ZFC) holds. Even though Tr is a proper class, the set of sentences it thinks are true is a complete consistent extension of ZFC, and so Con(ZFC) holds. QED
The argument already shows much more than merely Con(ZFC), for we have produced a proper class length elementary tower of transitive models of ZFC. But it generalizes even further, for example, by accommodating class parameters. For any class $A$, we can construct in the same way a truth predicate $\text{Tr}_A$ for truth in the first-order language of set theory augmented with a predicate for the class $A$.
In particular, KM proves that there is a truth predicate for truth-about-truth, that is, for truth-about-Tr, and for truth-about-truth-about-truth, and so on, iterating quite a long way. (Of course, this was also clear directly from the elementary tower of transitive models.)
The elementary tower of transitive elementary rank initial segments $V_\theta\prec V$ surely addresses what is often seen as an irritating limitation of the usual reflection theorem in ZFC, that one gets only $\Sigma_n$-reflection $V_\theta\prec_{\Sigma_n} V$ rather than this kind of full reflection, which is what one really wants in a reflection theorem. The point is that in KM we are able to refer to our first-order truth predicate Tr and overcome that restriction.
Doesn’t the existence of a truth predicate violate Tarski’s theorem on the non-definability of truth? No, not here, since the truth predicate Tr is not definable in the first-order language of set theory. Tarski’s theorem asserts that there can be no definable class (even definable with set parameters) that agrees with actual truth on quantifier-free assertions and which satisfies the recursive Tarskian truth conditions. But nothing prevents having some non-definable class that is such a truth predicate, and that is our situation here in KM.
Although the arguments here show that KM is strictly stronger than ZFC in consistency strength, it is not really very much stronger, since if $\kappa$ is an inaccessible cardinal, then it is not difficult to argue in ZFC that $\langle V_\kappa,\in,V_{\kappa+1}\rangle$ is a model of KM. Indeed, there will be many smaller models of KM, and so the consistency strength of KM lies strictly between that of ZFC, above much of the iterated consistency hierarchy, but below that of ZFC plus an inaccessible cardinal.