述語論理の部分アルゴリズムへの道のり
述語論理の論理式$ Aが，恒真validなら恒真validであると判定するアルゴリズムは存在する（とされる）
逆に$ Aがinvalidのときどうなるかは保証されない
ここで，述語論理のモデル$ \mathcal{M} = \lang D,I \rangについて，
$ Dは議論領域
$ Iは解釈である
$ \llbracket c \rrbracketは，この本では$ c^Iとかと書く
対応付けとかと呼んでいた
$ Q_1 \cdots Q_nは量化子，つまり$ \forall, \existsのどちらかとする
$ x_1 \cdots x_nは変項とする
$ Cは，量化子を含まない論理式とする
このとき，$ Q_1 x_1 . Q_2 x_2. \cdots Q_n x_n. Cを冠頭標準形と呼ぶ
任意の論理式$ Aについて，冠頭標準形$ A^*を構成することが出来る
$ Q_1 \cdots Q_nが全部$ \existsなものを存在冠頭標準形という．
$ A^Sは次のように作られる．以下，$ Aは冠頭標準形とする． $ Aが$ \exists x_1 .\cdots \exists x_m. \forall y. Bの形をしている
$ 0 \leq m，つまり存在量化子はなくても良い
このとき$ A' = \exists x_1 .\cdots \exists x_m. (B\lbrack f(x_1,\dots,x_m)/y \rbrack)を考える
これが存在冠頭標準形なら$ A^S = A'
違うなら，さっきまでの$ Aを$ A'と考えてもう一回$ \forallを消す
次のことが成り立つ
述語論理のモデルをちょっと弱めているバージョンと考えても…
述語論理の言語（構成要素）$ \mathscr{L}について
$ \mathscr{L}で構成可能な項全ての集合
ただし，$ \mathscr{L}に名前（定数）が一つも存在しない場合，
適当な名前を一つ追加した上で，項全ての集合とする
$ \mathscr{L}についてのHerbrand構造$ M_H = \lang D, I\rang $ D = H_\mathscr{L}
名前$ cについて$ c^I = c \in H_\mathscr{L}
関数/演算子$ f，$ t_1 \cdots t_n \in H_\mathscr{L}について$ f^I(t_1 \cdots t_n) \in H_\mathscr{L}
ここで，$ \mathscr{L}の述語などに関しては何も要請しないことに注意
次のことが成り立つ
集合$ Sを，$ \mathscr{L}上の量化子と自由変数を含まない論理式のある集合とする
$ Sのモデルが存在するなら，$ \mathscr{L}上のHerbrand構造$ M_H = \lang D, I\rangとして$ Sのモデルとなるものが存在する． 次のことが成り立つ
$ \mathscr{L}上の量化子と自由変数を含まない論理式$ Aが恒真であることは，
$ \mathscr{L}上の任意のHerbrand構造$ M_H = \lang D, I\rangとして恒真である ことと同値（必要十分）である
$ Aはそもそも量化子も自由変数も含まない
$ A = P(s) \to (Q(s,t) \lor P(t))であったとき，
ただし$ s,tは変項を含まない項，$ P,Qは述語
$ s,tが異なる項であるとき
エンブラン構造上では，$ s,tは異なる対象への指示，と解釈される
$ P(s), P(t), Q(s,t)はそれぞれ違う真理値を取る，
それらを命題記号$ p_1,p_2,q \in D_t = \{0,1\}として置き換える
この置き換えの処理を$ \pi(A)としてこれからも考える
$ \pi(A) = p_1 \to (q \lor p_2)
これは，命題論理のトートロジー判定と言っても過言ではない
つまり決定可能である（ご存知の通り）
今回の例では$ \pi(A)は恒真ではない
仮に，$ s,tが同じ項なら
$ \pi(A) = p \to (q \lor p)であって，これはトートロジーである
が，$ s,tは普通に別の項として，これからも扱う
$ Aに登場する同じ原始論理式にそれぞれ$ p,q,r,\cdotsという命題要素を割り当てることで生成される命題論理の論理式$ \pi(A)は，もちろんトートロジーであるかどうかを決定可能である
よって次のことが成り立つ
$ \mathscr{L}上の，量化子と自由変項を含まない論理式$ Aが任意のエンブラン構造上で恒真であることは，$ \pi(A)がトートロジーであることと同値であり，決定可能である．
つまり？
$ \mathscr{L}上の，量化子と自由変項を含まない論理式$ Aが恒真であるかどうかは決定可能である
そこで，閉じた存在冠頭標準形の論理式$ Aが恒真であることと同値なことを見つけます $ Bは言語$ \mathscr{L}の量化子を含まない論理式とする
このとき，
$ \exists x_1. \cdots \exists x_n.Bが恒真であることは次と同値である
$ \bigvee_{i=1}^m B \lbrack t_{i1}/x_1 \cdots t_{in}/x_n \rbrackが$ \mathscr{L}の任意のエンブラン構造で真となるような，自然数$ m及び項の組$ t_1 \cdots t_n \in H_\mathscr{L}が存在する
ここまでをまとめると，次のことが主張される
このとき，$ A^Sは$ \exists x_1. \cdots \exists x_n.Bの形をしている
ただし$ Bは言語$ \mathscr{L}の量化子を含まない論理式
2. $ \bigvee_{i=1}^m B \lbrack t_{i1}/x_1 \cdots t_{in}/x_n \rbrackが$ \mathscr{L}の任意のエンブラン構造で真となるような，自然数$ m及び項の組$ t_1 \cdots t_n \in H_\mathscr{L}が存在するかは，頑張れば探し当てられる
候補$ t_{11} \cdots t_{1n} \cdots t_{m1} \cdots t_{mn}が候補だと目星をつける
$ \bigvee_{i=1}^m B \lbrack t_{i1}/x_1 \cdots t_{in}/x_n \rbrackが恒真かどうかは命題論理の決定可能性から有限時間で判定出来る
よりちゃんと言えば命題論理の論理式$ \pi \left( \bigvee_{i=1}^m B \lbrack t_{i1}/x_1 \cdots t_{in}/x_n \rbrack \right)がトートロジーであるかは決定可能である
これを虱潰しにやる
$ \bigvee_{i=1}^m B \lbrack t_{i1}/x_1 \cdots t_{in}/x_n \rbrackが任意のエンブラン構造で真なら$ A^S = \exists x_1. \cdots \exists x_n.Bも恒真であり，
問題は，この頑張ればは本当に頑張る他ない，という点に尽きる
例
$ A = \exists x. \exists y. \forall z. \forall w. (P(x) \to Q(z)) \lor (Q(y) \to P(w))
$ Aのスコーレム標準形$ A^S = \exists x. \exists y. \left(P(x) \to Q(f(x,y))) \lor (Q(y) \to P(f(x,y))\right)
$ H_\mathscr{L} = \left\{ c, f(c), f(c,c), \dots \right\}
候補$ t_1 = c, t_2 = cを試してみる，$ m = 1
$ A^S \lbrack c/x, c/y \rbrack = \left(P(c) \to Q(f(c,c))) \lor (Q(c) \to P(f(c,c))\right)
$ \pi \left( A^S \lbrack c/x, c/y \rbrack \right) = (p_1 \to q_1) \lor (q_2 \to p_2)
これは明らかにトートロジーではない
候補$ t_1=f(c,c), t_2=cを試してみる，$ m = 2
$ A^S \lbrack f(c,c)/x, c/y \rbrack = \left(P(f(c,c)) \to Q(f(f(c,c),c))) \lor (Q(c) \to P(f(f(c,c),c))\right)
今，さっきの候補も選言に入れて$ \pi操作をしてみる
$ \pi \left( A^S \lbrack f(c,c)/x, c/y \rbrack \lor A^S \lbrack c/x, c/y \rbrack \right) = (p_1 \to q_1) \lor (q_2 \to p_2) \lor (p_2 \to q_3) \lor (q_2 \to p_4)
バラすと，$ \lnot p_1 \lor q_1 \lor \lnot q_2 \lor p_2 \lor \lnot p_2 \lor q_3 \lor \lnot q_2 \lor p_4
明らかに$ p_2の結果としてトートロジーになる
以上より（Herbrand定理などより），$ \vDash A（$ Aは恒真）