A Definability Theorem for First Order Logic

Resumé

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 (i.e., a subset S = {a | M |= phi(a)} defined by some formula phi) is invariant under all
automorphisms of M. The same is of course true for subsets of M" 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 T-provable formulas hold, and in which every (Boolean valued) subset which is invariant under all automorphisms of M is definable 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 [1]. In fact, one of the results in that paper could be interpreted as a definability theorem for infinitary logic, using topological rather than Boolean valued models.