A definability theorem for first order logic

In this paper we will present a definability theorem for first order logic This theorem is very easy to state and its proof only uses elementary tools To explain the theorem let us first observe that if M is a model of a theory T in a language L then clearly any definable subset S M ie a subset S fa j M j ag defined by some formula is invariant under all automorphisms of M The same is of course true for subsets of Mn defined by formulas with n free variables Our theorem states that if one allows Boolean valued models the converse holds More precisely for any theory T we will construct a Boolean valued model M in which precisely the Tprovable formulas hold and in which every Boolean valued subset which is invariant under all automorphisms of M is denable by a formula of L Our presentation is entirely selfcontained and only requires familiarity with the most elementary properties of model theory In particular we have added a first section in which we review the basic definitions concerning Boolean valued models. The Boolean algebra used in the construction of the model will be presented concretely as the algebra of closed and open subsets of a topological space X naturally associated with the theory T The construction of this space is closely related to the one in In fact one of the results in that paper could be interpreted as a definability theorem for innitary logic using topological rather than Boolean valued model