An ordered field (K, < ) is said to be real-closed if it satisfies one of the following equivalent conditions:
The prototypical example of a real-closed field is ℝ. Other notable examples include Puiseux series in ℝ, Hahn series in ℝ, and the surreal numbers.
The ordering on a real closed field can be algebraically defined: x ≥ y if and only if x − y is a square. Real closed fields are uniquely orderable, so it makes sense to say that a pure field K is real closed.
The Artin-Schreier theorem (?) says that if K is a field with finite absolute Galois group, then either K is algebraically closed, or K is real closed (and hence of characteristic zero). So the real closed fields can also be described as those pure fields with finite but non-trivial absolute Galois group.
The class of real closed fields is an elementary class, i.e., the set of models of some theory. This theory is usually denoted RCF. Unlike the case of ACF, RCF is complete. One usually works in one of two languages:
The theory RCF is the model companion of ordered fields, or more generally ordered domains. In the pure ring language, it is also the model companion of the theory of orderable fields, i.e., fields admitting at least one ordering. (These turn out to be exactly the fields in which − 1 is not a sum of squares.)
RCF is o-minimal, and therefore NIP. On the other hand, RCF (obviously) has the strong order property, so it is not stable, or simple.
RCF has elimination of imaginaries, as does every o-minimal expansion of RCF. In fact, RCF and its o-minimal expansions all have definable choice: if ϕ(x; y) is a formula, then there is a formula ψ(x; y) such that for every b, if ϕ(K; b) is non-empty, then ψ(K; b) is a singleton in ϕ(K; b). In particular, RCF and its o-minimal expansions have definable Skolem functions. Every definably closed set is a model. ::: ::: :::