<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

Online veröffentlicht: 28. März 2018

Seitenbereich: 249 - 259

Eingereicht: 29. Nov. 2017

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

Schlüsselwörter
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

Online veröffentlicht: 28. März 2018

Seitenbereich: 249 - 259

Eingereicht: 29. Nov. 2017

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

Schlüsselwörterformally 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.

Schlüsselwörter
formally real fields, ordered fields, abstract value, square roots