<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

Published Online: Mar 28, 2018

Page range: 249 - 259

Received: Nov 29, 2017

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

Keywords
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

Published Online: Mar 28, 2018

Page range: 249 - 259

Received: Nov 29, 2017

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

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

Keywords
formally real fields, ordered fields, abstract value, square roots