# 2017 seminar talk: A model of second-order arithmetic with the choice scheme in which $\Pi^1_2$-dependent choice fails

Talk held by Victoria Gitman (CUNY Graduate Center, New York, USA) at the KGRC seminar on 2017-05-18.

### Abstract

In second-order arithmetic, the *choice scheme* is the scheme of assertions,
for every second-order formula $\varphi(n,X,A)$, that if for every $n$
there is a set $X$ such that $\varphi(n,X,A)$ holds, then there is a
single set $Y$ whose $n$-th slice $Y_n$ witnesses $\varphi(n,Y_n,A)$. While
full second-order arithmetic ${\textrm Z}_2$ implies the choice scheme
for $\Sigma^1_2$-assertions, the reals of the Feferman-Lévy model
form a model of ${\textrm Z}_2$ in which $\Pi^1_2$-choice fails. The *dependent choice scheme*
is the analogue ${\textrm DC}$ for second-order arithmetic and it asserts,
for every second-order formula $\varphi(X,Y,A)$, that if for every set $X$
there is another set $Y$ such that $\varphi(X,Y,A)$ holds, then there is
a single set $Z$, viewed as an $\omega$-sequence of sets, such that for
every $n$, $\varphi(Z\restrict n,Z_n,A)$ holds. The theory ${\textrm Z}_2$
implies $\Sigma^1_2$-dependent choice, and Simpson has conjectured that
there is a model of ${\textrm Z}_2$ with the choice scheme in which $\Pi^1_2$-dependent
choice fails. We prove Simpson's conjecture by constructing a symmetric submodel
of a forcing extension in which ${\textrm AC}_\omega$ holds, but ${\textrm DC}$ fails
for a $\Pi^1_2$-definable relation on the reals.

We force over $L$ with a tree iteration of Jensen's forcing (a ccc subposet of Sacks forcing adding a unique generic real) along the tree ${}^{\lt\omega}\omega_1$, adding a tree, isomorphic to ${}^{\lt\omega}\omega_1$, of finite sequences of reals ordered by extension, such that that the sequences on level $n$ are $L$-generic for the $n$-length iteration of Jensen's forcing. We extend the uniqueness of generic reals properties of Jensen's forcing (obtained earlier by Jensen and later by Lyubetsky and Kanovei) by showing that in the tree iteration extension, the only sequences of reals $L$-generic for the $n$-length iteration of Jensen's forcing are those explicitly added on level $n$ of the generic tree. The uniqueness property implies that the generic tree is $\Pi^1_2$-definable.

The theorem arose out of our attempts to separate the analogues of the choice scheme and the dependent choice scheme over Kelley-Morse set theory, and we conjecture that an appropriate generalization of our arguments will now achieve this result.

This is joint work with Sy-David Friedman.