Choice schemes for Kelley-Morse set theory

This is a talk at the Colloquium Logicum Conference in Munich, Germany, September 4-6, 2014.
Slides

In first-order ${\rm ZFC}$ set theory, classes are the definable (with parameters) sub-collections of the model. To formalize the possibility of non-definable classes, we need second-order set theory. The syntax of second-order set theory consists of two sorts of variables, one for sets and one for classes, as well as corresponding sorts for quantifiers. The convention is to use uppercase letters for classes and lowercase letters for sets. Semantically, a model of a second-order set theory is a triple $\langle M,\in,S \rangle$, where $M$ is the sets and $S$, consisting of subsets of $M$, is the classes. The two most common axiomatizations of second-order set theory are the Gödel-Bernays axioms (${\rm GBC}$) and Kelley-Morse axioms (${\rm KM}$). The first-order part of both set theories is axiomatized by ${\rm ZFC}$. For classes, both assert that there is a global choice function and that replacement holds, meaning that the range of every class function restricted to a set is a set. The difference lies in their class existence principles, the comprehension schemes. The theory ${\rm GBC}$ restricts class comprehension to first-order formulas (with class parameters), while ${\rm KM}$ has full comprehension for all second-order assertions (see this post). The difference is significant. Every model of ${\rm ZFC}$ with definable classes can be extended to a model of ${\rm GBC}$ (without adding sets) by forcing the existence of a global choice function (see this post). It follows that ${\rm GBC}$ is conservative over ${\rm ZFC}$: every first-order property of sets provable in ${\rm GBC}$ is already provable in ${\rm ZFC}$. The theory ${\rm KM}$ proves that there is a truth predicate for the universe $\langle V,\in \rangle$ and that $V$ is the union of an elementary chain of a sub-collection of its rank initial segments $V_\alpha$. This later property means that the consistency strength of ${\rm KM}$ is above the hierarchy one obtains by iterating the Con operation starting with $\text{Con}({\rm ZFC})$ (see this post of Joel Hamkins). But it is much below an inaccessible cardinal because if $\kappa$ is inaccessible, then $$\langle V_\kappa,\in, V_{\kappa+1}\rangle \models{\rm KM}$$ and therefore there are many models of ${\rm KM}$ already in $V_\kappa$.

Why should one care about non-definable classes or second-order set theory? There are at least two interesting situations that I know where models of second-order set theories arise. The famous Kunen Inconsistency showing that there is no ($\Sigma_1$-) elementary embedding $j:V\to V$ is trivial for definable embeddings. The power of the theorem lies in that it is a statement about embeddings in models of Kelley-Morse set theory and the assertion is that so long as replacement (and choice) holds no class existence principle can yield elementary embeddings from $V$ to $V$ [1]. The other application is to model theory of set theory, where models of set theory with desired properties are often constructed as external ultrapowers of models $\langle M,\in,S\rangle$ of second-order set theory (usually ${\rm GBC}$), whose elements are equivalence classes of functions in $S$ using an ultrafilter on $S$ (see this post). I am also guessing, based on the number of MathOverflow questions I have seen on the topic, that second-order set theory is a good formal setting for working with Conway's surreal numbers (for instance, see here).

${\rm KM}$ is generally considered one of the most powerful second-order set theories, but I will argue that it fails to have two highly desirable properties. Because of the key role ultrapowers play in set theoretic constructions, internal ultrapowers of a model of a robust second-order set theory, whether you consider non-standard ultrapowers on $\omega$ or the well-founded ultrapowers on a measurable $\kappa$, should satisfy the corresponding second-order version of Łoś. In this version, classes of the ultrapower on a set $I$ are represented by coded class functionals $\langle F_i\mid i\in I\rangle$. But this is not the case! Indeed, we show that an ultrapower on $\omega$ of a ${\rm KM}$ model may not even satisfy ${\rm KM}$. Another desirable property is to have second-order complexity classes be closed under first-order quantification, so that there is a normal form for second-order formulas with all the first-order quantifiers grouped to the right. We show that this property too can fail in ${\rm KM}$ models.

