Parameter-free comprehension in second-order arithmetic

This is a talk at the CUNY Logic Workshop, CUNY Graduate Center, March 24, 2023.
Slides

Second-order arithmetic has two types of objects: numbers and sets of numbers, which we think of as the reals. The second-order arithmetic framework has been used successfully to investigate what kinds of real numbers need to exist to prove various significant results in analysis. One of the strongest second-order arithmetic axiomatizations is the theory ${\rm Z}_2$ consisting of the axioms ${\rm PA}$ (for numbers), the set induction axiom, and comprehension for all second-order formulas with set parameters. How significant is the inclusion of set parameters in the comprehension scheme? Let ${\rm Z}_2^{-p}$ be like ${\rm Z}_2$, but where set parameters are not allowed in the comprehension scheme. Harvey Friedman showed that ${\rm Z}_2$ and ${\rm Z}_2^{-p}$ are equiconsistent because parameter-free comprehension suffices to build a model's version of the constructible universe $L$ inside the model and the 'constructible' reals satisfy ${\rm Z}_2$. Kanovei recently showed that models of ${\rm Z}_2^{-p}$ can be very badly behaved, for example, their sets may not even be closed under complement. Kanovei also showed that there can be nicely behaved models of ${\rm Z}_2^{-p}$ in which $\Sigma^1_2$-comprehension (with set parameters) holds. He constructed his model in a forcing extension by a tree iteration of Sacks forcing. In Kanovei's model, $\Sigma^1_4$-comprehension (with set parameters) fails and he asked whether this can be improved to $\Sigma^1_3$-comprehension. In this talk, I will show how to construct a model of $\Sigma^1_2$-comprehension and ${\rm Z}_2^{-p}$ in which $\Sigma^1_3$-comprehension fails. The model will be constructed in a forcing extension by a tree iteration of Jensen's forcing. Jensen's forcing is a sub-poset of Sacks forcing constructed by Jensen to show that it is consistent to have a non-constructible $\Pi^1_2$-definable singleton real (every $\Sigma^1_2$-definable set of reals is constructible by Shoenfield's Absoluteness).