量化記号消去

同義語：量化子消去quantifier elimination

概要

前提知識: 一階述語論理, 構造(モデル), コンパクト性定理(一階論理)

実数 $b,c$ について「$x^2+bx+c=0$ となる実数 $x$ が存在する」という条件は、判別式の条件「$b^2-4c\ge0$」と同値である。左の条件は量化記号「存在する」を含むが、右の条件は $b,c$ の多項式の符号だけで書けている。このように、ある理論のもとで、量化記号を含む論理式がいつも量化記号を含まない論理式に書き直せるとき、その理論は 量化記号消去（quantifier elimination）をもつという。量化記号消去をもつ理論では、論理式で定義される集合は「原子論理式で定まる集合の有限個の和・共通部分・補集合」の形に限られ、モデルの間の関係も原子論理式だけで調べられる。
この記事では、量化記号消去を定義し、それを示すには「存在する」を 1 つだけ含む簡単な形の論理式を扱えば足りることを証明する。そのうえで、端点のない稠密な全順序の理論 DLO が量化記号消去をもつことを書き換えで直接示す。次に、モデルの中の元の組の比較で量化記号消去を判定する方法をコンパクト性定理から証明し、これを使って代数閉体の理論 ACF が量化記号消去をもつことを示す。実閉体の量化記号消去は Tarski–Seidenbergの定理の主題であり、ここでは見出しで引く。
以下、$L$ は一階言語、構造の台集合は空でないとする（一階述語論理の記事の定義「構造」）。$\bar x=(x_1,\dots,x_n)$（$n\ge0$）は相異なる変数の組で、論理式 $\varphi$ の自由変数がすべて $\bar x$ の中にあるとき $\varphi(\bar x)$ と書く。構造 $M$ と $\bar a\in M^n$ について、$x_i$ に $a_i$ を割り当てて $\varphi$ が充足されることを $M\models\varphi(\bar a)$ と書く。$T$ は $L$ の文の集合である。

定義

量化記号のない論理式 とは、原子論理式と、恒真の論理式 $\top$・恒偽の論理式 $\bot$ から、$\lnot,\land,\lor,\to$ だけで作った論理式のことである。$\top$ と $\bot$ を加えておくのは、定数記号のない言語でも、自由変数のない量化記号のない論理式（真偽の決まった文）を作れるようにするためである。原子論理式と $\top,\bot$ およびそれらの否定を リテラル という。

T 同値と量化記号消去

論理式 $\varphi(\bar x),\psi(\bar x)$ が $T$ 同値 であるとは、$T$ のすべてのモデル $M$ とすべての $\bar a\in M^n$ について、$M\models\varphi(\bar a)$ と $M\models\psi(\bar a)$ が同値であることをいう。
$T$ が 量化記号消去をもつ（admits quantifier elimination）とは、$L$ のすべての論理式 $\varphi$ に対し、$\varphi$ と $T$ 同値で、自由変数が $\varphi$ の自由変数の中にある量化記号のない論理式 $\psi$ が存在することをいう。
$L$ 構造 $M$ が量化記号消去をもつとは、$M$ で真な文の全体 $\operatorname{Th}(M)$ が量化記号消去をもつことをいう。

自由変数についての条件により、とくに文（自由変数のない論理式）は、量化記号のない文と $T$ 同値になる。つまり $T$ のモデルでの文の真偽は、量化記号のない文の真偽だけで決まる。この点は後の節「量化記号消去の帰結」で完全性を導くときに使う。
量化記号消去は、どの記号を言語に含めるかに強く依存する。同じ実数の集合でも、順序 $<$ を含む言語では量化記号消去をもつが、環の言語 $\{+,-,\cdot,0,1\}$ では量化記号消去をもたない（後の ex-qe-counterexamples）。
元の組を比べるときは、それが満たす量化記号のない論理式の全体を使う。

量化記号のない型

$L$ 構造 $M$ と $\bar a\in M^n$ に対し、$M\models\psi(\bar a)$ となる量化記号のない論理式 $\psi(\bar x)$ の全体を $\bar a$ の 量化記号のない型 といい、$\operatorname{qftp}^M(\bar a)$ と書く。

