Definition of Pythagorean fields

[ghost]

Similar question to the one whether the definition of group should include an explicit inverse function or not (cf #37):
Should a Pythagorean field $F$ be defined as a field such that for all elements $a:F$ and $b:F$ there merely exists an element $c:R$ such that $a^2 + b^2 = c^2$,
or as a field with a binary function $\rho:F \times F \to F$ such that for all elements $a:F$ and $b:F$, $a^2 + b^2 = \rho(a, b)^2$?

[DanGrayson]

Why not just use the field of real numbers, instead of introducing the notion of Pythagorean field?

[ghost]

Currently, the proposed section 8.6 for chapter 8 of the Symmetry book has the following title: "ordered fields, real-closed fields, pythagorean fields, euclidean fields". I have no idea who proposed the section titles/topics for the chapter.

[UlrikBuchholtz]

The section heading currently numbered 8.6 dates back to our initial brain-storming of possible topics. (I may have been the one proposing these.) However, covering ordered fields, real-closed fields, euclidean and pythagorean fields, etc., is probably not appropriate for the book as it is now. It could be appropriate for a more advanced sequel, though.

In any case, the definition should be with the mere existence of square roots of sums of squares, so as not to lose automorphisms.

[ghost]

I suppose I'll stick this in this discussion since we were talking about section 8.6 earlier.

Even though there might not be space to talk about Euclidean fields in the textbook, if one were to define Euclidean fields, is the proper definition of an Euclidean field an ordered field $F$ where for every element $f:F$ such that $f > 0$ there merely exists an element $g:F$ such that $f = g^2$, or an ordered field $F$ where for every element $f:F$ such that $f \geq 0$ there merely exists an element $g:F$ such that $f = g^2$? These two definitions are interchangeable in classical mathematics since $0^2 = 0$ and excluded middle, but are not equivalent in constructive mathematics. I assume that one wants mere existence here as well, instead of structure.

[UlrikBuchholtz]

There are many definitions of euclidean fields that are classically equivalent, and I haven't really thought about how/whether they differ constructively. In Elementary constructive theory of ordered fields, Lombardi and Roy only consider discrete fields.

Another definition is: F is euclidean iff it's formally real and every invertible element is either plus or minus a square. In this case, one gets/hopes that there's a unique ordering with positive elements exactly the invertible squares.

A test of whether we have a good definition would be to give a formulation of Sylvester's law of inertia that holds constructively for the reals, and then it should also hold for all euclidean fields. Another test would be to give a good definition of the Witt ring for Heyting fields, including a signature map to the integers, and show that for euclidean fields the signature is a bijection.