A model of second-order arithmetic satisfying AC but not DC

  • S. Friedman and V. Gitman, “A model of second-order arithmetic satisfying AC but not DC.” (manuscript under review)  
    @ARTICLE{FriedmanGitman:ModelOfACNotDC,
    author = {Sy-David Friedman and Victoria Gitman},
    title = {A model of second-order arithmetic satisfying {AC} but not {DC}},
    note = {manuscript under review},
    url = {},
    pdf={https://boolesrings.org/victoriagitman/files/2018/03/ModelOfACNotDC.pdf},
    }


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.

[1] [doi] S. G. Simpson, Subsystems of second order arithmetic, Second ed., Cambridge University Press, Cambridge; Association for Symbolic Logic, Poughkeepsie, NY, 2009.
[Bibtex]
@book {simpson:second-orderArithmetic,
AUTHOR = {Simpson, Stephen G.},
TITLE = {Subsystems of second order arithmetic},
SERIES = {Perspectives in Logic},
EDITION = {Second},
PUBLISHER = {Cambridge University Press, Cambridge; Association for
Symbolic Logic, Poughkeepsie, NY},
YEAR = {2009},
PAGES = {xvi+444},
ISBN = {978-0-521-88439-6},
MRCLASS = {03F35 (03-02 03B30)},
MRNUMBER = {2517689 (2010e:03073)},
DOI = {10.1017/CBO9780511581007},
URL = {http://dx.doi.org/10.1017/CBO9780511581007},
}
[2] 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.
[Bibtex]
@incollection {levy:choicescheme,
AUTHOR = {L{\'e}vy, Azriel},
TITLE = {Definability in axiomatic set theory. {II}},
BOOKTITLE = {Mathematical {L}ogic and {F}oundations of {S}et {T}heory
({P}roc. {I}nternat. {C}olloq., {J}erusalem, 1968)},
PAGES = {129--145},
PUBLISHER = {North-Holland, Amsterdam},
YEAR = {1970},
MRCLASS = {02.60},
MRNUMBER = {0268037 (42 \#2936)},
MRREVIEWER = {G. Kreisel},
}
[3] 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.
[Bibtex]
@incollection {jensen:real,
AUTHOR = {Jensen, Ronald},
TITLE = {Definable sets of minimal degree},
BOOKTITLE = {Mathematical logic and foundations of set theory ({P}roc.
{I}nternat. {C}olloq., {J}erusalem, 1968)},
PAGES = {122--128},
PUBLISHER = {North-Holland, Amsterdam},
YEAR = {1970},
MRCLASS = {02K05},
MRNUMBER = {0306002 (46 \#5130)},
MRREVIEWER = {D. A. Martin},
}
[4] V. Kanovei and V. Lyubetsky, “A countable definable set of reals containing no definable elements.”
[Bibtex]
@ARTICLE {kanovei:productOfJensenReals,
AUTHOR = {Kanovei, Vladimir and Lyubetsky, Vassily},
TITLE = {A countable definable set of reals containing no definable elements},
EPRINT ={1408.3901}}
[5] A. M. Zarach, “Replacement $\nrightarrow$ collection,” in Gödel ’96 (Brno, 1996), Berlin: Springer, 1996, vol. 6, pp. 307-322.
[Bibtex]
@incollection {Zarach1996:ReplacmentDoesNotImplyCollection,
AUTHOR = {Zarach, Andrzej M.},
TITLE = {Replacement {$\nrightarrow$} collection},
BOOKTITLE = {G\"odel '96 ({B}rno, 1996)},
SERIES = {Lecture Notes Logic},
VOLUME = {6},
PAGES = {307--322},
PUBLISHER = {Springer},
ADDRESS = {Berlin},
YEAR = {1996},
MRCLASS = {03E30 (03E35)},
MRNUMBER = {1441120 (98g:03120)},
}
This entry was posted in publications and tagged , , , , , , . Bookmark the permalink.

9 Responses to A model of second-order arithmetic satisfying AC but not DC

  1. Ali Enayat says:

    Hi Vika. Do you happen to know whether the technology of your paper can be adapted to also settle the set-theoretic version, i.e., build a model of KM in which Ord-AC holds but ORD-DC does not?

    • Ali, without looking into the details right now, off the bat I’d say that take an inaccessible $\kappa$, then do the standard forcing for the failure of DC while preserving AC at $\kappa$, and you end up with a universe in which $V_{\kappa+1}$ is a model of KM with AC but not DC.

      • Victoria Gitman says:

        Hello Asaf. Yes, this is a natural approach to take, but we tried it for some time and couldn’t get it to work. The standard forcing (which you helped me to understand years ago) adds a tree of Cohen subsets of omega_1, an object that’s too big for a model of second-order arithmetic (a corresponding situation occurs for inaccessible kappa). If you instead try to add a tree of Cohen reals, other nasty issues arise. The argument ultimately ended up being much more complicated. It makes a fundamental use of recent results of Kanovei and Lyubetsky about uniqueness properties of Jensen’s generic reals.

        • But Ali asked about KM, not SOA… 🙂

          • Victoria Gitman says:

            I think all the same obstacles arise for inaccessible kappa. Isn’t the forcing to get AC_kappa to hold but DC_kappa to fail basically the same as for omega?

          • Yes, it’s the same as $\omega$, and I fail to see where would the problem lie in the case of an inaccessible.

          • Victoria Gitman says:

            Asaf, the problem for kappa is the same as for omega. The standard forcing will add a tree of Cohen subsets of kappa^+ and V_kappa+1 cannot see this object.

          • Oh, of course. You’re right.

            So the idea should be to have some iteration that slowly adds a tree inside $V_\kappa$, and then use automorphisms to kill its branches, while preserving global choice in $V_\kappa$.

    • Victoria Gitman says:

      Hello Ali. The original motivation for looking at models of second-order arithmetic was precisely to eventually get at the KM case. We are very optimistic that a generalization of these techniques can be used to show that there is a model of KM in which Ord-AC holds but Ord-DC fails. I am hoping to work out the details soon.

Leave a Reply

Your email address will not be published. Required fields are marked *