Jensen forcing at an inaccessible and a model of Kelley-Morse satisfying ${\rm CC}$ but not ${\rm DC}_\omega$
S.-D. Friedman and V. Gitman, “Jensen forcing at an inaccessible and a model of Kelley-Morse satisfying ${\rm CC}$ but not ${\rm DC}_ω$,” Manuscript, 2023.
Second-order set theory has two types of objects: sets and classes. Unlike in first-order set theory, where classes are relegated to the meta-theory, in second-order set theory we are able to formally study properties of classes. Second-order set theory is formalized in a two-sorted logic with separate sorts (variables and quantifiers) for sets and classes. To distinguish between the two types of objects, we will use lower case letters for sets and upper case letters for classes. Complexity of formulas in second-order set theory is determined by the number of alternations of class quantifiers. A second-order formula is $\Sigma^1_n$ (or $\Pi^1_n$) if it has the form an alternation of $n$ class quantifiers followed by a first-order formula. A model of second-order set theory is a triple $\mathscr V=(V,\in, \mathcal C)$, where $V$ consists of the sets, $\mathcal C$ consists of the classes, and $\in$ is the membership relation between sets and between sets and classes. Each element of $\mathcal C$ is viewed as a sub-collection of $V$ consisting of those elements which are $\in$-related to it. An axiomatization for second-order set theory consists of axioms for sets, classes, and the interactions between the two sorts. A typical axiomatization consists of the basic axioms: ${\rm ZFC}$ axioms for sets, extensionality for classes, the class replacement axiom asserting that every class function restricted to a set is a set, the global well-order axiom asserting that there is a class well-ordering of all sets, together with some class existence axioms. The most common class existence axioms take the form of comprehension axioms, asserting that collections defined by formulas of some complexity are classes. One of the weakest second-order axiomatizations is the theory ${\rm GBC}$, which consists of the above mentioned basic axioms together with comprehension for first-order formulas. The theory ${\rm GBC}$ is equiconsistent with ${\rm ZFC}$ because every model of ${\rm ZFC}$ that has a definable global well-order (such as the constructible universe $L$), when taken together with its definable collections, is a model of ${\rm GBC}$. We get increasingly stronger second-order theories by extending the amount of available comprehension to formulas of higher complexity. This hierarchy of theories culminates in the theory Kelley-Morse ${\rm KM}$, which consists of the basic axioms together with comprehension for all second-order formulas. The theory ${\rm KM}$ has consistency strength greater than ${\rm ZFC}$, but less than ${\rm ZFC}$ with the existence of an inaccessible cardinal.
Although, in terms of comprehension, ${\rm KM}$ is the strongest possible second-order theory, it can be made much more robust by adding choice axioms for classes. Analogously to how sets have much more structure in models of ${\rm ZFC}$ than in models of ${\rm ZF}$, classes have much more structure in models of ${\rm KM}$ together with class choice axioms than they do in models of just ${\rm KM}$. The two most common choice principles used in the second-order context are the choice scheme ${\rm CC}$ and the dependent choice schemes ${\rm DC}_\alpha$ (for a regular cardinal $\alpha$ or $\alpha={\rm Ord}$). The choice scheme asserts for every second-order formula $\varphi(x,X,A)$, with parameter $A$, that if for every set $x$, there is a class $X$ such that $\varphi(x,X,A)$ holds, then there is a single class $Y$ collecting on its slices witnesses for every set $x$, namely, for every set $x$, $\varphi(x,Y_x,A)$ holds, where $Y_x=\{y\mid \langle x,y\rangle\in Y\}$ is the $x$'s slice of $Y$. Given a regular cardinal $\alpha$ or $\alpha={\rm Ord}$, the dependent choice scheme ${\rm DC}_\alpha$ asserts for every second-order formula $\psi(X,Y,A)$, with parameter $A$, that if $\psi$ defines a relation without terminal nodes (for every class $X$, there is a class $Y$ such that $\psi(X,Y,A)$ holds), then we can make $\alpha$-many dependent choices along $\psi$, namely, there is a class $F$ such that for every $\xi\lt\alpha$, $\psi(F\upharpoonright\xi, F_\xi,A)$ holds, where $F_\xi$ is the $\xi$-th slice of $F$ and $F\upharpoonright\xi$ is the restriction of the class $F$ to slices indexed by ordinals $\eta\lt\xi$ ($F\upharpoonright \xi=\{\langle \eta,y\rangle\in F\mid \eta\lt\xi\}$). The choice scheme is viewed as the analogue of ${\rm AC}$ for classes and the ${\rm DC}_\alpha$-scheme is viewed as the analogue of dependent choice ${\rm DC}_\alpha$. The second author and Hamkins showed that the theory ${\rm KM}$ is not strong enough to prove even the weakest instances of the choice scheme, those where we make only $\omega$-many choices for a first-order formula. That is, it is consistent that there is a model of ${\rm KM}$ and a first-order assertion $\varphi(x,X)$ such that in the model, for every $n\in\omega$, there is a class $X$ such that $\varphi(n,X)$ holds, but there is no class $Y$ such that $\varphi(n,Y_n)$ holds for every $n\in\omega$ [1]. Given this situation, the next natural question which arises is whether the theory Kelley-Morse together with the choice scheme ${\rm KM}+{\rm CC}$ proves ${\rm DC}_\omega$, the weakest of the dependent choice principles. The axiom of choice ${\rm AC}$, of course, implies all the dependent choice axioms ${\rm DC}_\alpha$ over ${\rm ZF}$, but results from second-order arithmetic suggested that ${\rm KM}+{\rm CC}$ may not be able to prove at least some of the dependent choice principles ${\rm DC}_\alpha$. The study of the two fields has shown that there are many parallels as well as some differences between these mathematical domains, with second-order arithmetic being the more well-developed of the two because of its connections to analysis.
Second-order arithmetic has two types of objects: numbers and sets of numbers (which we think of as the reals). A typical axiomatization of second-order arithmetic consists of the basic axioms: the ${\rm PA}$ axioms for numbers and the set induction axiom asserting that induction holds for every set, together with some set existence axioms. The primary set existence axioms are again comprehension axioms and choice principles for sets. The choice scheme ${\rm CC}$, in this context, is the exact analogue of the choice scheme in second-order set theory and the dependent choice scheme ${\rm DC}$ is the exact analogue of ${\rm DC}_\omega$. The analogue of ${\rm GBC}$ is the second-order arithmetic theory ${\rm ACA}_0$, which is equiconsistent with ${\rm PA}$, and the analogue of ${\rm KM}$ is the theory ${\rm Z}_2$, which has comprehension for all second-order formulas. An argument, using Shoenfield absoluteness, shows that ${\rm Z}_2$ implies ${\rm CC}$ for $\Sigma^1_2$-formulas (note the contrast with the ${\rm KM}$ situation, where ${\rm KM}$ does not prove ${\rm CC}$ even for first-order formulas) and that ${\rm Z}_2+{\rm CC}$ implies ${\rm DC}$ for $\Sigma^1_2$-formulas [2]. Feferman and Levy constructed a model of ${\rm ZF}$ in which $\omega_1$ is a countable union of countable sets as a symmetric submodel of a forcing extension by the finite-support product $\Pi_{n\lt\omega}{\rm Coll}(\omega,\aleph_n)$ of collapse forcings [3]. The reals of this classical choiceless model form a model of ${\rm Z}_2$ in which ${\rm CC}$ optimally fails for a $\Pi^1_2$-assertion. The authors of the present article, together with Kanovei, showed that it is consistent that there is a model of ${\rm Z}_2+{\rm CC}$ in which ${\rm DC}$ fails for a $\Pi^1_2$-assertion. The model was obtained as the reals of a symmetric submodel of a forcing extension by a tree iteration of Jensen's forcing [4].
Jensen's forcing $\mathbb J$ is a subposet of Sacks forcing that was constructed by Jensen in $L$ using the guessing principle $\diamondsuit$. The forcing $\mathbb J$ has two key properties: it has the ccc and it adds a unique ($\Pi^1_2$-singleton) generic real over $L$. Jensen used the forcing $\mathbb J$ to show that it is consistent to have a $\Pi^1_2$-singleton non-constructible real (every $\Sigma^1_2$-singleton is in $L$ by Shoenfield's absoluteness) [5]. Since then his forcing has found a number of other applications. While $\diamondsuit$ is crucial to the construction of a poset with the two key properties of $\mathbb J$, the constructible universe is not. A subposet of Sacks forcing with the ccc that adds a unique generic real can be constructed in any universe with $\diamondsuit$, with only the complexity of the generic real possibly being lost.
Lyubetsky and Kanovei extended the "unique generics" property of Jensen's forcing to a finite-support $\omega$-length product $\mathbb J^{\lt\omega}$ of $\mathbb J$. They showed that in any forcing extension $L[G]$ by $\mathbb J^{\lt\omega}$, the only generic reals for $\mathbb J$ are those added by the slices of $G$ [6]. Abraham showed that, for $n\lt\omega$, a finite $n$-length iteration $\mathbb J_n$ of $\mathbb J$ adds a unique $n$-length generic sequence of reals (missing reference). The authors of the current article and Kanovei showed that certain tree iterations of $\mathbb J$ have a "unique generics" property, and this property was instrumental in obtaining the model of second-order arithmetic satisfying ${\rm AC}$ but not ${\rm DC}$.
In this paper, we generalize Jensen's construction from $\omega$ to an inaccessible cardinal $\kappa$ to define an analogue of Jensen's forcing with perfect $\kappa$-trees. We show that if $\kappa$ is an inaccessible cardinal and the guessing principle $\diamondsuit_{\kappa^+}(\mathrm{Cof}(\kappa))$ holds, then there is a poset $\mathbb J(\kappa)$, whose elements are perfect $\kappa$-trees ordered by the subset relation, with the three key properties: it is $\lt\kappa$-closed, it has the $\kappa^+$-cc, and it adds a unique generic subset of $\kappa$. A number of obstacles needed to be overcome to make Jensen's construction work for perfect $\kappa$-trees. Perfect trees have several nice properties properties, like the existence of greatest lower bounds for compatible conditions, which fail for perfect $\kappa$-trees, and these properties played a significant role in the construction of Jensen's forcing. Another problem which did not arise in the original construction was presented by the $\lt\kappa$-closure requirement. The poset $\mathbb J$ is built up as the union of a continuous chain of posets of length $\omega_1$ with maximal antichains being sealed at stages given by $\diamondsuit$ along the way. In the case of the poset $\mathbb J(\kappa)$, we couldn't simply take unions at the limit stages of building up the analogous chain because then we would lose $\lt\kappa$-closure, but closing the union under $\lt\kappa$-sequences could potentially unseal maximal antichains. We shall argue that this doesn't happen. We also define finite iterations and tree iterations of the poset $\mathbb J(\kappa)$ partially analogously to how finite iterations $\mathbb J_n$ and tree iterations of $\mathbb J$ were defined in [4].
We show that bounded-support $\kappa$-length products of $\mathbb J(\kappa)$, finite iterations of $\mathbb J(\kappa)$, and certain tree iterations of $\mathbb J(\kappa)$ have "unique generics" properties analogous to those of Jensen's forcing.
Theorem: Suppose that $\kappa$ is an inaccessible cardinal and $\diamondsuit_{\kappa^+}(\mathrm{Cof}(\kappa))$ holds. There is a poset $\mathbb J(\kappa)$ whose elements are perfect $\kappa$-trees ordered by the subset relation with the following three properties:- $\mathbb J(\kappa)$ is $\lt\kappa$-closed.
- $\mathbb J(\kappa)$ has the $\kappa^+$-cc.
- In any forcing extension by $\mathbb J(\kappa)$, there is a unique generic subset of $\kappa$. If the starting universe is $L$, then the unique generic subset is a $\Pi^1_1$-singleton.
Let $\mathbb J(\kappa)^{\lt\kappa}$ denote the bounded-support $\kappa$-length product of the poset $\mathbb J(\kappa)$ and let $\mathbb J(\kappa)_n$, for $n\lt\omega$, denote the $n$-length iteration of $\mathbb J(\kappa)$.
Theorem: Suppose that $\kappa$ is an inaccessible cardinal and $\diamondsuit_{\kappa^+}(\mathrm{Cof}(\kappa))$ holds. In a forcing extension $V[G]$ by $\mathbb J(\kappa)^{\lt\kappa}$, the only generic subsets of $\kappa$ for $\mathbb J(\kappa)$ are those added by the slices of $G$.
Theorem: Suppose that $\kappa$ is an inaccessible cardinal, $\diamondsuit_{\kappa^+}(\mathrm{Cof}(\kappa))$ holds, and $n\in\omega$. The iteration $\mathbb J(\kappa)_n$ of the poset $\mathbb J(\kappa)$ of length $n$ adds a unique $n$-length generic sequence of subsets of $\kappa$.
Theorem: Suppose that $\kappa$ is an inaccessible cardinal and $\diamondsuit_{\kappa^+}(\mathrm{Cof}(\kappa))$ holds. In any forcing extension by the tree iteration of $\mathbb J(\kappa)$ along the tree $(\kappa^+)^{\lt\omega}$, for every $n\in\omega$, the only $n$-length generic sequences of subsets of $\kappa$ for the iteration $\mathbb J(\kappa)_n$ are those arising from the $n$-length nodes of the generic tree.
We construct a symmetric submodel of a forcing extension by the tree iteration of $\mathbb J(\kappa)$ along the tree $(\kappa^+)^{\lt\omega}$ such that in this model $\mathscr V=(V_\kappa,\in, V_{\kappa+1})$ is a model of ${\rm KM}+{\rm CC}$ in which the scheme ${\rm DC}_\omega$ fails.
Theorem: It is consistent that there is a model of ${\rm KM}+{\rm CC}+\neg{\rm DC}_\omega$.
References
- V. Gitman and J. D. Hamkins, “Kelley-Morse set theory and choice principles for classes.”
- S. G. Simpson, Subsystems of second order arithmetic, Second. Cambridge University Press, Cambridge; Association for Symbolic Logic, Poughkeepsie, NY, 2009, p. xvi+444.
- A. Lévy, “Definability in axiomatic set theory. II,” in Mathematical Logic and Foundations of Set Theory (Proc. Internat. Colloq., Jerusalem, 1968), North-Holland, Amsterdam, 1970, pp. 129–145.
- S.-D. Friedman, V. Gitman, and V. Kanovei, “A model of second-order arithmetic satisfying AC but not DC,” J. Math. Log., vol. 19, no. 1, pp. 1850013, 39, 2019.
- R. Jensen, “Definable sets of minimal degree,” in Mathematical logic and foundations of set theory (Proc. Internat. Colloq., Jerusalem, 1968), North-Holland, Amsterdam, 1970, pp. 122–128.
- V. G. Kanovei and V. A. Lyubetski, “A definable countable set containing no definable elements,” Mat. Zametki, vol. 102, no. 3, pp. 369–382, 2017. Available at: https://doi.org/10.4213/mzm10842