<abstract xmlns="http://www.w3.org/1999/xhtml"><p> We extend the algebraic theory of ordered fields [7, 6] in Mizar [1, 2, 3]: we show that every preordering can be extended into an ordering, i.e. that formally real and ordered fields coincide.We further prove some characterizations of formally real fields, in particular the one by Artin and Schreier using sums of squares [4]. In the second part of the article we define absolute values and the square root function [5].</p></abstract>

We extend the algebraic theory of ordered fields [7, 6] in Mizar [1, 2, 3]: we show that every preordering can be extended into an ordering, i.e. that formally real and ordered fields coincide.We further prove some characterizations of formally real fields, in particular the one by Artin and Schreier using sums of squares [4]. In the second part of the article we define absolute values and the square root function [5].

Formally Real Fields

Formalized Mathematics

This work is licensed under the Creative Commons Attribution-ShareAlike 4.0 International (CC BY-SA 4.0) License.

{"article-title":"Formally Real Fields"}

We extend the algebraic theory of ordered fields [7, 6] in Mizar [1, 2, 3]: we show that every preordering can be extended into an ordering, i.e. that formally...

Formally Real Fields

Publié en ligne: 28 mars 2018

Pages: 249 - 259

Reçu: 29 nov. 2017

DOI: https://doi.org/10.1515/forma-2017-0024

Mots clés
formally real fields, ordered fields, abstract value, square roots

© by Christoph Schwarzweller

This work is licensed under the Creative Commons Attribution-ShareAlike 4.0 International (CC BY-SA 4.0) License.

Formally Real Fields

Publié en ligne: 28 mars 2018

Pages: 249 - 259

Reçu: 29 nov. 2017

DOI: https://doi.org/10.1515/forma-2017-0024

Mots clésformally real fields, ordered fields, abstract value, square roots

© by Christoph Schwarzweller

This work is licensed under the Creative Commons Attribution-ShareAlike 4.0 International (CC BY-SA 4.0) License.

Mots clés
formally real fields, ordered fields, abstract value, square roots