Let L be a first order language. If M is an L-structure, let LM be the expansion of L obtained by adding constants for the elements of M.
Definition. A type is definable if and only if for any L-formula , there is an LM-formula so that for all iff M ⊨ dθ(¯). The formula dθ is called the definition of θ.
Definable types play a central role in stability theory and have also proven useful in the study of models of arithmetic. We also remark that it is well known and easy to see that for M ≺ N, the property that every M-type realized in N is definable is equivalent to N being a conservative extension of M, where
Definition. If M ≺ N, we say that N is a conservative extension of M if for any n and any LN -definable S ⊂ Nn, S ∩ Mn is LM-definable in M.
Van den Dries [Dl] studied definable types over real closed fields and proved the following result.
0.1 (van den Dries), (i) Every type over (R, +, -,0,1) is definable.
(ii) Let F and K be real closed fields and F ⊂ K. Then, the following are equivalent:
(a) Every element of K that is bounded in absolute value by an element of F is infinitely close (in the sense of F) to an element of F.
(b) K is a conservative extension of F.