述語論理でResolutionを使う場合、命題論理と同じく反証法(refutation)を用いることになる。そこで、述語論理で新しく登場した∃xや∀yを含むconjectureについて、どういうことになるのかを考えてみる。

最初は1引数の述語の場合について考える。
次のような状況であるとする。

例)
　黒いコインを2枚を、5つの(1から5まで番号がついている)枠に適当に置いて、それをセンサーで識別する。センサーはその結果をFactとして論理式を作り出力する。たとえば

　Σ1= {+B(1), +B(2)}

は、1と2の枠にコインがあるとき、真となる。

このΣ1についてまず考えよう。

1. 変数なしの場合(1)
　conjecture(以下、conj)を+B(1)とすると、conjectureの否定(以下、¬conj)は -B(1)となるので
　Σ1, -B(1)から次のような反証木が得られる。

　+B(1)  -B(1)
  —--------------- {}
　　　□

線の右に書いた{}は、resolutionで求められるmguを示していて、この場合は空代入なので{}と書いた。

Σ1, ¬conjから矛盾を導出できたので、これを変形して

　+B(1) ⊢ +B(1) 

という証明が導き出せる。

ここまでは、以前の例の復習だが、mguがそこにあることを示してみた。

2. ∃x+B(x)の場合

次に、conjectureが∃x+B(x)の場合を考える。

このconjectureは、+B(x)となるxが存在するという意味なので、Σ1で+B(1)も+B(2)も真だと言っているのだから、xに1か2をとれば成立する。

¬conjは、
　-(∃x +B(x))
であるから、これをclauseに変形すると
　∀x -B(x)
つまり
　-B(x)
というclauseになる。

そうすると

　Σ1, -B(x) ⊢ □

は2つ存在して
、
　+B(1)  -B(x)
  —--------------- {x←1}   …  (R1)
　　　□

と

　+B(2)  -B(x)
  —--------------- {x←2}   … (R2)
　　　□

がそれになる。証明としてはどちらか一つの反証木があれば十分である。

さて、反証木を変形して、conjectureの証明に変形するとこうも書ける。

　　+B(1) ⊢ +B(x)・{x←1}  … (R1')
　　+B(2) ⊢ +B(x)・{x←2}  … (R2')

自明なようにも見えるが、ポイントは

　反証(□の証明)で得られるmguがconjectureのxのどの値について、矛盾するかを示している

ということだ。

証明するだけなら、矛盾を一つ見つければ十分だという話をしたが、このようにΣ1, -B(x)からの証明をすべて求めると、Σ1に含まれる-B(x)という観点から見た情報がすべて取り出せると考えることもできる。
証明をすべて求めるというのはFactの有限集合の場合は、有限の時間で行える(はず)である。
Σの形で保存された情報を別の形に変換しているだけとも言える。

3. ∀+B(x)の場合

次に、conjecture が ∀x+B(x) の場合を考える。
これは、すべての対象xについて+B(x)だと主張しているので、Σ1の場合は正しいだろう。
というのも +B(1)や+B(2)にでてくる定数 1, 2 を自然数のひとつだと考えてしまうと、B(3)やB(4)の真偽値がΣ1からはわからなくなるのでなんとも言えなくなるからだ。Σ1に限定して考えるとどうかを問題にしよう。

¬conjは次のようにclauaeに変形できる。

　-∀x+B(x)

のnotをBの方に移動していくと

　∃x-B(x)

となる。そして、この∃xをskolem関数(ここでは定数)sで置き換えて

　-B(s)

とすればclauseである。ここで、

　Σ1, -B(s) ⊢ □　　... (1)

となる反証を求めることになる。

sが定数ならば、sが1でも2でもないとすると、Σ1の+B(1)や+B(2)とこの¬conjはresolveできないので、(1)のか矛盾は導出できないことになる。

そこで、skolem関数がどういうものなのかに立ち戻ってみる。
さしあたって、skolem関数の引数のない、定数の場合だけについて考える。
skolem関数とは

　∃x+P(x) を +P(s) と書き換えても良い

　つまりこの二つが同値であるようなsをもってこいと言っているのでなくては辻褄があわない。私はずっと、このことを「神様がsを与えてくれる」ということだとばかり思っていたのだが、今回の例をみると「∃x+P(x)は(+P(s)を満たすsを選べば)+P(s)と同値だ」と言っているように見える。

　ということは、この例におけるsは「Σ1にある定数 1, 2を順番に試していって +B(s)が真になるものをsにせよ」と言っているようだ。
　これは、(1) を次のように解釈しなくてはらないということではないだろうか。

　Σ1の+B(s)を満たすどの定数をsとしても、Σ1, -B(s) ⊢ □ となる … (2)

これは定数が1と2しかないので、こう書き換えられる

　Σ1-1 = (+B(1), Σ1, -B(s))・{s←1} = {Σ1, -B(1)} … (1-1)
　Σ1-2 = (+B(2), Σ1, -B(s))・{s←2} = {Σ1, -B(2)}  … (1-2)

のそれぞれについて

　Σ1-1 ⊢ □
　Σ1-2 ⊢ □

の両方の反証が求められたらconjの証明ができた、と考える。
 (ちょっと{Σ1, -B(s)}の集合の書き方がおかしいが、気にしないでほしい)

ということだと思う。しかし、これは自明ではないだろうか。それぞれのΣの左端にかいた +B(1)や+B(2)はskolemの定数が満たすべき条件を追加したのだが、これではΣ1の中身と関係なく矛盾が導出できてしまう。
これは、skolem定数を導入する式 ∃x-B(x)が証明しようとしているconjの否定から作られているからなので、反証法の場合はこのやり方では空振りになっているような気がする。

意味のありそうな方法としては、skolem定数に関する条件をつけないこのような解釈なら納得できると思う。

　Σ1どの定数をsについても、Σ1, -B(s) ⊢ □ となる … (3)

これからは

　Σ1-1' = (Σ1, -B(s))・{s←1} = {Σ1, -B(1)} … (1-1')
　Σ1-2' = (Σ1, -B(s))・{s←2} = {Σ1, -B(2)}  … (1-2')

