Kreisel’s unwinding of Artin’s proof. (English) Zbl 0876.12002

Odifreddi, Piergiorgio (ed.), Kreiseliana: about and around Georg Kreisel. Wellesley, MA: A K Peters. 113-246 (1996).
Georg Kreisel has sketched two ways to “unwind” Artin’s theorem of 1926 stating that positive semidefinite rational functions \(f\in\mathbb{Q} (X_1,\dots,X_n)\) can be represented as sums of squares of rational functions: \(f= \sum_i r_i^2\) for some \(r_i\in\mathbb{Q} (X_1,\dots, X_n)\) (cf. p. 116). “Unwinding” means to determine the constructive content or the constructive equivalent of non-constructive concepts and theorems. The author’s purpose is “to work out […] Kreisel’s two sketches of constructive proofs of Artin’s theorem, thereby showing […] that those sketches are essentially correct. Whatever additional result I establish here will also be based only on knowledge (e.g., of Hilbert’s \(\varepsilon\)-substitution method) available up to the time of those sketches (1955). The point of this is to show that after Kreisel’s contribution, most results of Artin-Schreier theory […] either were, or easily could have been, satisfactorily constructivized” (p. 129). The paper deals with Kreisel’s second sketch, whereas Part II, which is still in preparation, will discuss Kreisel’s first sketch and continuous versions of Artin’s theorem found in the 80s.
For the entire collection see [Zbl 0894.03002].


12D15 Fields related with sums of squares (formally real fields, Pythagorean fields, etc.)
01A60 History of mathematics in the 20th century
03F65 Other constructive mathematics