Formally real fields

Christoph Schwarzweller


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].
Author Christoph Schwarzweller II
Christoph Schwarzweller,,
- Institute of Informatics
Journal seriesFormalized Mathematics, ISSN 1426-2630, e-ISSN 1898-9934
Issue year2017
Publication size in sheets0.5
Keywords in Englishformally real fields, ordered fields, abstract value, square root
Languageen angielski
LicenseJournal (articles only); published final; Uznanie Autorstwa - Na Tych Samych Warunkach (CC-BY-SA); with publication
Score (nominal)12
ScoreMinisterial score = 12.0, 23-04-2018, ArticleFromJournal
Ministerial score (2013-2016) = 12.0, 23-04-2018, ArticleFromJournal
Citation count*0
Share Share

* presented citation count is obtained through Internet information analysis and it is close to the number calculated by the Publish or Perish system.