Both these properties follow naturally from augmenting ${\rm KM}$ with the full choice scheme, which asserts for every second-order formula $\varphi(x,X)$ (with parameters) that $$\forall x\exists X\varphi(x,X)\rightarrow \exists Z\forall x\varphi(x,Z_x),$$ where $Z_x=\{y\mid (x,y)\in Z\}$ is the slice on coordinate $x$ of $Z$. In words, whenever for every set $x$, there is a class $Y$ witnessing a certain property, the choice scheme provides a class coding a witness for every $x$. The choice scheme has an obvious set-sized variant, where we must bound the first quantifier by some set $a$, and both the class and set-sized variants can be stratified by formula complexity. It is not difficult to see that the Łoś theorem for internal ultarpowers on sets is equivalent to the set-sized choice scheme. It appears that the choice schemes were first studied by Marek and Mostowski in the 1970's. More recently, they have played a role in work on non-standard set theory and in analysis of class forcing extensions (thanks Karel Hrbáček and Carolin Antos for pointing this out).

An analogous version of the choice scheme comes up in second-order arithmetic, a subject that has many fruitful connections with second-order set theory. The two sorts in second-order arithmetic are numbers and sets of numbers. The first-order part of a model of second-order arithmetic is a model of Peano Arithmetic and axiomatizations for the second-order part differ primarily on set existence principles (and for which second-order formulas to allow induction) [2]. The analogues of ${\rm GBC}$ and ${\rm KM}$ in second-order arithmetic are ${\rm ACA}_0$ and $Z_2$: ${\rm ACA}_0$ has comprehension for first-order formulas (with set parameters), while ${\rm Z}_2$ allows full comprehension for any second-order assertion (and induction for all second-order formulas). The choice scheme asserts for every second-order formula $\varphi(n,X)$ (with set parameters) that $$\forall n\exists X\varphi(n,X)\rightarrow \exists Z\forall n\varphi(n,Z_n).$$ The theory ${\rm Z}_2$ proves all $\Sigma_2^1$ instances of the choice scheme ($\varphi$ is $\Sigma_2^1)$. This is because a model of ${\rm Z}_2$ can construct its own $L_\alpha$ hierarchy with respect to which it satisfies Shoenfield's absoluteness theorem that $\Sigma_2^1$ assertions are absolute. Thus, it can choose an $L$-least witness to every $\Sigma_2^1$ assertion $\exists X\varphi(n,X)$. The choice scheme for a $\Pi_2^1$-formula fails in the sets of numbers of the Feferman-Lévy model of ${\rm ZF}$, a classical symmetric model obtained from the ${\rm Coll}(\omega,<\aleph_\omega)$ forcing extension. The model can construct $L_{\aleph_n}$ for every number $n$, but it cannot have one set coding all the $L_{\aleph_n}$ because $L_{\aleph_\omega}$ remains uncountable in the Feferman-Lévy model. An analogous construction to the Feferman-Lévy model, using the ${\rm Coll}(\kappa,\lt\kappa^{+\omega})$ forcing extension for an inaccessible $\kappa$, shows that the choice scheme can fail for a $\Pi_1^1$-formula in a model of ${\rm KM}$ (complexity goes down because checking whether a class codes a well-ordered relation is first-order expressible, while it is $\Pi_1^1$ in second-order arithmetic). But indeed, we show that ${\rm KM}$ fails to prove even instances of the choice scheme restricted to first-order assertions. More specifically, we produce, using forcing, a model of ${\rm KM}$ in which there are $\omega$-many ${\rm ORD}$-trees each of which has a branch, but there is no choice class for the branches.

Finally, let me mention a fascinating (but easily seen) connection between ${\rm KM}$ augmented with the choice scheme, which we call ${\rm KM}^+$, and another favorite interest of mine, the theory ${\rm ZFC}^-$, which is roughly ${\rm ZFC}$ without the powerset axiom (see this post). It has been observed that the theory ${\rm ZFC}^-$ together with the assertion that there is a largest cardinal and it is inaccessible is bi-interpretable with ${\rm KM}^+$ (thanks Ali Enayat for pointing this out). A ${\rm ZFC}^-$ model $M$ having the largest inaccessible cardinal $\kappa$ can be turned into the ${\rm KM}^+$-model $\langle V_\kappa^M, \in, P^M(V_\kappa)\rangle$ and a ${\rm KM}^+$-model $\langle M,\in, S\rangle$ can construct a ${\rm ZFC}^-$-model consisting of all well-founded relations coded in $S$.

This is joint work with Joel David Hamkins.

References

  1. K. Kunen, “Elementary embeddings and infinitary combinatorics,” J. Symbolic Logic, vol. 36, pp. 407–413, 1971.
  2. S. G. Simpson, Subsystems of second order arithmetic, Second. Cambridge University Press, Cambridge; Association for Symbolic Logic, Poughkeepsie, NY, 2009, p. xvi+444.