Corps réel clos

Les corps suivants sont réels clos :

• le corps des réels,
• le sous-corps des réels algébriques,
• le corps des réels calculables (au sens de Turing),
• le corps des réels définissables (en),
• le corps des séries de Puiseux à coefficients réels,
• tout corps superréel (en particulier tout corps hyperréel).

Un corps commutatif F est réel clos (selon la définition de l'introduction) si et seulement s'il vérifie l'une des propriétés équivalentes suivantes[2] :

1. F est euclidien[3] et tout polynôme de degré impair à coefficients dans F admet au moins une racine dans F ;
2. –1 n'est pas un carré dans F et F(√-1) est algébriquement clos ;
3. la clôture algébrique de F est une extension finie propre de F ;
4. il existe un ordre sur F pour lequel le théorème des valeurs intermédiaires est vrai pour tout polynôme sur F.

Une démonstration de l'implication 1 ⇒ 2 (attribuée par Nicolas Bourbaki à Euler et Lagrange[4]) est donnée dans l'article consacré au théorème de d'Alembert-Gauss.

Emil Artin et Otto Schreier ont démontré en 1927[5] que pour tout corps totalement ordonné K, il existe un corps réel clos algébrique sur K et dont l'ordre prolonge celui de K. Cette extension, unique à isomorphisme près, est appelée la clôture réelle de K.

Par exemple, « la » clôture réelle de ℚ est le corps ℝ∩ℚ des réels algébriques, d'après la caractérisation 2 ci-dessus. On peut remarquer[6] que d'après la caractérisation 3, c'est « l'unique » extension algébrique de ℚ dont « la » clôture algébrique ℚ est une extension finie propre.

De plus, pour tout sous-corps « réel » (c'est-à-dire totalement ordonnable) d'un corps algébriquement clos ${\displaystyle L}$, il existe un sous-corps intermédiaire ${\displaystyle F}$ réel clos tel que ${\displaystyle L=F({\sqrt {-1}})}$[7].

La théorie des corps réels clos est une théorie du premier ordre dont les symboles non logiques sont les constantes 0 et 1, les opérations arithmétiques +, ×, et la relation ≤ ; les formules sont construites à partir des formules atomiques via les connecteurs ⋀, ⋁, ⇒, et les quantificateurs ∀, ∃ ; les axiomes sont ceux qui expriment que la structure est précisément un corps réel clos.

Cette théorie admet l'élimination des quantificateurs, c'est-à-dire qu'il est possible, à partir d'une formule avec quantificateurs, de trouver une formule sans quantificateurs, avec les mêmes variables libres, et équivalente (c'est-à-dire que l'équivalence logique des deux formules, celle avant élimination et celle après élimination, se déduit des axiomes). Il existe des algorithmes qui mettent en œuvre cette élimination. Le premier, dû à Alfred Tarski[8], a une complexité non élémentaire, c'est-à-dire qui n'est pas bornée par une tour d'exponentielles ${\displaystyle 2^{2^{\dots ^{n}}}}$, et a donc un intérêt principalement historique, mais donne un exemple d'une théorie axiomatique non triviale ne vérifiant pas le premier théorème d'incomplétude de Gödel.

James Davenport et Joos Heintz ont montré en 1988 que le problème est intrinsèquement complexe : il existe une famille Φ_n de formules avec n quantificateurs, de longueur O(n) et de degré constant, telle que toute formule sans quantificateur équivalente à Φ_n doit mettre en œuvre des polynômes de degré ${\displaystyle 2^{2^{\Omega (n)}}}$ et de longueur ${\displaystyle 2^{2^{\Omega (n)}}}$, avec les notations asymptotiques O et Ω.

Le logiciel QEPCAD et la fonction Reduce de Mathematica 5[9], par exemple, proposent des implémentations d'algorithmes d'élimination des quantificateurs pour les corps réels clos.

En raison de l'existence d'algorithmes d'élimination des quantificateurs, la théorie des corps réels clos est décidable : à partir de toute formule close, on peut obtenir algorithmiquement une formule équivalente sans quantificateurs ni variables libres, donc facilement décidable.

Une autre conséquence de l'élimination des quantificateurs (indépendamment du fait qu'elle soit réalisable algorithmiquement) est que cette théorie est complète, donc tout corps réel clos a la même théorie du premier ordre que ℝ.

Le groupe multiplicatif de tout corps réel clos ${\displaystyle F}$ est la somme directe du sous-groupe ${\displaystyle \{\pm 1\}}$ et de sous-groupes isomorphes à ${\displaystyle \mathbb {Q} }$ : ${\displaystyle F^{*}\simeq \mathbb {Z} /2\mathbb {Z} \oplus \mathbb {Q} ^{(|F|)}}$[10]. En effet, 1 et –1 sont ses seuls éléments de torsion (c.-à-d. racines de l'unité), et le sous-groupe des éléments positifs (les carrés) est divisible.

Réciproquement, pour tout cardinal infini ${\displaystyle \kappa }$, il existe un corps réel clos dont le groupe multiplicatif est isomorphe à ${\displaystyle \mathbb {Z} /2\mathbb {Z} \oplus \mathbb {Q} ^{(\kappa )}}$[10]. En effet, il existe un corps algébriquement clos de caractéristique 0 et de cardinal κ, et (voir supra) un tel corps possède un sous-corps réel clos de même cardinal.

• (en) Saugata Basu, Richard Pollack et Marie-Françoise Roy, Algorithms in Real Algebraic Geometry, Berlin/New York, Springer, coll. « Algorithms and Computation in Mathematics » (n^o 10), 2003, 662 p. (ISBN 978-3-540-33099-8, lire en ligne)
• (en) Bob F. Caviness et Jeremy R. Johnson, éditeurs, Quantifier Elimination and Cylindrical Algebraic Decomposition, Springer, 1998 (ISBN 978-3-7091-9459-1)
• (en) Chen Chung Chang et Howard Jerome Keisler, Model Theory, Elsevier, 3^e éd., 1990 (ISBN 978-0-444-88054-3)
• (en) Harold Garth Dales et W. Hugh Woodin, Super-Real Fields, Clarendon Press, 1996 (ISBN 978-0-19853991-9)
• (en) Bhubaneswar Mishra (en), « Computational Real Algebraic Geometry », dans Handbook of Discrete and Computational Geometry, CRC Press, 1997 ([PDF] ou p. 743-764 de l'édition 2004 sur Google Livres)