量化記号のない論理式 $\psi$ ごとに、$\psi$ か $\lnot\psi$ のどちらか一方だけが $\operatorname{qftp}^M(\bar a)$ に属する。$n\ge1$ のとき、$\bar a\in M^n$ と $\bar b\in N^n$ の量化記号のない型が等しいことは、$a_i\mapsto b_i$ が、$\bar a$ が生成する部分構造から $\bar b$ が生成する部分構造への同型写像に延びることと同値である。生成された部分構造の元は項の値 $t^M[\bar a]$ であり（構造(モデル) の記事の定理「生成された部分構造」）、$t^M[\bar a]\mapsto t^N[\bar b]$ が矛盾なく定まって単射であることは等式 $t=s$ の真偽が一致することから、関数と関係を保つことは原子論理式の真偽が一致することから分かるからである。

例

代数閉体と実閉体での消去

体では、$\exists y\,(x\cdot y=1)$ は $\lnot(x=0)$ と同値である。これはどの体でも成り立つので、体の理論のもとで $T$ 同値である。
代数閉体では、$\exists y\,(a\cdot y\cdot y+b\cdot y+c=0)$ は $\lnot(a=0)\lor\lnot(b=0)\lor(c=0)$ と同値である。$a\ne0$ なら 2 次式は根をもち、$a=0$、$b\ne0$ なら 1 次式の根 $-c/b$ があり、$a=b=0$ なら式は $c=0$ になるからである。
実閉体では、同じ論理式は判別式を使った条件と同値になる（Tarski–Seidenbergの定理の記事の例「2 次方程式の実数解の存在」）。
有理数体 $\mathbb{Q}$ では、$\exists y\,(y\cdot y=x)$（$x$ が平方数である）は、環の言語の量化記号のない論理式と同値にならない（後の ex-qe-counterexamples）。

2 と 3 を比べると、根の存在が代数閉体では係数が $0$ かどうかだけで決まるのに対し、実閉体では不等号が必要になる。量化記号消去の形は、理論が「どのような条件で解が存在するか」をどう決めているかを映している。

還元：1 つの存在量化記号で足りる

存在量化記号 1 つへの還元

$T$ が量化記号消去をもつためには、次が成り立てば十分である：リテラルの連言 $\theta$ と変数 $y$ のすべてについて、$\exists y\,\theta$ は、自由変数が $\exists y\,\theta$ の自由変数の中にある量化記号のない論理式と $T$ 同値である。

要点：論理式の組み立て方についての帰納法で示す。結合子はそのまま通り、$\exists y$ は中身を選言標準形にして選言の各項に分配すれば仮定の形になり、$\forall y$ は $\lnot\exists y\lnot$ に直す。

詳しい証明を開く

論理式 $\varphi$ の組み立て方についての帰納法で、$\varphi$ と $T$ 同値で $\operatorname{FV}(\psi)\subset\operatorname{FV}(\varphi)$ を満たす量化記号のない $\psi$ があることを示す（$\operatorname{FV}$ は自由変数の集合）。

原子論理式は自分自身をとればよい。$\varphi=\lnot\varphi_1$、$\varphi_1\land\varphi_2$、$\varphi_1\lor\varphi_2$、$\varphi_1\to\varphi_2$ なら、帰納法の仮定で得た $\psi_1,\psi_2$ を同じ結合子でつなげばよい。$T$ 同値は充足関係の定義により結合子で保たれる。

$\varphi=\exists y\,\varphi_1$ とする。帰納法の仮定で $\varphi_1$ と $T$ 同値な量化記号のない $\psi_1$ をとる。命題論理の選言標準形により、$\psi_1$ は、$\psi_1$ に現れる原子論理式のリテラルの連言 $\theta_1,\dots,\theta_k$ の選言 $\theta_1\lor\cdots\lor\theta_k$ と論理的に同値である（$k=0$ のときは $\bot$）。充足関係の定義から、$T$ のモデル $M$ と割り当てについて $$ M\models\exists y\,\varphi_1\iff M\models\exists y\,\psi_1\iff M\models\exists y\,\theta_1\lor\cdots\lor\exists y\,\theta_k $$ である（「ある $c$ で $\theta_1$ または … または $\theta_k$」は「$\theta_1$ を満たす $c$ がある、または …」と同じ）。仮定により、各 $\exists y\,\theta_j$ は $\operatorname{FV}(\chi_j)\subset\operatorname{FV}(\exists y\,\theta_j)\subset\operatorname{FV}(\psi_1)\setminus\{y\}\subset\operatorname{FV}(\varphi)$ を満たす量化記号のない $\chi_j$ と $T$ 同値である。よって $\chi_1\lor\cdots\lor\chi_k$（$k=0$ なら $\bot$）が求めるものである。

