Quantifier elimination for ordered real closed fields
= Quantifier elimination for ordered real closed fields
= Tarski quantifier elimination theorem
{c}
{synonym}
In the language of ordered rings, the <Theory of real closed fields> has <quantifier elimination>. In its pure ring reduct the order is definable by nonzero squares, so model completeness survives, although quantifier elimination does not. Keeping these two language conventions separate is essential when constructing a <model companion>.