Definability is most often considered only for a first-order language (not a theory); a definable set is an equivalence class of formulas? which evaluate in the same way in every -structure. It makes sense to do the same for a theory: in that case in the definition of the equivalence relation one restricts to models of .
Let be a first-order language and a theory in . Any formula , whose only free variables could be among , together with a model for evaluates to a truth value on each , hence it determines the subset of all such that . Two formulas with the same number of free variables are equivalent if for every model of . A definable set in is an equivalence class of formulas in under this relation. Consider the category of -structures and elementary monomorphism?s and its full subcategory whose objects are the models of . We can also view a definable set for a theory as a functor which is of the form for some -formula .
By denote the set of all such that holds, i.e. is true for any choice of representative .
Given two definable sets in a definable function is a definable subset of the product sort such that is a function (we also write ) for every model of . Analogously a definable equivalence relation is a definable subset such that is an equivalence relation for every model of .
Proposition. Given a small category and two functors the natural transformations are in 1-1 correspondence with functors such that and such that is a functional relation.
Proof. If is an -indexed family with components viewed as functional relations , then the extension to a functor means
that there is a (automatically unique) dotted arrow
making the diagram commutative (once the existence of is known, the functoriality of comes by uniqueness of and the functoriality of which it restricts from). That means that for every should be sent to by , what is a restriction of , but by being functional relation this must be the same as , i.e. that . Q.E.D.
In other words, functoriality of is the same as being natural.
Corollary. Definable functions for (for ) are in 1-1 correspondence with natural transformations of definable sets as functors (resp. ).
For a fixed (multi-sorted, first-order) theory , definable sets and definable functions form a category . This category (or any equivalent category) is the syntactic category of the theory. Models of can be recovered as left exact functors . Notice that definable sets are functors from models to sets, and models are functors definable sets to sets; just the latter are the “evaluation functionals” among all functors.
See also definable groupoid.
An -definable set is an intersection of definable sets.
We can also consider a relative version of a definable set (definability with parameters).
Given definable sets , a fixed model and a fixed set , we say that an element is definable over if there is and a -definable function such that . All elements definable over form the subset . A subset is definably closed if it is closed under definable functions. Given , there is the minimal definably closed subset such that , the definable closure of .
If we extend the language by the constants from we get a new language . The definable sets in language over are the definable sets in language over .
Moshe Kamensky, Ind- and Pro- definable sets, math.LO/0608163
D. Haskell, E. Hrushovski, H.D.Macpherson, Definable sets in algebraically closed valued fields: elimination of imaginaries, J. reine und angewandte Mathematik 597 (2006), MR2007i:03040, doi/CRELLE.2006.066)