$\varphi=\forall y\,\varphi_1$ なら、$\varphi$ は $\lnot\exists y\,\lnot\varphi_1$ と論理的に同値である。帰納法の仮定で $\lnot\varphi_1$ は $\lnot\psi_1$ と $T$ 同値なので、上と同じ議論で $\exists y\,\lnot\varphi_1$ と $T$ 同値な量化記号のない $\chi$ がとれ、$\lnot\chi$ が求めるものである。$\square$

逆に、$T$ が量化記号消去をもてば、この補題の条件はもちろん成り立つ。したがって量化記号消去を示すには、「リテラルの連言を満たす $y$ が存在する」という条件を量化記号なしで書き直せばよい。

稠密な全順序

端点のない稠密な全順序の理論

言語 $\{<\}$（2 項関係記号 1 つ）の次の文からなる理論を DLO という。

$\forall x\,\lnot(x< x)$、$\forall x\,\forall y\,\forall z\,(x< y\land y< z\to x< z)$、$\forall x\,\forall y\,(x< y\lor x=y\lor y< x)$（全順序）。
$\forall x\,\forall y\,(x< y\to\exists z\,(x< z\land z< y))$（稠密）。
$\forall x\,\exists y\,(y< x)$、$\forall x\,\exists y\,(x< y)$（端点がない）。

$(\mathbb{Q},<)$ と $(\mathbb{R},<)$ は DLO のモデルである。

DLO の量化記号消去

DLO は量化記号消去をもつ。