のそれぞれについて

　Σ1-1' ⊢ □
　Σ1-2' ⊢ □

の反証を求めることに帰着でき、その反証にはΣ1のfactが関与するので意味があると思える。

　いずれにせよ、このように、skolem定数がでてくると「Σ1の定数をsとして」という手順を踏む、あるいは「複数のΣを作って、それらすべての反証を求める」というようなメタな証明プロセスを含むことになるのはおもしろい。

∀x+B(x)の場合は「すべて」の証明のため、個々の証明の範囲を超えた「手」が必要になるということではないだろうか。それがskolem関数というもので象徴されている気がする。

(ブログラミング言語であるLISP的にはmap関数に似ているかもしれない)

ただし、Σ1のように有限のfactの集合を考えている場合は、ここでみたようにskolem定数を具体的に選んで列挙することができるので、神ならぬ人間にも実行ではるものになっているのだと思う。

ちなみに反証にいく前に、conjを定数に分解するとこうなるだろう。
つまり、定数についての知識があり、そもそも定数が1と2しかないことを知っていれば、

　∀x+B(x) ⇔ +B(1)∧+B(2)

であるから、右側をconjと考えると¬conjは

　-B(1) ∨ -B(2)

である。

　Σ1, -B(1) ∨ -B(2)⊢□

の反証は

　　+B(1)  -B(1)∨-B(2)
　 —--------------------------
　　+B(2)　　-B(2)
　 —--------------------------
　　　　　□

になる。

「になる」といっても、この場合だけの話で一番的ではないし、
「-B(1) ∨ -B(2)を作る」というステップは、証明の定義の範囲を超えているので、メタな部分を除外できるわけではない。

まとめ

resolution反証法で証明できるのは∃xタイプのconjecture!

余談 1つのclause集合にできないか

ここまで、Σ1-1' とΣ1-2'は2つのclause集合であり、それぞれに反証しているがこれを1つのclause集合にできないだろうか。つまり、

　Σ1-1'-2' = Σ1-1' ∪ Σ1-2'

として

　Σ1-1'-2' ⊢ □ ?

を求めるということだ。こうすると、メタな概念によらず、∀x+B(x)の証明をするように見える。しかし、∃x+B(x)の場合は、1つの矛盾を見つければ証明が完成したが、こちらはすべての矛盾をみつけないといけないので、やはりすべてのxについてという部分が証明のわくを超えているように思う。