量化子の除去

量化子除去は、数理論理学、モデル理論、理論計算機科学で使用される簡略化の概念です。非公式には、量化された文「${\displaystyle \exists x}$「 ～のような 」は「いつ～があるか」という質問と見なすことができる${\displaystyle x}$「～である 」という問いに対して、量化子のない文は、その問いへの答えと見なすことができる。^{[ 1 ]}

数式を分類する一つの方法は、量化子の量による分類である。量化子の交替が少ない数式はより単純であると考えられ、量化子のない数式が最も単純である。ある理論が量化子除去を持つとは、すべての数式に対して以下の条件が満たされることを意味する。${\displaystyle \alpha }$別の公式が存在する$\displaystyle \alpha _{QF}}$量化子がない場合、それは（この理論を法として）それと同等である。

数学の例では、1変数の2次多項式が実根を持つのは判別式が非負の場合のみである、とされています。 ^{[ 1 ]}

$${\displaystyle \exists x\in \mathbb {R} .(a\neq 0\wedge ax^{2}+bx+c=0)\ \ \Longleftrightarrow \ \ a\neq 0\wedge b^{2}-4ac\geq 0}$$

ここで、左側の文には数量詞が含まれています。${\displaystyle \exists x\in \mathbb {R} }$一方、右側の同等の文はそうではない。

量化子消去法を用いて決定可能であることが示されている理論の例としては、^{プレスバーガー算術 [ 2 ] [ 3 ] [ 4 ] [ 5 ] [ 6 ] [ 7 ] スコレム算術 [} 8 ]^{代数的閉体、実閉体[ 9 ] [ 10 ]無原子ブール代数、項}代数、^稠密線形順序[ 9 ]^{アーベル群[ 11 ]}ラドグラフ、およびプレスバーガー算術を^用いたブール^{代数やキュー}を用いた項代数など^、それらの多くの組み合わせが挙げ^られる。

順序加法群としての実数論における量化子消去はフーリエ・モツキン消去であり、実数体の理論における量化子消去はタルスキー・ザイデンベルクの定理である。^{[ 9 ]}

量化子消去法は、決定可能な理論を「組み合わせる」ことで新しい決定可能な理論が得られることを示すためにも使用できます（フェファーマン・ヴォートの定理を参照）。

ある理論に量化子除去がある場合、特定の質問に取り組むことができます。決定する方法はありますか？$\displaystyle \alpha _{QF}}$各${\displaystyle \alpha }$もしそのような方法が存在するならば、それを量化子除去アルゴリズムと呼ぶ。そのようなアルゴリズムが存在するならば、その理論の決定可能性は、量化子を含まない文の真偽を決定することに帰着する。

量化子除去には様々なモデル理論的な考え方が関連しており、様々な同値条件が存在する。

量化子消去を持つすべての一階理論はモデル完全である。逆に、普遍的帰結の理論が融合特性を持つモデル完全理論は、量化子消去を持つ。^{[ 12 ]}

理論の普遍的帰結の理論のモデル${\displaystyle T}$はまさにモデルの内部構造である${\displaystyle T}$[ ^{12 ]線形順序の理論には}量化子消去はありません。しかし、その普遍的帰結の理論には融合特性があります。

理論が量化子除去を持つことを構成的に示すには、リテラルの連言に適用された存在量化子を除去できることを示せば十分である。つまり、次の形式の各式が次のようになることを示せばよい。

$${\displaystyle \exists x.\bigwedge _{i=1}^{n}L_{i}}$$

それぞれ${\displaystyle L_{i}}$はリテラルであり、 は量化子のない式と同等です。実際、リテラルの論理積から量化子を取り除く方法がわかっていると仮定すると、${\displaystyle F}$これは量化子を含まない式なので、選言標準形で書くことができます。

$${\displaystyle \bigvee _{j=1}^{m}\bigwedge _{i=1}^{n}L_{ij},}$$

そして、

$${\displaystyle \exists x.\bigvee _{j=1}^{m}\bigwedge _{i=1}^{n}L_{ij}}$$

と同等

$${\displaystyle \bigvee _{j=1}^{m}\exists x.\bigwedge _{i=1}^{n}L_{ij}.}$$

最後に、全称量化子を排除するために

$${\displaystyle \forall xF}$$

どこ${\displaystyle F}$量化子がないため、変換します ${\displaystyle \lnot F}$選言標準形に変換し、${\displaystyle \forall xF}$ と同等${\displaystyle \lnot \exists x.\lnot F.}$

初期のモデル理論では、量化子除去法を用いて、様々な理論が決定可能性や完全性といった性質を持つことを証明した。一般的な手法は、まず理論が量化子除去を許容することを示し、その後、量化子を含まない式のみを考慮することで決定可能性や完全性を証明するというものであった。この手法は、プレスバーガー算術が決定可能であることを示すためにも用いることができる。

理論は決定可能であっても、量化子消去を許容しない場合がある。厳密に言えば、加法自然数の理論は量化子消去を許容しなかったが、加法自然数の拡張として決定可能であることが示された。理論が決定可能であり、かつその有効な式の言語が可算である場合、可算個の関係を用いて理論を拡張することで量化子消去が可能になる（例えば、理論の各式に対して、その式の自由変数を関連付ける関係記号を導入することができる）。

例:代数的に閉じた体と微分的に閉じた体のヌルシュテルンザッツ。

• 円筒代数分解
• 消去理論
• 接続詞の除去