Class choice and the surprising weakness of Kelley-Morse set theory

TL;DR

This paper reveals that Kelley-Morse set theory (KM) is weaker than commonly believed, lacking several principles like class choice and Łoś theorem, but these can be recovered by augmenting KM with the class choice scheme to form KM+.

Contribution

The paper demonstrates the limitations of KM and introduces KM+ as a stronger, more robust second-order set theory by adding the class choice scheme.

Findings

KM does not prove the class choice scheme.

KM fails Łoś theorem for internal ultrapowers.

KM does not preserve $oldsymbol{orall ext{quantifier invariance}}$ for $oldsymbol{ ext{Σ}^1_n}$ formulas.

Abstract

Kelley-Morse set theory KM is weaker than generally supposed and fails to prove several principles that may be desirable in a foundational second-order set theory. Even though KM includes the global choice principle, for example, (i) KM does not prove the class choice scheme, asserting that whenever every set $x$ admits a class $X$ with $\varphi(x,X)$, then there is a class $Z\subseteq V\times V$ for which $\varphi(x,Z_x)$ on every section. This scheme can fail with KM even in low-complexity first-order instances $\varphi$ and even when only a set of indices $x$ are relevant. For closely related reasons, (ii) the theory KM does not prove the {\L}o\'s theorem scheme for internal second-order ultrapowers, even for large cardinal ultrapowers, such as the ultrapower by a normal measure on a measurable cardinal. Indeed, the theory KM itself is not generally preserved by internal ultrapowers. Finally, (iii) KM does not prove that the $\Sigma^1_n$ logical complexity is invariant under first-order quantifiers, even bounded first-order quantifiers. For example, $\forall \alpha{<}\delta\ \psi(\alpha,X)$ is not always provably equivalent to a $\Sigma^1_1$ assertion when $\psi$ is. Nevertheless, these various weaknesses in KM are addressed by augmenting it with the class choice scheme, thereby forming the theory KM+, which we propose as a robust KM alternative for the foundations of second-order set theory.