<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

Data publikacji: 28 mar 2018

Zakres stron: 249 - 259

Otrzymano: 29 lis 2017

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

Słowa kluczowe
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

Data publikacji: 28 mar 2018

Zakres stron: 249 - 259

Otrzymano: 29 lis 2017

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

Słowa kluczoweformally 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.

Słowa kluczowe
formally real fields, ordered fields, abstract value, square roots