| Summary: | In this paper we prove that for any <inline-formula><math display="inline"><semantics><mrow><mi>m</mi><mo>≥</mo><mn>1</mn></mrow></semantics></math></inline-formula> there exists 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 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><msub><mi mathvariant="bold">D</mi><mrow><mn>1</mn><mi>m</mi></mrow></msub></semantics></math></inline-formula> of all reals definable by a parameter free type-theoretic formula with types bounded by <i>m</i>, and hence the Tarski ‘definability of definable’ sentence <inline-formula><math display="inline"><semantics><mrow><msub><mi mathvariant="bold">D</mi><mrow><mn>1</mn><mi>m</mi></mrow></msub><mo>∈</mo><msub><mi mathvariant="bold">D</mi><mrow><mn>2</mn><mi>m</mi></mrow></msub></mrow></semantics></math></inline-formula> (even in the form <inline-formula><math display="inline"><semantics><mrow><msub><mi mathvariant="bold">D</mi><mrow><mn>1</mn><mi>m</mi></mrow></msub><mo>∈</mo><msub><mi mathvariant="bold">D</mi><mn>21</mn></msub></mrow></semantics></math></inline-formula>) holds for this particular <i>m</i>. This solves an old problem of Alfred Tarski (1948). Our methods, based on the almost-disjoint forcing of Jensen and Solovay, are significant modifications and further development of the methods presented in our two previous papers in this Journal.
|
|---|