Jensen's forcing at an inaccessible

This is a talk at the 16th International Luminy Workshop in Set Theory, CIRM, September 14, 2021 (virtual).
Slides

Jensen constructed in $L$, using $\diamondsuit$, a subposet of the Sacks forcing with the ccc and the property that it adds a unique generic real over $L$ (in contrast to, say, Cohen forcing which adds continuum many generic reals). He used what came to be known as Jensen's forcing to show that, consistently, there can be a $\Pi^1_2$-definable non-constructible real. The 'uniqueness of generic reals' property of Jensen's forcing can be extended to products of Jensen's forcing and in some form to iterations, when forcing over $L$. Indeed, a Jensen-like forcing with the uniqueness properties can be constructed in any universe with a $\diamondsuit$-sequence. In a joint work with Friedman and Kanovei, we used a tree iteration of Jensen's forcing to construct (in a symmetric submodel of the forcing extension) a model of full second-order arithmetic ${\rm Z}_2$ with the choice scheme in which the dependent choice scheme failed for a $\Pi^1_2$-assertion (this is optimal because ${\rm Z}_2$ with the choice scheme implies dependent choice for $\Sigma^1_2$-assertions). In this talk, I will present a generalization of Jensen's forcing to a sub-forcing of the $\kappa$-Sacks forcing for an inaccessible cardinal $\kappa$. I will show that Jensen's forcing at an inaccessible has some of the same 'uniqueness of generics' properties as Jensen's forcing. One of the goals of this work is to prove an analogue of the second-order arithmetic result for second-order set theory by showing that the dependent choice scheme is independent of the second-order Kelley-Morse set theory with the choice scheme. This is joint work with Sy-David Friedman.