实闭域

形式实域

假设所论之域的特征数皆为零。若在一个域${\displaystyle F}$ 中，${\displaystyle -1}$ 无法写成平方和（表法：${\displaystyle -1\neq \sum F^{2}}$ ），则称${\displaystyle F}$ 是形式实的。

每个有序域都是形式实域；形式实的定义本身不涉及序结构，但借由实闭包的存在性可证明每个形式实域皆带序结构。

实封闭域

一个实封闭域${\displaystyle F}$ 若满足下列等价条件，则称之实封闭域：

• ${\displaystyle F}$ 上存在一个序结构，使得其中每个正元素皆可表为平方，且任何奇数次多项式都有根。
• ${\displaystyle F}$ 上存在一个序结构，使之满足中间值定理。
• 对任意${\displaystyle a\in F}$ ，或者${\displaystyle a\in F^{2}}$ 或者${\displaystyle -a\in F^{2}}$ ；且任何奇数次多项式都有根。
• ${\displaystyle F}$ 非代数封闭，而${\displaystyle F({\sqrt {-1}})}$ 代数封闭。
• 若${\displaystyle F'\supset F}$ ，${\displaystyle F'}$ 是形式实的，则${\displaystyle F'=F}$ 。

我们可以纯以代数性质定义实封闭域，并由${\displaystyle a>0\Leftrightarrow a\in F^{2},a\neq 0}$ 得到唯一的序结构。

对任何形式实域${\displaystyle F}$ ，都存在代数扩张${\displaystyle R\subset F}$ ，使得${\displaystyle R}$ 是实封闭的。我们称${\displaystyle R}$ 是${\displaystyle F}$ 的一个实闭包。实闭包并不唯一。

若在${\displaystyle F}$ 上固定一个序结构，并要求${\displaystyle R}$ 的序结构与之相容；则此时实闭包${\displaystyle R}$ 存在并唯一，且${\displaystyle \mathrm {Aut} (R/F)=\{\mathrm {id} _{R}\}}$ 。

• 实数域${\displaystyle \mathbb {R} }$ 
• ${\displaystyle \mathbb {R} \cap \mathbb {Q} ^{\mathrm {alg} }}$ ；它是${\displaystyle \mathbb {Q} }$ 的实闭包。
• 可计算数
• Puiseux级数

实封闭域的研究首先由数学家展开，随后引起了逻辑学家的兴趣。采用形式语言${\displaystyle {\mathcal {L}}:=\langle +,-,\cdot ,>\rangle }$ ，设${\displaystyle \mathrm {RCF} }$ 为实封闭域（带序结构）的${\displaystyle {\mathcal {L}}}$ -一阶理论，塔斯基证明了${\displaystyle \mathrm {RCF} }$ 上有量词消去；因此任两个${\displaystyle \mathrm {RCF} }$ 的模型都是初等等价的。一方面，我们可运用${\displaystyle \mathbb {R} }$ 上的特有工具（微积分、拓扑等等）证明一般实封闭域上的一阶句子；另一方面，则可透过适当的域扩张解决${\displaystyle \mathbb {R} }$ 上的问题，后一方向上最著名的成就是 Abraham Robinson 对希尔伯特第十七问题的证明。

如果改采形式语言${\displaystyle {\mathcal {L}}^{-}:=\langle +,-,\cdot \rangle }$ ，并取实封闭域的代数定义${\displaystyle \mathrm {RCF} ^{-}}$ ，此时则无法消去量词（在${\displaystyle \mathrm {RCF} ^{-}}$ 中考虑公式${\displaystyle \exists y\;y=x^{2}}$ ）。

设${\displaystyle R}$ 是实封闭域，换言之${\displaystyle R\models _{\mathcal {L}}\mathrm {RCF} }$ ，根据${\displaystyle \mathrm {RCF} }$ 上的量词消去，${\displaystyle R}$ 上的可定义集只是有限多个线段与孤立点的并集。此性质称作O-极小性，它较量词消去为弱，却是研究${\displaystyle R^{n}}$ 上可定义集的几何构造之关键。

量词消去也蕴含${\displaystyle \mathrm {RCF} }$ 的可判定性，然而塔斯基给出的算法其复杂度过高，并不实用。

若承认广义连续统假设，则可进一步以超积描述实封闭域的性状。

• Chang, Chen Chung and Keisler, H. Jerome: Model Theory, North-Holland, 1989.
• H. Garth Dales and W. Hugh Woodin: Super-Real Fields, Clarendon Press, 1996.
• Computational Real Algebraic Geometry, Bhubaneswar Mishra, Handbook of Discrete and Computational Geometry, CRC Press, 1997 (Postscript 版本 （页面存档备份，存于互联网档案馆）); 亦见 2004 edition, p. 743, ISBN 1-58488-301-4
• Saugata Basu, Richard Pollack and Marie-Françoise Roy, Algorithms in real algebraic geometry, Springer, Algorithms and computation in mathematics, 2003, ISBN 3540330984 (在线版本)
• Bob F. Caviness, Jeremy R. Johnson, editors, Quantifier elimination and cylindrical algebraic decomposition, Springer, 1998, ISBN 3211827943