lem-qe-reduction により、リテラルの連言 $\theta$ について、$\exists y\,\theta$ が DLO 同値な量化記号のない論理式で、自由変数が $\exists y\,\theta$ の自由変数の中にあるものをもつことを示せばよい。以下の書き換えはどれも、DLO のどのモデルでも同値な論理式への書き換えであり、新しい自由変数を持ち込まない。
段 1（否定を外す）． $\theta$ が $\bot$ か $\lnot\top$ を含めば $\exists y\,\theta$ は $\bot$ と同値であり、$\top$ と $\lnot\bot$ は取り除ける。全順序では $\lnot(u< v)$ は $v< u\lor u=v$ と、$\lnot(u=v)$ は $u< v\lor v< u$ と同値である。これらを代入して分配法則で展開すると、$\theta$ は原子論理式の連言 $\theta_1,\dots,\theta_k$ の選言と同値になり、$\exists y\,\theta$ は $\exists y\,\theta_1\lor\cdots\lor\exists y\,\theta_k$ と同値になる。よって $\theta$ は原子論理式 $u< v$、$u=v$（$u,v$ は変数）の連言としてよい。
段 2（$y$ を含まない部分を外へ出す）． $\theta=\theta'\land\theta''$ で、$\theta''$ は $y$ を含まない原子論理式の連言、$\theta'$ は $y$ を含む原子論理式の連言とすると、$\exists y\,\theta$ は $(\exists y\,\theta')\land\theta''$ と同値である。$\theta'$ の中の $y=y$ は取り除き、$y< y$ があれば $\exists y\,\theta'$ は $\bot$ と同値である。
段 3（等式がある場合）． $\theta'$ が $y$ と別の変数 $x$ の等式 $y=x$ または $x=y$ を含めば、$\exists y\,\theta'$ は、$\theta'$ の $y$ をすべて $x$ に置き換えた量化記号のない論理式と同値である（$y$ の値は $x$ の値に限られる）。
段 4（不等式だけの場合）． 残るのは、$y$ と異なる変数 $u_i$（$i\in I$）、$v_j$（$j\in J$）について
$$ \theta'=\bigwedge_{i\in I}u_i< y\ \land\ \bigwedge_{j\in J}y< v_j $$
の形である。このとき、DLO のモデル $M$ で
$$ \exists y\,\theta'\iff\bigwedge_{i\in I,\ j\in J}u_i< v_j $$
が成り立つ（右辺は $I$ か $J$ が空なら $\top$）。左から右は推移律による。右から左を示す。$I,J$ がともに空でなければ、有限個の元 $u_i$ の最大のもの $u$ と、$v_j$ の最小のもの $v$ をとる（全順序なので存在する）。仮定から $u< v$ であり、稠密性から $u< c< v$ となる $c\in M$ があって、$c$ が $\theta'$ を満たす。$J$ だけが空なら、端点がないことから $u< c$ となる $c$ があり、$I$ だけが空なら同様である。$I,J$ がともに空なら、$M$ は空でないので任意の $c$ でよい。$\square$

この証明は、DLO のどの公理がどの段で使われたかを示している。全順序の公理は段 1（否定の書き換え）と段 4 の最大・最小に、稠密性と端点がないことは段 4 の解の存在に使われた。稠密性か端点がないことを外すと、量化記号消去は成り立たなくなる（ex-qe-counterexamples）。

DLO の完全性と定義可能集合

DLO の任意の 2 つのモデルは同じ文を満たす。とくに $(\mathbb{Q},<)$ と $(\mathbb{R},<)$ は初等同値である。
DLO のモデル $M$ の部分集合で、$M$ の元をパラメータとする論理式で定義されるものは、有限個の点と開区間（端が $\pm\infty$ のものを含む）の和である。

1：言語 $\{<\}$ には定数記号がないので、量化記号のない文は $\top$ と $\bot$ から結合子だけで作った文であり、真偽はモデルによらない。thm-qe-dlo により、どの文もそのような文と DLO 同値なので、真偽はモデルによらない。
2：$D=\{c\in M\mid M\models\varphi(c,\bar b)\}$ とする。thm-qe-dlo により $\varphi(y,\bar z)$ は量化記号のない $\psi(y,\bar z)$ と DLO 同値である。$\psi(y,\bar b)$ の原子論理式で $y$ を含むものは $y< b_k$、$b_k< y$、$y=b_k$、$y< y$、$y=y$ の形なので、$b_1,\dots,b_m$ を小さい順に並べて $M$ を点 $b_k$ と開区間に分けると、各点と各開区間の上で $\psi(y,\bar b)$ の真偽は一定である。$\square$

1 は Löwenheim–Skolemの定理の記事の例「稠密な線形順序と代数閉体」でも、可算なモデルがすべて同型であることと Łoś–Vaught の判定法から導かれている。量化記号消去による上の証明は、モデルの同型を使わずに書き換えだけで完全性を示している。2 は、$(\mathbb{Q},<)$ と $(\mathbb{R},<)$ が o-極小構造であること（同記事の命題「稠密な順序は o-極小」）の別証明にあたる。

元の組の比較による判定法

DLO では書き換えを直接実行できたが、代数閉体のように書き換えの具体的な手順が複雑な理論では、次の判定法が便利である。モデルの中で、量化記号のない性質が同じ元の組は、すべての性質が同じであることを示せばよい。

量化記号消去の判定法

論理式 $\varphi(\bar x)$（$\bar x=(x_1,\dots,x_n)$、$n\ge0$）について、次は同値である。

$\varphi$ は、自由変数が $\bar x$ の中にある量化記号のない論理式と $T$ 同値である。
$T$ の任意のモデル $M,N$ と、$\operatorname{qftp}^M(\bar a)=\operatorname{qftp}^N(\bar b)$ を満たす任意の $\bar a\in M^n$、$\bar b\in N^n$ について、$M\models\varphi(\bar a)$ ならば $N\models\varphi(\bar b)$ である。

1 ⇒ 2：$\varphi$ と $T$ 同値な量化記号のない $\psi(\bar x)$ をとる。$M\models\varphi(\bar a)$ なら $M\models\psi(\bar a)$、すなわち $\psi\in\operatorname{qftp}^M(\bar a)=\operatorname{qftp}^N(\bar b)$ なので $N\models\psi(\bar b)$、よって $N\models\varphi(\bar b)$ である。
2 ⇒ 1：新しい定数記号 $c_1,\dots,c_n$ を加えた言語を $L'$ とし、$L$ の論理式 $\chi(\bar x)$ の $x_i$ に $c_i$ を代入した $L'$ の文を $\chi(\bar c)$ と書く。$L'$ 構造は、$L$ 構造 $M$ と $c_i$ の値の組 $\bar a\in M^n$ の対 $(M,\bar a)$ と同じものであり、$(M,\bar a)\models\chi(\bar c)$ と $M\models\chi(\bar a)$ は同値である（一階述語論理の記事の補題「代入補題」）。
$$ \Gamma:=\bigl\{\psi(\bar x)\text{ 量化記号のない論理式（自由変数は }\bar x\text{ の中）}\ \big|\ T\text{ のすべてのモデル }M\text{ と }\bar a\in M^n\text{ で、}M\models\varphi(\bar a)\Rightarrow M\models\psi(\bar a)\bigr\} $$
とおく。
段 1． $L'$ の文の集合 $T\cup\{\psi(\bar c)\mid\psi\in\Gamma\}\cup\{\lnot\varphi(\bar c)\}$ はモデルをもたないことを示す。モデル $(N,\bar b)$ があったとし、$\Delta:=\operatorname{qftp}^N(\bar b)$ とおく。$\Sigma:=T\cup\{\delta(\bar c)\mid\delta\in\Delta\}\cup\{\varphi(\bar c)\}$ がモデル $(M,\bar a)$ をもったとすると、$\Delta\subset\operatorname{qftp}^M(\bar a)$ である。量化記号のない $\psi$ ごとに $\psi$ か $\lnot\psi$ が $\Delta$ に属し、両方が $\operatorname{qftp}^M(\bar a)$ に属することはないので、$\operatorname{qftp}^M(\bar a)=\Delta=\operatorname{qftp}^N(\bar b)$ である。$M\models\varphi(\bar a)$ なので 2 により $N\models\varphi(\bar b)$ となり、$N\models\lnot\varphi(\bar b)$ に反する。よって $\Sigma$ はモデルをもたず、コンパクト性定理(一階論理) により、ある $\delta_1,\dots,\delta_k\in\Delta$（$k\ge0$）について $T\cup\{\delta_1(\bar c),\dots,\delta_k(\bar c),\varphi(\bar c)\}$ がモデルをもたない。$\delta:=\delta_1\land\cdots\land\delta_k$（$k=0$ なら $\top$）とおくと、$T$ のモデル $M$ と $\bar a$ について $M\models\varphi(\bar a)$ なら $M\models\lnot\delta(\bar a)$ であり、$\lnot\delta\in\Gamma$ となる。一方 $\delta_i\in\Delta$ なので $N\models\delta(\bar b)$ であり、$(N,\bar b)$ が $\{\psi(\bar c)\mid\psi\in\Gamma\}$ を満たすことに反する。
段 2． 段 1 とコンパクト性定理により、ある $\psi_1,\dots,\psi_m\in\Gamma$ について $T\cup\{\psi_1(\bar c),\dots,\psi_m(\bar c),\lnot\varphi(\bar c)\}$ がモデルをもたない。$\psi:=\psi_1\land\cdots\land\psi_m$（$m=0$ なら $\top$）は自由変数が $\bar x$ の中にある量化記号のない論理式で、$T$ のモデル $M$ と $\bar a$ について、$M\models\psi(\bar a)$ なら $M\models\varphi(\bar a)$ である。逆に $M\models\varphi(\bar a)$ なら、各 $\psi_i\in\Gamma$ により $M\models\psi(\bar a)$ である。よって $\varphi$ と $\psi$ は $T$ 同値である。$\square$

$n=0$ の場合、2 は「量化記号のない文を同じように満たす $T$ の 2 つのモデルは、文 $\varphi$ も同じように満たす」と読む。lem-qe-reduction と合わせると、$T$ が量化記号消去をもつことは、次の性質と同値である：$T$ の任意のモデル $M,N$、量化記号のない型が等しい $\bar a\in M^n$、$\bar b\in N^n$、リテラルの連言 $\theta(\bar x,y)$ について、$M$ に $\theta(\bar a,c)$ を満たす $c$ があれば、$N$ にも $\theta(\bar b,d)$ を満たす $d$ がある。

量化記号消去の帰結

$T$ は量化記号消去をもつとする。

（モデル完全性）$M,N$ が $T$ のモデルで $M$ が $N$ の部分構造なら、$M$ は $N$ の初等部分モデルである。
（完全性）$T$ がモデルをもち、$T$ のどの 2 つのモデルも同じ量化記号のない文を満たすなら、$T$ の任意の 2 つのモデルは初等同値である。

1：論理式 $\varphi(\bar x)$ と $\bar a\in M^n$ をとり、$\varphi$ と $T$ 同値な量化記号のない $\psi(\bar x)$ をとる。包含写像は埋め込みなので、量化記号のない論理式の真偽を保つ（初等埋め込みの記事の命題「埋め込みが保つ式」の (i)）。よって $M\models\varphi(\bar a)\iff M\models\psi(\bar a)\iff N\models\psi(\bar a)\iff N\models\varphi(\bar a)$ である。
2：文 $\sigma$ は量化記号のない文 $\psi$ と $T$ 同値であり、$\psi$ の真偽は仮定によりモデルによらないので、$\sigma$ の真偽もモデルによらない。$\square$

2 の結論は、$T$ が完全な理論であるということである。2 の仮定は、言語が定数記号をもたないとき（量化記号のない文は $\top,\bot$ から作られる）や、ある構造が $T$ のすべてのモデルに埋め込めるときに満たされる。

代数閉体

環の言語 $L_{\mathrm{ring}}=\{+,-,\cdot,0,1\}$（$-$ は 1 項の符号反転）を使う。項は整数係数の多項式を表すので、原子論理式 $t_1=t_2$ は、どの可換環でも $p=0$（$p=t_1-t_2\in\mathbb{Z}[\bar x]$）と同値である。体の公理に、各 $m\ge1$ についての文
$$ \forall a_0\cdots\forall a_{m-1}\ \exists y\ \bigl(y^m+a_{m-1}y^{m-1}+\cdots+a_1y+a_0=0\bigr) $$
を加えた理論を ACF（代数閉体の理論）という。そのモデルはちょうど代数閉体である。標数を $p$（素数または $0$）に定める文を加えたものを $\mathrm{ACF}_p$ と書く。

代数閉体の量化記号消去

ACF は量化記号消去をもつ。

thm-qe-test の後の注意により、次を示せばよい：$M,N$ を代数閉体、$\bar a\in M^n$ と $\bar b\in N^n$ を量化記号のない型が等しい組、$\theta(\bar x,y)$ をリテラルの連言とし、$c\in M$ が $M\models\theta(\bar a,c)$ を満たすとき、$N\models\theta(\bar b,d)$ となる $d\in N$ がある。リテラル $\top$、$\lnot\bot$ は取り除け、$\bot$、$\lnot\top$ は $c$ があるので現れない。よって整数係数の多項式 $p_i,q_j\in\mathbb{Z}[\bar x,y]$ により
$$ \theta(\bar x,y)\ \text{は}\ \bigwedge_i p_i(\bar x,y)=0\ \land\ \bigwedge_j\lnot\bigl(q_j(\bar x,y)=0\bigr)\ \text{と同値} $$
としてよい。
段 1（$\bar a$ と $\bar b$ が生成する体の同型）． $R_a:=\{r(\bar a)\mid r\in\mathbb{Z}[\bar x]\}$ は $M$ の部分環で、$R_b$ も同様とする。整数係数の多項式 $r$ について、$r(\bar a)=0$ は量化記号のない論理式 $r(\bar x)=0$ が $\bar a$ で成り立つことなので、仮定から $r(\bar a)=0\iff r(\bar b)=0$ である。よって $\sigma(r(\bar a)):=r(\bar b)$ は矛盾なく定まる単射で（$r(\bar a)=r'(\bar a)\iff(r-r')(\bar a)=0\iff r(\bar b)=r'(\bar b)$）、環の同型 $R_a\to R_b$ である。$R_a,R_b$ は体の部分環なので整域であり、$\sigma$ は商体の同型 $\sigma\colon F_a\to F_b$ に延びる（$F_a\subset M$、$F_b\subset N$）。$g\in\mathbb{Z}[\bar x,y]$ について、$g(\bar a,Y)\in F_a[Y]$ の係数に $\sigma$ を施したものは $g(\bar b,Y)$ である。
段 2（$c$ が $F_a$ 上代数的な場合）． ある $i$ で $p_i(\bar a,Y)$ が $F_a[Y]$ の零でない多項式なら、$c$ はその根なので $F_a$ 上代数的である。$c$ の $F_a$ 上の最小多項式を $P$ とし、係数に $\sigma$ を施した $P^\sigma\in F_b[Y]$ の根 $d\in N$ を 1 つとる（$P^\sigma$ は定数でなく、$N$ は代数閉体）。環準同型 $\tau_0\colon F_a[Y]\to N$、$g\mapsto g^\sigma(d)$ の核は $P$ を含み、$1$ を含まない。$(P)$ は $F_a[Y]$ の極大イデアルなので核は $(P)$ に等しく、$\tau_0$ から単射 $F_a[Y]/(P)\to N$ が得られる。$F_a(c)\cong F_a[Y]/(P)$（$c\leftrightarrow Y$）と合成して、$\sigma$ を延長する単射な環準同型 $\tau\colon F_a(c)\to N$ で $\tau(c)=d$ となるものを得る。$g\in\mathbb{Z}[\bar x,y]$ について $\tau(g(\bar a,c))=g(\bar b,d)$ なので、$p_i(\bar b,d)=\tau(0)=0$、$q_j(\bar b,d)=\tau(q_j(\bar a,c))\ne0$（$\tau$ は単射）である。
段 3（どの $p_i(\bar a,Y)$ も零多項式の場合）． $p_i(\bar a,Y)$ の係数は整数係数の多項式 $r$ による $r(\bar a)$ の形で、それがすべて $0$ なので $r(\bar b)=0$ であり、$p_i(\bar b,Y)$ も零多項式である。一方 $q_j(\bar a,c)\ne0$ なので $q_j(\bar a,Y)$ は零多項式でなく、ある係数 $r(\bar a)\ne0$ に対して $r(\bar b)\ne0$ だから、$q_j(\bar b,Y)$ も零でない多項式であり、$N$ の中の根は有限個である。代数閉体は無限体である（代数閉体の記事の命題「有限体の非代数閉性」）ので、どの $q_j(\bar b,Y)$ の根でもない $d\in N$ がとれ、$N\models\theta(\bar b,d)$ となる。$\square$

