A real closed field is a formally real field with no proper formally real algebraic extension. Equivalently every positive element in its unique compatible order is a square and every odd-degree polynomial has a root. Its positive cone is definable in the field language as the nonzero squares. The Theory of real closed fields is model-complete.
A real closure of an ordered field is a real closed algebraic extension whose order extends the chosen order of . Existence is the real closure theorem; uniqueness holds up to ordered field isomorphism over . A different ordering of a formally real field can produce a different ordered real closure.
Every ordered field has an ordered algebraic real closure. Combined with the Artin-Schreier ordering criterion, every formally real field embeds into a real closed field. This is one embedding direction in the model companion relation between their theories.
Articles by others on the same topic
A **real closed field** is a type of field in which certain algebraic properties analogous to those of the real numbers hold. More formally, a field \( K \) is called a real closed field if it satisfies the following conditions: 1. **Algebraically Closed**: Every non-constant polynomial in one variable with coefficients in \( K \) has a root in \( K \).