数量詞の除去

量指定子除去は、数理論理学、モデル理論、理論計算機科学において用いられる単純化の概念である。非公式には、「…となるような」という量指定子付きの文は、「…となるようなものはいつ存在するのか？」という問いとみなすことができ、量指定子のない文はその問いへの答えとみなすことができる。^[1]${\displaystyle \exists x}$ ${\displaystyle x}$

論理式を分類する方法の一つに、量化の程度があります。量化子の交替の深さが少ない論理式はより単純であると考えられ、量化子のない論理式が最も単純です。ある理論が量化子除去を持つとは、任意の論理式に対して、それと等価な量化子のない別の論理式が存在することを意味します（この理論を法として）。 ${\displaystyle \alpha}$ ${\displaystyle \alpha_{QF}}$

例

数学の例では、一変数二次多項式が実根を持つのは、判別式が非負の場合のみである。^[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]} 原子なし ブール代数、項代数、稠密線型順序、^[7] アーベル群、^[9] ラドグラフ、およびそれらの多くの組み合わせ（プレスブルガー算術を含むブール代数、キューを含む項代数など）がある。

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

量指定子の除去は、決定可能理論を「組み合わせる」ことで新しい決定可能理論が得られることを示すためにも使用できます( Feferman-Vaught の定理を参照)。

アルゴリズムと決定可能性

理論に量指定子除去法がある場合、「それぞれ を決定する方法はあるか？」という具体的な疑問に答えることができます。そのような方法がある場合、それを量指定子除去アルゴリズムと呼びます。そのようなアルゴリズムがある場合、理論の決定可能性は、量指定子のない文の真偽を決定することに帰着します。量指定子のない文には変数がないため、特定の理論におけるその妥当性は多くの場合計算可能であり、量指定子除去アルゴリズムを使用して文の妥当性を決定できます。 ${\displaystyle \alpha_{QF}}$ ${\displaystyle \alpha}$

関連概念

さまざまなモデル理論的なアイデアが量限定子の除去に関連しており、さまざまな同等の条件が存在します。

量指定子除去を伴うすべての一階理論はモデル完全である。逆に、普遍帰結理論が融合性を持つモデル完全理論は量指定子除去を持つ。^[10]

理論の普遍的帰結の理論のモデルは、まさにのモデルの部分構造である。^[10]線型順序の理論には量化子除去はない。しかし、その普遍的帰結の理論には融合性がある。 ${\displaystyle T}$ ${\displaystyle T}$

基本的な考え方

理論に量指定子除去機能があることを構成的に示すには、リテラルの論理積に適用された存在量指定子を除去できること、つまり、次の形式の各式が

$${\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.}$

決定可能性との関係

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

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

例:代数的に閉じた体と微分的に閉じた体に対する零点定理。^{[説明が必要]}

参照

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

注記

1. ブラウン 2002より。
2. プレスバーガー 1929年。
3. 注意：基本的なプレスブルガー算術では、量指定子の除去は認められません。Nipkow (2010)：「プレスブルガー算術では、量指定子の除去を可能にするために、除算可能性（または合同性）述語 '|' が必要です。」${\displaystyle \langle \mathbb {N} ,+,0,1\rangle }$
4. Grädel et al. (2007, p. 20) はプレスブルガー算術をと定義している。この拡張では量指定子の除去が可能である。${\displaystyle \langle \mathbb {N} ,+,<,0,1,(\equiv _{k})_{k>0}\rangle {\text{ where }}x\equiv _{k}y{\text{ iff }}x=y(\mod {k})}$
5. モンク 2012、240頁。
6. エンダートン 2001、188ページ。
7. Grädel et al. 2007.
8. フリード＆ジャーデン 2008年、171ページ。
9. Szmielew 1955、229ページでは「定量化を排除する方法」について説明しています。
10. ホッジス 1993より。

参考文献

• Brown, Christopher W. (2002年7月31日). 「What is Quantifier Elimination」 . 2023年8月30日閲覧。

• Cooper, DC (1972). Meltzer, Bernard ; Michie, Donald (編). 「乗算を使わない算術における定理証明」(PDF) .機械知能. 7.エディンバラ: エディンバラ大学出版局: 91–99 . 2023年8月30日閲覧.

• エンダートン、ハーバート（2001年）『論理学への数学的入門』（第2版）ボストン、マサチューセッツ州：アカデミック・プレス、ISBN 978-0-12-238452-3。

• フリード、マイケル D.ジャーデン、モーシェ (2008)。フィールド演算。 Ergebnisse der Mathematik および ihrer Grenzgebiete。 3.フォルゲ。 Vol. 11 (第 3 改訂版)。スプリンガー・フェルラーグ。ISBN 978-3-540-77269-9. Zbl  1145.12001。

• グレーデル, エーリッヒ;コライティス, フォキオン G.;リブキン, レオニード; マールテン, マルクス;スペンサー, ジョエル;ヴァルディ, モシェ Y .; ヴェネマ, イデ; ワインスタイン, スコット (2007).有限モデル理論とその応用. 理論計算機科学テキスト. EATCSシリーズ. ベルリン:シュプリンガー出版. ISBN 978-3-540-00428-8. Zbl  1133.03001。

• ホッジス、ウィルフリッド(1993).モデル理論. 数学とその応用百科事典. 第42巻.ケンブリッジ大学出版局. doi :10.1017/CBO9780511551574. ISBN 9780521304429。

• Kuncak, Viktor; Rinard, Martin (2003). 「非再帰型の構造的サブタイピングは決定可能である」(PDF) .第18回IEEEコンピュータサイエンス論理シンポジウム, 2003. Proceedings . pp.  96– 107. doi :10.1109/LICS.2003.1210049. ISBN 0-7695-1884-2. S2CID  14182674。

• モンク、J. ドナルド (2012). 『数学論理学』（Graduate Texts in Mathematics (37)）（1976年初版のソフトカバー復刻版）. Springer. ISBN 9781468494549。

• Nipkow, Tobias (2010). 「線形量指定子除去」（PDF） . Journal of Automated Reasoning . 45 (2): 189– 212. doi :10.1007/s10817-010-9183-0. S2CID  14279141. 2022年11月12日閲覧.

• プレスブルガー、モジェシュ（1929年）。 「Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt」。Comptes Rendus du I congrès de Mathématiciens des Pays Slaves、ワルシャワ: 92–101。英語訳はStansifer (1984)を参照

• スタンシファー, ライアン (1984年9月). プレスバーガーの整数演算に関する論文：解説と翻訳(PDF) (技術レポート). TR84-639巻. ニューヨーク州イサカ: コーネル大学コンピュータサイエンス学部.

• シュミエルフ, ワンダ(1955). 「アーベル群の基本的性質」. Fundamenta Mathematicae . 41 (2): 203– 271. doi : 10.4064/fm-41-2-203-271 . MR  0072131.

• Jeannerod, Nicolas; Treinen, Ralf.更新を伴う特徴木代数の第一階理論の決定. 自動推論に関する国際合同会議 (IJCAR). doi :10.1007/978-3-319-94205-6_29.

• スターム、トーマス (2017). 「実数量子除去、決定、充足可能性のためのいくつかの手法とその応用に関する概説」.コンピュータサイエンスにおける数学. 11 ( 3–4 ): 483–502 . doi : 10.1007/s11786-017-0319-z . hdl : 11858/00-001M-0000-002C-A3B5-B .