| Summary: | In this paper, we prove the following. If <inline-formula><math display="inline"><semantics><mrow><mi>n</mi><mo>≥</mo><mn>3</mn></mrow></semantics></math></inline-formula>, then there is a generic extension of <inline-formula><math display="inline"><semantics><mi mathvariant="bold">L</mi></semantics></math></inline-formula>, the constructible universe, in which it is true that the set <inline-formula><math display="inline"><semantics><mrow><mrow><mspace width="0.42502pt"></mspace><mi mathvariant="script">P</mi><mspace width="0.42502pt"></mspace></mrow><mo>(</mo><mi>ω</mi><mo>)</mo><mo>∩</mo><mi mathvariant="bold">L</mi></mrow></semantics></math></inline-formula> of all constructible reals (here—subsets of <inline-formula><math display="inline"><semantics><mi>ω</mi></semantics></math></inline-formula>) is equal to the set <inline-formula><math display="inline"><semantics><mrow><mrow><mspace width="0.42502pt"></mspace><mi mathvariant="script">P</mi><mspace width="0.42502pt"></mspace></mrow><mrow><mo>(</mo><mi>ω</mi><mo>)</mo></mrow><mo>∩</mo><msubsup><mi>Δ</mi><mi>n</mi><mn>1</mn></msubsup></mrow></semantics></math></inline-formula> of all (lightface) <inline-formula><math display="inline"><semantics><msubsup><mi>Δ</mi><mi>n</mi><mn>1</mn></msubsup></semantics></math></inline-formula> 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 <inline-formula><math display="inline"><semantics><mrow><mrow><mspace width="0.42502pt"></mspace><mi mathvariant="double-struck">Q</mi><mspace width="0.42502pt"></mspace></mrow><mo>=</mo><mi mathvariant="double-struck">C</mi><mo>ℂ</mo><mo>×</mo><msub><mo>∏</mo><mi>ν</mi></msub><msub><mrow><mspace width="0.42502pt"></mspace><mi mathvariant="double-struck">Q</mi><mspace width="0.42502pt"></mspace></mrow><mi>ν</mi></msub></mrow></semantics></math></inline-formula> in <inline-formula><math display="inline"><semantics><mi mathvariant="bold">L</mi></semantics></math></inline-formula>, where <inline-formula><math display="inline"><semantics><mi mathvariant="double-struck">C</mi></semantics></math></inline-formula> adds a generic collapse surjection <i>b</i> from <inline-formula><math display="inline"><semantics><mi>ω</mi></semantics></math></inline-formula> onto <inline-formula><math display="inline"><semantics><mrow><mrow><mspace width="0.42502pt"></mspace><mi mathvariant="script">P</mi><mspace width="0.42502pt"></mspace></mrow><mo>(</mo><mi>ω</mi><mo>)</mo><mo>∩</mo><mi mathvariant="bold">L</mi></mrow></semantics></math></inline-formula>, whereas each <inline-formula><math display="inline"><semantics><msub><mrow><mspace width="0.42502pt"></mspace><mi mathvariant="double-struck">Q</mi><mspace width="0.42502pt"></mspace></mrow><mi>ν</mi></msub></semantics></math></inline-formula>, <inline-formula><math display="inline"><semantics><mrow><mi>ν</mi><mo><</mo><msubsup><mi>ω</mi><mn>2</mn><mi mathvariant="bold">L</mi></msubsup></mrow></semantics></math></inline-formula>, is an almost-disjoint forcing notion in the <inline-formula><math display="inline"><semantics><msub><mi>ω</mi><mn>1</mn></msub></semantics></math></inline-formula>-version, that adjoins a subset <inline-formula><math display="inline"><semantics><msub><mi>S</mi><mi>ν</mi></msub></semantics></math></inline-formula> of <inline-formula><math display="inline"><semantics><msubsup><mi>ω</mi><mn>1</mn><mi mathvariant="bold">L</mi></msubsup></semantics></math></inline-formula>. The forcing notions involved are independent in the sense that no <inline-formula><math display="inline"><semantics><msub><mrow><mspace width="0.42502pt"></mspace><mi mathvariant="double-struck">Q</mi><mspace width="0.42502pt"></mspace></mrow><mi>ν</mi></msub></semantics></math></inline-formula>-generic object can be added by the product of <inline-formula><math display="inline"><semantics><mi mathvariant="double-struck">C</mi></semantics></math></inline-formula> and all <inline-formula><math display="inline"><semantics><msub><mrow><mspace width="0.42502pt"></mspace><mi mathvariant="double-struck">Q</mi><mspace width="0.42502pt"></mspace></mrow><mi>ξ</mi></msub></semantics></math></inline-formula>, <inline-formula><math display="inline"><semantics><mrow><mi>ξ</mi><mo>≠</mo><mi>ν</mi></mrow></semantics></math></inline-formula>. This allows the definition of each constructible real by a <inline-formula><math display="inline"><semantics><msubsup><mo>Σ</mo><mi>n</mi><mn>1</mn></msubsup></semantics></math></inline-formula> formula in a suitably constructed subextension of the <inline-formula><math display="inline"><semantics><mrow><mspace width="0.42502pt"></mspace><mi mathvariant="double-struck">Q</mi><mspace width="0.42502pt"></mspace></mrow></semantics></math></inline-formula>-generic extension. The subextension is generated by the surjection <i>b</i>, sets <inline-formula><math display="inline"><semantics><msub><mi>S</mi><mrow><mi>ω</mi><mo>·</mo><mi>k</mi><mo>+</mo><mi>j</mi></mrow></msub></semantics></math></inline-formula> with <inline-formula><math display="inline"><semantics><mrow><mi>j</mi><mo>∈</mo><mi>b</mi><mo>(</mo><mi>k</mi><mo>)</mo></mrow></semantics></math></inline-formula>, and sets <inline-formula><math display="inline"><semantics><msub><mi>S</mi><mi>ξ</mi></msub></semantics></math></inline-formula> with <inline-formula><math display="inline"><semantics><mrow><mi>ξ</mi><mo>≥</mo><mi>ω</mi><mo>·</mo><mi>ω</mi></mrow></semantics></math></inline-formula>. A special character of the construction of forcing notions <inline-formula><math display="inline"><semantics><msub><mrow><mspace width="0.42502pt"></mspace><mi mathvariant="double-struck">Q</mi><mspace width="0.42502pt"></mspace></mrow><mi>ν</mi></msub></semantics></math></inline-formula> is <inline-formula><math display="inline"><semantics><mi mathvariant="bold">L</mi></semantics></math></inline-formula>, which depends on a given <inline-formula><math display="inline"><semantics><mrow><mi>n</mi><mo>≥</mo><mn>3</mn></mrow></semantics></math></inline-formula>, obscures things with definability in the subextension enough for vice versa any <inline-formula><math display="inline"><semantics><msubsup><mi>Δ</mi><mi>n</mi><mn>1</mn></msubsup></semantics></math></inline-formula> real to be constructible; here the method of <i>hidden invariance</i> is applied. A discussion of possible further applications is added in the conclusive section.
|
|---|