A version of Jensen's forcing for an inaccessible cardinal

Jensen's forcing is a subposet of Sacks forcing with two key properties (1) it has the ccc and (2) it adds a unique generic real. Another ccc forcing adding a generic real is, of course, Cohen's original forcing, but, as is well known, once you have added a Cohen generic, you have actually added continuum many of them, so no uniqueness is to be had there. Unlike Cohen's forcing, you cannot construct Jensen's forcing in any universe $V$, you need the guessing principle $\diamondsuit$, so, in particular, you are stuck with universes satisfying ${\rm CH}$. Although, in $L$, we can specify a unique Jensen's forcing, as we will see later, there is are variables in the construction that can result in different forcing notions, all with the required two properties. We will refer to any forcing constructed according to the recipe of Jensen's forcing (which we will sketch below) as $\mathbb J$. As the name suggests, the forcing $\mathbb J$ was discovered by Jensen in 1970, who used it to show that it is consistent to have a $\Pi^1_2$-definable non-constructible (sigleton) real [1]. Namely, you force with $\mathbb J$ over $L$, adding the unique generic real $r$ and argue that in $L[r]$, the singleton $\{r\}$ is $\Pi^1_2$-definable. This is the best possible result because, by Shoenfield's Absoluteness, every $\Sigma^1_2$-definable real has to be in $L$.

More recently, Lyubetsky and Kanovei generalized the 'uniqueness of generic reals' property of Jensen's forcing to finite support $\omega$-length products of $\mathbb J$, showing that in a forcing extension by the finite support $\omega$-length product of $\mathbb J$, the only generic reals for $\mathbb J$ are the $\omega$-many slices of the generic filter [2]. Lyubetsky and Kanovei used their result to show that there can be a countable hereditarily ordinal definable set of reals without any definable members, namely the set consisting of the $\omega$-many generic reals in a forcing extension by the finite-support $\omega$-length product of $\mathbb J$. This answered a question posed on Math Overflow that the set theory community found quite exciting.

Together with Sy Friedman, we defined the notion of 'finite iterations' $\mathbb J_n$ (of length $n$) of Jensen's forcing, for $n\lt\omega$, and showed that these too have unique generics. This notion is a bit more complicated than simply forcing with a name for a forcing constructed according to Jensen's recipe in the extension, because in order to ensure uniqueness we have to be more careful about what goes into the forcing. For such a carefully constructed finite iteration $\mathbb J_n$, there is a unique $n$-length sequence of generic reals. The uniqueness property for the finite iterations $\mathbb J_n$ comes out of a more complicated result about tree iterations of Jensen's forcing. Given a tree $\mathcal T$ of height $\omega$, such as say $\omega^{\lt\omega}$ or $\omega_1^{\lt\omega}$, we define that a condition in the iteration $\mathbb J_{\mathcal T}$ of Jensen's forcing along the tree $\mathcal T$ is a function $f$ from a finite subtree $T$ of $\mathcal T$ into $\bigcup_{n\lt\omega}\mathbb J_n$ such that for a node $s$ of length $n$ in $T$, $f(s)\in \mathbb J_n$ and having the coherence property that whenever $s\lt$ are nodes in $T$, then $f(t)$ restricted to the length of $s$ is equal to $f(s)$. Forcing with $\mathbb J_{\mathcal T}$ adds a tree whose nodes on level $n$ are (mutually) generic for $\mathbb J_n$. The uniqueness property is that in a forcing extension by $\mathbb J_{\mathcal T}$, the only finite sequences of reals that are generic for $\mathbb J_n$ are those coming from the nodes on level $n$ of the generic tree.

