Real closed field

In mathematics, a real closed field is a field F that has the same first-order properties as the field of real numbers. Some examples are the field of real numbers, the field of real algebraic numbers, and the field of hyperreal numbers. A real closed field is a field F in which any of the following equivalent conditions is true: F is elementarily equivalent to the real numbers. In other words, it has the same first-order properties as the reals: any sentence in the first-order language of fields is true in F if and only if it is true in the reals. There is a total order on F making it an ordered field such that, in this ordering, every positive element of F has a square root in F and any polynomial of odd degree with coefficients in F has at least one root in F. F is a formally real field such that every polynomial of odd degree with coefficients in F has at least one root in F, and for every element a of F there is b in F such that a = b2 or a = −b2. F is not algebraically closed, but its algebraic closure is a finite extension. F is not algebraically closed but the field extension is algebraically closed. There is an ordering on F that does not extend to an ordering on any proper algebraic extension of F. F is a formally real field such that no proper algebraic extension of F is formally real. (In other words, the field is maximal in an algebraic closure with respect to the property of being formally real.) There is an ordering on F making it an ordered field such that, in this ordering, the intermediate value theorem holds for all polynomials over F with degree ≥ 0. F is a weakly o-minimal ordered field. If F is an ordered field, the Artin–Schreier theorem states that F has an algebraic extension, called the real closure K of F, such that K is a real closed field whose ordering is an extension of the given ordering on F, and is unique up to a unique isomorphism of fields identical on F (note that every ring homomorphism between real closed fields automatically is order preserving, because x ≤ y if and only if ∃z : y = x + z2).