証明の段 2 は「$c$ を満たす代数的な条件は、同型な体の上で同じ形の根で実現できる」こと、段 3 は「零でない多項式の根は有限個なので、避ける条件は無限体でいつでも満たせる」ことを使っている。代数閉体という仮定は段 2 の根 $d$ の存在に、無限であることは段 3 に効いている。

代数閉体の理論の帰結

素数または $0$ である $p$ について、$\mathrm{ACF}_p$ の任意の 2 つのモデルは初等同値である。
代数閉体 $K\subset K'$ について、$K$ は $K'$ の初等部分モデルである。
代数閉体 $K$ の部分集合で、$K$ の元をパラメータとする論理式で定義されるものは、有限集合か、有限集合の補集合である。

1：$L_{\mathrm{ring}}$ の量化記号のない文は、$\top,\bot$ と整数を表す項の等式 $m\cdot1=0$（$m\in\mathbb{Z}$）から作られ、その真偽は標数だけで決まる。よって prop-qe-consequences の 2 による。2：prop-qe-consequences の 1 による。3：定義する論理式 $\varphi(y,\bar z)$ を thm-qe-acf により量化記号のない $\psi(y,\bar z)$ に取り替える。パラメータ $\bar e$ を代入すると、$\psi(y,\bar e)$ の原子論理式は $g(y)=0$（$g\in K[y]$）の形で、$g$ が零多項式なら $K$ 全体を、そうでなければ有限集合を定める。有限集合と補有限集合の全体は有限個の和・共通部分・補集合で閉じている。$\square$