We showed (with Kanovei) that a forcing extension of $L$ by the tree iteration $\mathbb J_{\omega_1^{\lt\omega}}$ has a symmetric submodel in which ${\rm AC}_\omega$ holds, but ${\rm DC}$ fails [3]. The symmetric model has the tree of the generic sequences for $\mathbb J_n$ but it doesn't have a branch through it, witnessing a violation of ${\rm DC}$. Moreover, the violation of ${\rm DC}$ is definable over $H_{\omega_1}$ of the symmetric submodel because we can express what it means for a sequence to be $L$-generic for $\mathbb J_n$ and the ordering on the sequences in the tree is just end-extension. It follows that the model of full second-order arithmetic (satisfying comprehension for all second-order definable assertions) consisting of the reals of the symmetric submodel satisfies the Choice Scheme, but not the Dependent Choice Scheme. The Choice Scheme and the Dependent Choice Scheme are choice principles for classes in the second-order context. The Choice Scheme asserts for any second-order formula $\varphi(n,X)$ that if for every number $n$, there is a class $X$ satisfying $\varphi(n,X)$, then there is a single class $Z$ coding a witness for $n$ on its $n$-th slice $Z_n$. The Dependent Choice scheme asserts that we can make $\omega$-many dependent choices over any second-order definable relation $\varphi(X,Y)$ on classes which doesn't have terminal nodes. It also shows that there is a model of ${\rm ZFC}^-$ (${\rm ZFC}$ without powerset), namely the $H_{\omega_1}$ of the symmetric submodel, in which the ${\rm DC}_\omega$-scheme fails. In first-order, the ${\rm DC}_{\alpha}$-scheme, for a regular cardinal $\alpha$, is a strengthening of ${\rm DC}_\alpha$, which asserts that we can make $\alpha$-many dependent choices over any definable relation without terminal nodes. It is easy to see that having powerset implies that the ${\rm DC}_\alpha$-scheme holds for every regular $\alpha$ by reflecting the relation to a large enough $V_\beta$.

Jensen's forcing is a subposet of Sacks forcing, so its elements are perfect trees ordered by the subtree relation. So what is the recipe for constructing Jensen's forcing? The construction is certainly not straightforward. We construct a continuous chain of countable subposets $\mathbb J_\xi$ of Sacks forcing, for $\xi\lt\omega_1$, in $\omega_1$-many steps, using $\diamondsuit$ to seal maximal antichains and have $\mathbb J$ be the union of the chain. Along the way, a $\diamondsuit$-sequence gives us codes for 'nice' countable transitive models $M_\xi$ containing $\mathbb J_\xi$ and we force over $M_\xi$ to add an $M_\xi$-generic perfect tree, which together with $\mathbb J_\xi$ generates $\mathbb J_{\xi+1}$. Generic filters for the models $M_\xi$ exist in $V$ itself because the models are countable. The choice of the $\diamondsuit$-sequence and of the generic filters for the models $M_\xi$ can yield different posets $\mathbb J$ but each will have the required two properties. An extension $V[r]$ by $\mathbb J$ continues to satisfy $\diamondsuit$ because $\mathbb J$ is ccc. So we can construct in $V[r]$, a $\mathbb J$-like forcing following the same recipe. However, in order to construct the iterations $\mathbb J_n$, we don't use just any such forcing. In constructing the $\mathbb J$-like forcings in $V[r]$, we use forcing extensions of models $M_\xi$ chosen by the $\diamondsuit$-sequence from $V$.

The original project of constructing a model of full second-order arithmetic with the Choice Scheme in which the Dependent Choice scheme fails was motivated by an analogous question in second-order set theory. The second-order set theory Kelley-Morse is considered to be one of the strongest second-order theories because it includes comprehension for all second-order assertions. But it turns out that classes in second-order set theory behave much nicer if the theory also includes choice principles for them. Think about how much nicer it is to work in ${\rm ZFC}$ instead of ${\rm ZF}$ (not that there is anything wrong with ${\rm ZF}$, things just get much messier there). Among these useful choice principles for classes are the Choice Scheme and the $\alpha$-Dependent Choice schemes ($\alpha\in{\rm REG}$ or $\alpha={\rm Ord}$) and these basically generalize their second-order arithmetic counterparts. The Choice Scheme asserts for every for second-order formula $\varphi(x,X)$ that if for every set $x$, there is a class $X$ witnessing $\varphi(x,X)$, then there is a single class $Z$ coding a witness for $x$ on its $x$-th slice $Z_x$. The $\alpha$-Dependent Choice Scheme asserts that we can make $\alpha$-many dependent choices over any second-order definable relation on classes without terminal nodes. We showed with Joel Hamkins that Kelley-Morse does not prove the Choice Scheme even for first-order formulas and just $\omega$-many choices [4]. The next question which arose was whether Kelley-Morse together with the Choice Scheme proved the $\omega$-Dependent Choice Scheme. The best way to start answering a question in second-order set theory is to search for its analogue in second-order arithmetic, where a great deal more work was done over the years. But it seemed that the analogous question in second-order arithmetic was not known! Simpson had claimed that full second-order arithmetic together with the Choice Scheme did not prove the Dependent Choice Scheme, but the proof appeared to be lost years ago. So Sy and I set out to prove it by generalizing the work of Lyubetsky and Kanovei on the uniqueness properties of products of $\mathbb J$ to tree iterations. It then turned out that Kanovei had already proved the result decades ago using (what else?) Jensen's forcing with a slightly different construction. So we ended up with a joint paper.

