<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

Pubblicato online: 28 mar 2018

Pagine: 249 - 259

Ricevuto: 29 nov 2017

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

Parole chiave
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

Pubblicato online: 28 mar 2018

Pagine: 249 - 259

Ricevuto: 29 nov 2017

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

Parole chiaveformally 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.

Parole chiave
formally real fields, ordered fields, abstract value, square roots