1 は Löwenheim–Skolemの定理の記事の例「稠密な線形順序と代数閉体」が、非可算な濃度での範疇性と Łoś–Vaught の判定法から導いた結果の別証明である。2 は Lefschetz の原理（移行原理）ともよばれ、BPR16 Theorem 1.38（p. 36）が述べている。3 は BPR16 Corollary 1.36（p. 36）にある。1 つの代数閉体の中でパラメータを許す形の量化記号消去は BPR16 Theorem 1.34（p. 36）であり、同書は構成可能集合の射影が構成可能であること（Theorem 1.32、p. 35）から導いている。幾何学の言葉では、これは Chevalleyの定理と同じ内容である。

実閉体

順序環の言語 $\{+,-,\cdot,0,1,<\}$ で、実閉体の理論 RCF も量化記号消去をもつ。Tarski–Seidenbergの定理の記事の定理「Tarski–Seidenbergの定理（量化記号消去）」は、1 つの実閉体 $R$ の中で、整数係数の論理式が整数係数の量化記号のない論理式と同値であることを述べている。同値であるという主張は整数係数の文 $\forall\bar x\,(\varphi\leftrightarrow\psi)$ が $R$ で真ということであり、同記事が挙げる Tarski–Seidenberg の原理（整数係数の文は、ある実閉体で真ならすべての実閉体で真。BPR16 Theorem 2.98・2.99、p. 81）により、すべての実閉体で真になる。この記事では証明しない。
代数閉体との違いは、根の存在が等式だけで決まらず、不等号が必要になる点にある。実数の環の言語の構造 $(\mathbb{R},+,-,\cdot,0,1)$ は量化記号消去をもたない（次の節）。順序 $<$ は環の言語で $x< y\iff\exists z\,(z\ne0\land y-x=z^2)$ と定義できるので、言語に $<$ を加えても定義できる集合は変わらないが、量化記号なしで書ける集合が増える。

