On the ‘Definability of Definable’ Problem of Alfred Tarski

Abstract

In this paper we prove that for any m≥1 there exists a generic extension of L, the constructible universe, in which it is true that the set of all constructible reals (here subsets of ω) is equal to the set D1m of all reals definable by a parameter free type-theoretic formula with types bounded by m, and hence the Tarski ‘definability of definable’ sentence D1m∈D2m (even in the form D1m∈D21) holds for this particular m. 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.

Keywords

• definability of definable
• tarski problem
• type theoretic hierarchy
• generic models
• almost disjoint forcing