Jensen <semantics><msubsup>Δn1</msubsup></semantics> Reals by Means of ZFC and Second-Order Peano Arithmetic - Vladimir Kanovei; Vassily Lyubetsky (Axioms, 2024)
It was established by Jensen in 1970 that there is a generic extension <semantics>L[a]</semantics> of the constructible universe <semantics>L</semantics> by a non-constructible real <semantics>a∉L</semantics>, minimal over <semantics>L</semantics>, such that a is <semantics><msubsup>Δ31</msubsup></semantics> in <semantics>L[a]</semantics>. Our first main theorem generalizes Jensen’s result by constructing, for each <semantics>n≥2</semantics>, a generic extension <semantics>L[a]</semantics> by a non-constructible real <semantics>a∉L</semantics>, still minimal over <semantics>L</semantics>, such that a is <semantics><msubsup>Δn+11</msubsup></semantics> in <semantics>L[a]</semantics> but all <semantics><msubsup>Σn1</msubsup></semantics> reals are constructible in <semantics>L[a]</semantics>. Jensen’s forcing construction has found a number of applications in modern set theory. A problem was recently discussed as to whether Jensen’s construction can be reproduced entirely by means of second-order Peano arithmetic <semantics>PA2</semantics>, or, equivalently, <semantics>ZFC−</semantics> (minus the power set axiom). The obstacle is that the proof of the key CCC property (whether by Jensen’s original argument or the later proof using the diamond technique) essentially involves countable elementary submodels of <semantics>Lω2</semantics>, which is way beyond <semantics>ZFC−</semantics>. We demonstrate how to circumvent this difficulty by means of killing only definable antichains in the course of a Jensen-like transfinite construction of the forcing notion, and then use this modification to define a model with a minimal <semantics><msubsup>Δn+11</msubsup></semantics> real as required as a class-forcing extension of a model of <semantics>ZFC−</semantics> plus <semantics>V=L</semantics>.