 Theory of real closed fields

This is the complete first-order theory of real closed fields.

The theory of real closed fields is complete and model-complete. In the language of ordered rings it eliminates quantifiers; in the pure language of rings its definable order prevents quantifier elimination.