実閉体
実閉体の理論は初めは代数学の中で発展したものだけれども、重要な示唆はモデル理論からもたらされた。順序体の公理系に
任意の正元が平方根を持つことを要請する公理
任意の奇数次多項式が少なくとも一つの根を持つことを要請する公理図式
を加えることにより、一階の理論が得られる。Tarski (1951) は、半順序環(英語版)に関する一階の言語(二項述語記号 "=", "≤", 加法、減法、乗法の演算および定数記号 0, 1 からなる)において、実閉体の理論が 量限定子消去(英語版)を許すことを示した。このことのもっとも重要なモデル理論的帰結は、実閉体の理論が完全(英語版)、o-極小(英語版)かつ決定可能なることである。
決定可能性が意味するのは少なくとも一つの決定手順が存在すること、すなわち実閉体に関する一階言語で書かれた文が真であるかどうかを決定するためのwell-definedなアルゴリズムが存在することである。ユークリッド幾何学(角度の決定可能性は除く)もまた実体の公理のモデルであって、したがって決定可能である。
この決定手順が「実用的」であるかは問わない。実閉体に対する決定手順は何れも計算量が極めて大きいことが知られているから、非常に単純な問題を除けば実際の実行時間は極めて長くなりうる。
タルスキーのアルゴリズムは量限定子消去(英語版)が複雑性クラス NONELEMENTARY(英語版) に属する可能性を示唆している。