Now the task remained to generalize the construction to obtain the desired result in second-order set theory. The agenda was to get an analogue of Jensen's forcing on an inaccesible cardinal $\kappa$, obtain a uniqueness property for some form of tree iterations of it, and force with the tree iteration over $L$ to obtain a symmetric submodel which had the tree of height $\omega$ of finite sequences generic for iterations of the inaccessible Jensen's forcing, but had no branch through the tree. The $V_\kappa$ of this model was going to be the $V_\kappa$ of $L$, and it together with its subsets in the symmetric submodel would be the desired model of Kelley-Morse with the Choice Scheme in which the $\omega$-Depedent Choice Scheme failed.

There were two obstacles to generalizing the $\mathbb J$ construction to an inaccessible cardinal $\kappa$. The first was that perfect $\kappa$-trees do not behave as nicely as perfect trees because of the limit levels business. For instance, a union of perfect trees is a perfect tree, but a union of perfect $\kappa$-trees need not be a perfect $\kappa$-tree. Another nice property of perfect trees is that if any two of them are compatible, that is there is a perfect tree in their intersection, then there is a maximal such perfect tree. Two perfect $\kappa$-trees can have perfect $\kappa$-trees in their intersection but no maximal such tree. The second obstacle was that any useful generalization of Jensen's forcing to an inaccessible $\kappa$ had to be $\lt\kappa$-closed, but that meant that in the generalization of the construction we could not simply take the union posets at the limit stages because we would lose closure. But closing under sequences of length $\lt\kappa$ at limit stages could potentially unseal maximal antichains. This second obstacle seemed the more difficult to overcome, but it turned out that miraculously closing at limits to maintain a bunch of required closure properties did not unseal maximal antichains or cause any other trouble for the construction. The construction requires that $V$ satisfies $\diamondsuit_{\kappa^+}(\text{Cof}(\kappa))$ and in such a universe we have a recipe for constructing a subposet of the $\kappa$-Sacks forcing, let's call it $\mathbb J^{\kappa}$, with the properties that (1) it is $\lt\kappa$-closed, (2) it has the $\kappa^+$-cc and (3) it adds a unique generic subset of $\kappa$. We can show that in a forcing extension by the bounded support product of length $\kappa$ of the $\mathbb J^{\kappa}$, the only $\mathbb J^{\kappa}$-generic subsets of $\kappa$ are those added on the slices of the generic filter. We can also construct finite iterations $\mathbb J^{\kappa}_n$, for $n\lt\omega$, of Jensen's forcing at an inaccessible $\kappa$ and show that they have unique generic filters. The uniqueness property is again a consequence of a more general uniqueness property for the tree iterations of $\mathbb J^{\kappa}$ along a tree of height $\omega$. Conditions in the tree iteration along a tree $\mathcal T$ are functions with domain some subtree $T$ of $\mathcal T$ of size $\lt\kappa$ and range $\bigcup_{n\lt\omega}\mathbb J^{\kappa}_n$ such that nodes on level $n$ get mapped to elements of $\mathbb J^{\kappa}_n$ and higher nodes cohere with lower nodes.

At the moment, it seems that the details are going to work out to produce a model of Kelley-Morse together with the Choice Scheme in which the $\omega$-Dependent Choice Scheme fails. But I might have to retract (smiley face).

References

  1. 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.
  2. 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
  3. 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.
  4. V. Gitman and J. D. Hamkins, “Kelley-Morse set theory and choice principles for classes.”