An elementary definability theorem for first order logic (Q4934027)

The authors prove the following definablility theorem. For any first order theory \(T\) there exists a Boolean valued model \(M\) such that (i) for any sentence \(\phi\), \(M \models \phi\) iff \(T \vdash \phi\) and (ii) any predicate which is invariant under all automorphisms of \(M\) is definable. This is a generalisation e.g. of the well-known fact that every countable complete theory has a model with the above properties, for example a countable recursively saturated model. The paper is entirely self-contained. The authors give a comprehensive introduction into Boolean valued models. Using only elementary tools from model theory, a small Boolean valued model satisfying (i) and (ii) is constructed. In an appendix the authors give a topos-theoretical interpretation of this Boolean valued model, which yields a variant of a theorem of Freyd's [\textit{P. Freyd}, ``All topoi are localic or why permutation models prevail'', J. Pure Appl. Algebra 46, 49-58 (1987; Zbl 0611.18003)].