反例：条件を外すと成り立たない

外す条件	反例	成り立たなくなること
端点がない（DLO）	端点のある稠密な全順序 $([0,1],<)$	量化記号消去：$\forall y\,\lnot(y< x)$（$x$ は最小元）
稠密（DLO）	端点のない稠密でない全順序 $(\mathbb{Z},<)$	量化記号消去：$\exists y\,(x< y\land y< z)$
代数閉（ACF）	有理数体 $(\mathbb{Q},+,-,\cdot,0,1)$	量化記号消去：$\exists y\,(y\cdot y=x)$
言語に順序がある（RCF）	実数体 $(\mathbb{R},+,-,\cdot,0,1)$	量化記号消去：$\exists y\,(y\cdot y=x)$

反例の確かめ

1 行目：自由変数が $x$ だけの、言語 $\{<\}$ の量化記号のない論理式は、$x< x$、$x=x$、$\top$、$\bot$ から作られる。全順序ではこれらの真偽は $x$ の値によらないので、そのような論理式は $[0,1]$ のすべての元で真か、すべての元で偽である。しかし $\forall y\,\lnot(y< x)$ は $x=0$ で真、$x=1$ で偽である。
2 行目：自由変数が $x,z$ の量化記号のない論理式は、$x< z$、$z< x$、$x=z$ などの原子論理式から作られ、$(x,z)=(0,1)$ と $(0,2)$ ではどの原子論理式の真偽も同じである。しかし $\exists y\,(x< y\land y< z)$ は $(0,1)$ で偽（$0$ と $1$ の間に整数はない）、$(0,2)$ で真である。
3・4 行目：$K=\mathbb{Q}$ または $\mathbb{R}$ とする。自由変数が $x$ だけの、環の言語の量化記号のない論理式は、$\top,\bot$ と $p(x)=0$（$p\in\mathbb{Z}[x]$）から作られる。$K$ の標数は $0$ なので、零でない整数係数の多項式は $K[x]$ でも零でなく、$p(x)=0$ は $K$ 全体か有限集合を定める。よってそのような論理式が定める集合は、有限集合か有限集合の補集合である。一方 $\exists y\,(y\cdot y=x)$ が定める平方の全体は、$\mathbb{Q}$ ではすべての $n^2$ を含み、補集合はすべての負の数を含むので、どちらも無限集合である。$\mathbb{R}$ では $[0,\infty)$ とその補集合 $(-\infty,0)$ で、どちらも無限集合である。

1・2 行目は、DLO の証明の段 4 で使った端点がないこと・稠密性が、量化記号消去に欠かせないことを示している。3 行目は、代数閉体の証明の段 2 で使った根の存在が欠かせないことを示す。4 行目は、同じ構造でも言語によって量化記号消去が成り立つかどうかが変わることを示す。実数体は順序環の言語では量化記号消去をもつ（前の節）。