On the <inline-formula> <mml:math id="mm11111111" display="block"> <mml:semantics> <mml:mrow> <mml:msubsup> <mml:mo mathvariant="bold">Δ</mml:mo> <mml:mi mathvariant="bold-italic">n</mml:mi> <mml:mn mathvariant="bold">1</mml:mn> </mml:msubsup> </mml:mrow> </mml:semantics> </mml:math> </inline-formula> Problem of Harvey Friedman

Abstract

In this paper, we prove the following. If n≥3, then there is a generic extension of L, the constructible universe, in which it is true that the set P(ω)∩L of all constructible reals (here—subsets of ω) is equal to the set P(ω)∩Δn1 of all (lightface) Δn1 reals. The result was announced long ago by Leo Harrington, but its proof has never been published. Our methods are based on almost-disjoint forcing. To obtain a generic extension as required, we make use of a forcing notion of the form Q=Cℂ×∏νQν in L, where C adds a generic collapse surjection b from ω onto P(ω)∩L, whereas each Qν, νω2L, is an almost-disjoint forcing notion in the ω1-version, that adjoins a subset Sν of ω1L. The forcing notions involved are independent in the sense that no Qν-generic object can be added by the product of C and all Qξ, ξ≠ν. This allows the definition of each constructible real by a Σn1 formula in a suitably constructed subextension of the Q-generic extension. The subextension is generated by the surjection b, sets Sω·k+j with j∈b(k), and sets Sξ with ξ≥ω·ω. A special character of the construction of forcing notions Qν is L, which depends on a given n≥3, obscures things with definability in the subextension enough for vice versa any Δn1 real to be constructible; here the method of hidden invariance is applied. A discussion of possible further applications is added in the conclusive section.

Keywords

• Harvey Friedman’s problem
• definability
• nonconstructible reals
• projective hierarchy
• generic models
• almost-disjoint forcing