Jensen _n¹ Reals by Means of ZFC and Second-Order Peano Arithmetic

It was established by Jensen in 1970 that there is a generic extension L[a] of the constructible universe L by a non-constructible real a is not an element of L, minimal over L, such that a is Delta(1)(3) in L[a]. Our first main theorem generalizes Jensen's result by constructing, for each n >= 2, a generic extension L[a] by a non-constructible real a is not an element of L, still minimal over L, such that a is Delta(1)(n+1) in L[a] but all Sigma(1)(n) reals are constructible in L[a]. 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 PA(2), or, equivalently, ZFC(-) (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 L-omega 2, which is way beyond ZFC(-). 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 Delta(1)(n+1) real as required as a class-forcing extension of a model of ZFC(-) plus V = L.