A model of second-order arithmetic satisfying AC but not DC
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.
Models of arithmetic are two-sorted structures, having two types of objects, which we think of as numbers and sets of numbers. Their properties are formalized using a two-sorted logic with separate variables and quantifiers for numbers and sets. By convention, we will denote number variables by lower-case letters and sets variables by upper-case letters. The language of second-order arithmetic is the language of first-order arithmetic $\mathcal L_A=\{+,\cdot,<,0,1\}$ together with a membership relation $\in$ between numbers and sets. A multitude of second-order arithmetic theories, as well as the relationships between them, have been extensively studied (see [1]).
An example of a weak second-order arithmetic theory is ${\rm ACA_0}$, whose axioms consist of the modified Peano axioms, where instead of the induction scheme we have the single second-order induction axiom $$\forall X [(0\in X\wedge \forall n(n\in X\rightarrow n+1\in X))\rightarrow \forall n (n\in X)],$$ and the comprehension scheme for first-order formulas. The latter is a scheme of assertions stating for every first-order formula, possibly with class parameters, that there is a set whose elements are exactly the numbers satisfying the formula. One of the strongest second-order arithmetic theories is ${\rm Z}_2$, often referred to as full second-order arithmetic, which strengthens comprehension for first-order formulas in ${\rm ACA}_0$ to full comprehension for all second-order assertions. This means that for a formula with any number of second-order quantifiers, there is a set whose elements are exactly the numbers satisfying the formula. The reals of any model of ${\rm ZF}$ is a model of ${\rm Z}_2$. We can further strengthen the theory ${\rm Z}_2$ by adding choice principles for sets: the choice scheme and the dependent choice scheme.
The choice scheme is a scheme of assertions, which states for every second-order formula $\varphi(n,X,A)$ with a set parameter $A$ that if for every number $n$, there is a set $X$ witnessing $\varphi(n,X,A)$, then there is a single set $Y$ collecting witnesses for every $n$, in the sense that $\varphi(n,Y_n,A)$ holds, where $Y_n=\{m\mid \langle n,m\rangle\in Y\}$ and $\langle n,m\rangle$ is any standard coding of pairs. More precisely, an instance of the choice scheme for the formula $\varphi(n,X,A)$ is $$\forall n\exists X\varphi(n,X,A)\rightarrow \exists Y\forall n\varphi(n,Y_n,A).$$ We will denote by $\Sigma^1_n$-${\rm AC}$ the fragment of the choice scheme for $\Sigma^1_n$-assertions, making an analogous definition for $\Pi^1_n$, and we will denote the full choice scheme by $\Sigma^1_\infty$-${\rm AC}$. The reals of any model of ${\rm ZF}+{\rm AC}_\omega$ (countable choice) satisfy ${\rm Z}_2+\Sigma^1_\infty$-${\rm AC}$. It is a folklore result, going back possibly to Mostowski, that the theory ${\rm Z}_2+\Sigma^1_\infty$-${\rm AC}$ is bi-interpretable with the theory ${\rm ZFC}^-$ (${\rm ZFC}$ without the powerset axiom, with Collection instead of Replacement) together with the statement that every set is countable.
The dependent choice scheme is a scheme of assertions, which states for every second-order formula $\varphi(X,Y,A)$ with set parameter $A$ that if for every set $X$, there is a set $Y$ witnessing $\varphi(X,Y,A)$, then there is a single set $Z$ making infinitely many dependent choices according to $\varphi$. More precisely, an instance of the dependent choice scheme for the formula $\varphi(X,Y,A)$ is $$\forall X\exists Y\varphi(X,Y,A)\rightarrow \exists Z\forall n\varphi(Z_n,Z_{n+1},A).$$ We will denote by $\Sigma^1_n$-${\rm DC}$ the dependent choice scheme for $\Sigma^1_n$-assertions, with an analogous definition for $\Pi^1_n$, and we will denote the full dependent choice scheme by $\Sigma^1_\infty$-${\rm DC}$. The reals of a model of ${\rm ZF}+{\rm DC}$ (dependent choice) satisfy ${\rm Z}_2+\Sigma^1_\infty$-${\rm DC}$.
It is not difficult to see that the theory ${\rm Z}_2$ implies $\Sigma^1_2$-${\rm AC}$, the choice scheme for $\Sigma^1_2$-assertions. Models of ${\rm Z}_2$ can build their own version of Gödel's constructible universe $L$. If a model of ${\rm Z}_2$ believes that a set $\Gamma$ is a well-order, then it has a set coding a set-theoretic structure constructed like $L$ along the well-order $\Gamma$. It turns out that models of ${\rm Z}_2$ satisfy a version of Shoenfield's absoluteness with respect to their constructible universes. For every $\Sigma^1_2$-assertion $\varphi$, a model of ${\rm Z}_2$ satisfies $\varphi$ if and only its constructible universe satisfies $\varphi$ with set quantifiers naturally interpreted as ranging over the reals. All of the above generalizes to constructible universes $L[A]$ relativized to a set parameter $A$. Thus, given a $\Sigma^1_2$-assertion $\varphi(n,X,A)$ for which the model satisfies $\forall n\exists X\varphi(n,X,A)$, the model can go to its constructible universe $L[A]$ to pick the least witness $X$ for $\varphi(n,X,A)$ for every $n$, because $L[A]$ agrees when $\varphi$ is satisfied, and then put the witnesses together into a single set using comprehension. So long as the unique witnessing set can be obtained for each $n$, comprehension suffices to obtain a single set of witnesses. How much more of the choice scheme follows from ${\rm Z}_2$? The reals of the classical Feferman-Lévy model of ${\rm ZF}$ (see [2], Theorem 8), in which $\aleph_1$ is a countable union of countable sets, is a $\beta$-model of ${\rm Z}_2$ in which $\Pi^1_2$-${\rm AC}$ fails. This is a particulary strong failure of the choice scheme because, as we explain below, $\beta$-models are meant to strongly resemble the full standard model $P(\omega)$.
There are two ways in which a model of second-order arithmetic can resemble the full standard model $P(\omega)$. A model of second-order arithmetic is called an $\omega$-model if its first-order part is $\omega$, and it follows that its second-order part is some subset of $P(\omega)$. But even an $\omega$-model can poorly resemble $P(\omega)$ because it may be wrong about well-foundedness by missing $\omega$-sequences. An $\omega$-model of second-order arithmetic which is correct about well-foundedness is called a $\beta$-model. The reals of any transitive ${\rm ZF}$-model is a $\beta$-model of ${\rm Z}_2$. One advantage to having a $\beta$-model of ${\rm Z}_2$ is that the constructible universe it builds internally is isomorphic to an initial segment $L_\alpha$ of the actual constructible universe $L$.
The theory ${\rm Z}_2$ also implies $\Sigma^1_2$-${\rm DC}$ (see [1], Theorem VII.9.2), the dependent choice scheme for $\Sigma^1_2$-assertions. In this article, we construct a symmetric submodel of a forcing extension of $L$ whose reals form a model of second-order arithmetic in which ${\rm Z}_2$ together with $\Sigma^1_\infty$-${\rm AC}$ holds, but $\Pi^1_2$-${\rm DC}$ fails. The forcing notion we use is a tree iteration of a forcing for adding a real due to Jensen.
Jensen's forcing, which we will call here $\mathbb P^J$, introduced by Jensen in [3], is a subposet of Sacks forcing constructed in $L$ using the $\diamondsuit$ principle. The poset $\mathbb P^J$ has the ccc and adds a unique generic real over $L$. The collection of all $L$-generic reals for $\mathbb P^J$ in any model is $\Pi^1_2$-definable. Jensen used his forcing to show that it is consistent with ${\rm ZFC}$ that there is a $\Sigma^1_3$-definable non-constructible real [3]. Recently Lyubetsky and Kanovei extended the "uniqueness of generic filters" property of Jensen's forcing to finite-support products of $\mathbb P^J$ [4]. They showed that in a forcing extension $L[G]$ by the $\omega$-length finite support-product of $\mathbb P^J$, the only $L$-generic reals for $\mathbb P^J$ are the slices of the generic filter $G$. The result easily extends to $\omega_1$-length finite support-products as well.
We in turn extend the ``uniqueness of generic filters" property to tree iterations of Jensen's forcing. We first define finite iterations $\mathbb P^J_n$ of Jensen's forcing $\mathbb P^J$, and then define an iteration of $\mathbb P^J$ along a tree $\mathcal T$ to be a forcing whose conditions are functions from a finite subtree of $\mathcal T$ into $\bigcup_{n<\omega}\mathbb P_n^J$ such that nodes on level $n$ get mapped to elements of the $n$-length iteration $\mathbb P_n^J$ and conditions on higher nodes extend conditions on lower nodes. The functions are ordered by extension of domain and strengthening on each coordinate. We show that in a forcing extension $L[G]$ by the tree iteration of $\mathbb P^J$ along the tree ${}^{\lt\omega}\omega_1$ (or the tree ${}^{\lt\omega}\omega$) the only $L$-generic filters for $\mathbb P_n^J$ are the restrictions of $G$ to level $n$ nodes of tree. We proceed to construct a symmetric submodel of $L[G]$ which has the tree of $\mathbb P_n^J$-generic filters added by $G$ but no branch through it. The symmetric model we construct satisfies ${\rm AC}_\omega$ and the tree of $\mathbb P_n^J$-generic filters is $\Pi^1_2$-definable in it. The reals of this model thus provide the desired $\beta$-model of ${\rm Z}_2$ in which $\Sigma^1_\infty$-${\rm AC}$ holds, but $\Pi^1_2$-${\rm DC}$ fails.
Our results also answer a long-standing open question of Zarach from [5] about whether the Reflection Principle holds in models of ${\rm ZFC}^-$. The Reflection Principle states that every formula can be reflected to a transitive set, and holds in ${\rm ZFC}$ by the Lévy-Montague reflection because every formula is reflected by some $V_\alpha$. In the absence of the von Neumann hierarchy, it is not clear how to realize reflection, and indeed we show that it fails in $H_{\omega_1}\models{\rm ZFC}^-$ of the symmetric model we construct.
References
- 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.
- 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
- A. M. Zarach, “Replacement $\nrightarrow$ collection,” in Gödel ’96 (Brno, 1996), vol. 6, Berlin: Springer, 1996, pp. 307–322.