Talk:Real closed field

Untitled

A real closed field is an ordered field F in which any of the following identical conditions are true:

(1) Every non-negative element of F has a square root in F, and any polynomial of odd degree has at least one root in F.

(2) The field extension $F({\sqrt {-1}})$ is algebraically closed.

(3) F has no proper algebraic extension to an ordered field.

If F is any ordered field, the Artin-Schreier theorem states that F has an algebraic extension, the real closure K of F, such that K is real closed and whose ordering is an extension of the ordering on F. For example, the real closure of the rational numbers are the real algebraic numbers. — Preceding unsigned comment added by Gene Ward Smith (talk • contribs) 23:09, 13 October 2004 (UTC)[reply]

This article desperately needs to be reviewed by someone familiar with the subject. I just removed some obvious nonsense, but there are still some highly suspicious statements (e.g., the definition of superreal field does not look to me like something which could guarantee real-closedness). EJ 22:18, 6 May 2005 (UTC)[reply]

Moreover, we do not need ultrapowers to construct Ϝ, we can do so much more constructively as the subfield of

\mathbb {R} ((G))

of formal power series on the Sierpinski group with a countable number of nonzero terms.

What are Sierpinski groups, and where can I find this construction? Tlepp 09:06, 8 November 2007 (UTC)[reply]

The general construction is decribed in the last but one subsection of formal power series, but I have no idea what the Sierpiński group is. -- EJ 10:32, 8 November 2007 (UTC)[reply]

I know what a power series is. The question is: how do you select a subfield of it constructively, and prove it's F. —Preceding unsigned comment added by Tlepp (talk • contribs) 11:18, 8 November 2007 (UTC)[reply]

I am not sure I follow you. I assume that "constructively" in the description of the field just means that it is explicitly defined (as opposed to the ultrapower construction, where you need to appeal to the axiom of choice to show, nonconstructively, the existence of a nonprincipal ultrafilter). Which it indeed is, provided the Sierpiński group (whatever it may be) is explicitly defined.

As for the proof (I am guessing here): you need to show that the structure is a RCF of cardinality of the continuum with the η₁ property. Now, by the comments in the formal power series article, it is automatically an ordered field, and it is real-closed if G is divisible. Obviously, it has the cardinality of continuum if G does (this is the place where the restriction to series with countable support is vital). It thus suffices to show the η₁ property, which I think should follow with a bit of effort from the η₁ property of G.

Incidentally, the conditions on G mentioned above are easily seen to be necessary, hence we can actually deduce what the Sierpiński group is: it is the divisible totally ordered abelian group of cardinality of the continuum with the η₁ property. (Such a structure is unique up to isomorphism, assuming the continuum hypothesis.) How to construct it explicitly is another matter though. -- EJ 11:11, 9 November 2007 (UTC)[reply]

Thanks for help, now it seems plausible with Sierpiński group hypothesis Tlepp 14:05, 9 November 2007 (UTC)[reply]

I removed the words "(The choice of signature is not significant.)" in the first equivalent proposition. Keisler says: "There is an important loophole in the result of Tarski. It applies only to formulas in the language of ordered fields, that is, formulas built up from the predicates =, <, the function symbols +, ., and the constants 0 and 1. Nothing has been said about how one might extend other real relations or functions to the larger set F. For example, the exponential functions, the trigonometric functions, and the set of natural numbers cannot be defined in the language of ordered fields." Excerpt taken from "The Hyperreal Line" found on p. 212 in the Monograph "Real Numbers, Generalizations of the Reals, and Theories of the Continua" edited by P. Ehrlich (1994) 83.81.41.27 (talk) 03:57, 3 April 2019 (UTC)[reply]

"Decidability and quantifier elimination" section

There seemed to be some confusion in the "Decidability and quantifier elimination" section, regarding the distinction between theories and languages. I have rewritten it for rigor as well as clarity. --Jordan Mitchell Barrett (talk) 03:53, 10 April 2020 (UTC)[reply]

euclidean geometry

Decidability of rcf is related to a theorem of Tarski about decidability of Euclidean geometry. Could a cross reference be added? Thanks. I had for some reason thought the Euclidean closure of Q was an rcf, but that is obviously wrong, so the situation is more complicated. 2601:644:8503:A980:8A6:A89B:8B0A:E2B1 (talk) 08:40, 31 May 2023 (UTC)[reply]

Redundancy in definition

The definition includes:

2. 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.

3. 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 = b² or a = −b².

It seems to me that this could be stated more simply as:

2. There is a total order on F.

3. 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 = b² or a = −b².

Philgoetz (talk) 15:07, 18 August 2024 (UTC)[reply]