A real closed field (RCF) K is a field in which -1 is not a sum of squares and every polynomial of odd degree has a root.
In [MR], Mourgues and Ressayre showed that every real closed field has an integer part.
Concerning the theorems mentioned above, the Axiom of Choice turns out to be indeed necessary: In section 4, we construct transitive models of Zermelo-Fraenkel set theory without the Axiom of Choice (ZF) containing a real closed field K, but no integer part of K.
Remark: In order for some of our statements to make sense, we note that the value group and the residue field of a real closed field K, being definable over K, exist in plain ZF.
We now construct a transitive M |= ZF such that, for some K [member of] M, M satisfies that K is a real closed field that has no integer part.
If K is a real closed field, then X [subset or equal to] K is bounded in K iff there is y [member of] K such that y > x for every x [member of] X.
Let K be a countable, unbounded, [omega]-homogenous real closed field, let [?
If K is a countable, unbounded, [omega]-homogenous real closed field, then no integer part I of K has a support.
Hence M believes that K' is a real closed field without an integer part.
If K is a real closed field, then x, y - K are called archimedean equivalent, written x ~ y, iff they are archimedean equivalent as elements of the totally ordered abelian group (K, +).
Let K be a real closed field with value group [theta]([K.
It was proved in [Ka] (Theorem 8) that every real closed field has a value group section with respect to the standard valuation.