∀と∃と反証法、1引数の場合 (2)
∀と∃と反証法、1引数の場合 (1)]の続き。
4. Σ2=Σ1 ∪ {-B(3), -B(4), -B(5)}の場合
[述語論理で反証に迷う(1引数の場合) 1]では、1と2の枡についてだけ考えてきたが、最初に、コインが置かれる枠が5つあると書いたのに、1と2以外の枠については何も触れてこなかった。コインを頭に思い浮かべているならば、暗黙のうちに{-B(3), -B(4), -B(5)}は前提となっていたかもしれない。
暗黙にそう思っていたとしても、
Σ1 ⊢ -B(3)
となるような反証はできない。
その理由としては次のものがある。
1) Σ1に3という定数がないので、Σ1のfactと+B(3)とのresolutionができない。
2) +B(3)とresolutionができて矛盾を導出するには、-B形のfactがΣ1になくてはならないが1つもない。
枡になにも存在しないのがデフォルト値だとすれば、何も書かれていない3,4,5について -B()が真であると考えるのは妥当だ。しかし、1,2以外のときに-Bになるという条件は、導出できないということだ。
そこで、例をすこし改良する。つまり、すべての枠を観測しているセンサーを、そこにボールがないと判定したとき、それをfact化できるとしよう。
すると、たとえば
Σ2 = {+B(1), +B(2), -B(3), -B(4), -B(5)}
というfactsの集合が検出できるだろう。
5. Σ2⊢∃x +B(x)の場合
これは、∃x +B(x)の場合と同様に、¬conjは -B(x)となり+B(1)か+B(2)かと矛盾するのでΣ1のときと同じR1、R2の反証木によって証明を導ける。
また、conjが∃x -B(x)の場合でも、これの¬conj は+B(x)となり、-B(3)か-B(4)か-B(5)のどれかと矛盾するので、証明ができる。
このように、+Bリテラルと-Bリテラルはunifyできなければお互いが存在することに影響を受けない。
6. Σ2⊢∀x.+B(x)の場合
Σ1⊢∀x.+B(x)は、¬conjを作る時skolem定数が導入され、すべての反証木を生成すれば真となると考えられるが、Σ2の場合はどうだろうか。
Σ2ではすべての定数について+B(s)ではないので、∀x+B(s)は証明できてはならない。
改めて、Σ2の定数は{1,2,3,4,5}なので、証明プロセスは次のようになるだろう。
Σ2のどの定数をsとしても、Σ2, -B(s) ⊢ □ となる … (1)
この場合、s=3か4か5で、-B(s)から矛盾が導出できないので、∀x+B(x)は偽となる。
「矛盾が導出できない」と断言できるのは、有限のfactを相手にしているからである。
7. ∀x(x=1∧x=2⇒+B(x))の場合
では、範囲をせばめたらどうだろうか。
conjとして
∀x(=1∧x=2⇒+B(x)) … (2)
を考える。xが1か2の場合は、+B(x)になるという意味になる。
この場合¬conjは
-∀x((x≠1∨x≠2∨+B(x))
であり、これをclauseに変形すると
∃x(x=1∧x=2∧-B(x))
から、skolem定数 sを導入して
s=1 ∧ s=2 ∧ -B(s) … (3)
となるので、証明すべきは
Σ2のどの定数をsとしても、Σ2, s=1, s=2, -B(s) ⊢ □ … (4)
となる。これをsに具体的な定数をあてはめて展開し
Σ2-1 = (Σ2, s=1, s=2, -B(s))・{s←1} = {Σ2, 1=1, 1=2, -B(1)} … (2-1)
Σ2-2 = (Σ2, s=1, s=2, -B(s))・{s←2} = {Σ2, 2=1, 2=2, -B(2)} … (2-2)
Σ2-3 = (Σ2, s=1, s=2, -B(s))・{s←3} = {Σ2, 3=1, 3=2, -B(3)} … (2-3)
Σ2-4 = (Σ2, s=1, s=2, -B(s))・{s←4} = {Σ2, 4=1, 4=2, -B(4)} … (2-4)
Σ2-5 = (Σ2, s=1, s=2, -B(s))・{s←5} = {Σ2, 5=1, 5=2, -B(5)} … (2-5)
これらすべてを反証できればconjは成り立つ。
この反証では、2≠1や3≠1などのclauseは与えられているとすると
1) s=1,またはs=2の場合は¬conjに対する+B(1), +B(2)がΣ2にあるので、矛盾を導出できる。(s=1, s=2は無関係)
2) s=3(4,5も同様) の場合は、3≠1,や3≠2から矛盾が導出できるので反証される。ただし、-B(3)については+B(3)∈Σ2なので、真と判定されるが、Σ全体から矛盾を得られるので問題ない。
やはり、skolem定数は、Σに出現するすべての定数ということにしておけばいいようだ。
しかし、やはり反証法を使うのはconjが∃xの時だけかもしれない。
8. 赤いコインのある場合
次に、黒だけでなく赤いコインもある場合を考える。
このときの書き方はいろいろ考えられるが、次のような書き方をしてみる。
追加する述語
黒いコインがあるB(x)の他に、赤いコインがあるR(x)、コインがないことを示すE(x)を使う。
R(x) : 赤いコインのある枡の番号がxのとき真
E(x) : 番号がxの枡にはコインがないとき真
ある時点のコインの状態をΣ3で表してみる。
Σ3 = {+B(1), +B(2), +R(3), +R(4), +E(5)}
このとき、∃x+B(x)も∃x+R(x)も証明できる。
∃x+E(x) も証明できるが、その意味はコインが存在しない場所があるということを言っているので+E(5)によって達成できる。
また、∀x+B(x)や∀x+R(x)の証明の反証では、定数は{1,2,3,4,5}であるから、sをこの範囲で選べば
Σ3のどの定数をsとしても、Σ3, -B(s)⊢□ ..; (5)
や
Σ3のどの定数をsとしても、Σ3, -R(s)⊢□ … (6)
をもとめることになり、成り立たない。
しかし、これらも(2)のように条件つきにすれば成り立つだろう。
制約条件とルール
B、R、Eという述語を導入したときは、これらの述語の間の関係も考えるべきかもしれない。たとえば、
∀x (+B(x) ∨ +R(x) ∨ -E(x)) … (7)
∀x +B(x)⇒(-R(x)∧-E(x)) … (8)
∀x +R(x)⇒(-B(x)∧-E(x)) … (9)
∀x +E(x)⇒(-B(x)∧-R(x)) … (10)
が成り立つと言えるだろう。
7は升にはどちらかのコインがあるか何もないかだと言っている。
(8)は、升には黒コインがあったら赤コインはないし、そこにコインがないこともないと言っている。(9)は同じことを赤コインがある場合について言っており、(10)は、升に何もないと言うことは黒コインも赤コインもないのだといっている。
また、これらの関係は、変数を含んでいるのでセンサーが観察したfactではない。
(センサーにfactから一般化を行う機能があれば作り出される条件になるかもしれない)
(8),(9),(10)はclausesにすると次の3つになる。
∀x(-B(x) ∨ -R(x)) … (11)
∀x(-R(x) ∨ -E(x)) … (12)
∀x(-E(x) ∨ -B(x)) … (13)
必要なclausesをΡ1(ロー1)として定義しておく。
Ρ1 = {(7), (11), (12), (13) }
上で説明した観点からは、Ρ1は「ルール」と読んでいいのかなと思う。
こういうルールあるいは性質は他にもいろいろあると思うが、それはいくらでも考えられるだろう。
例えば、一つの升には1つのコインしか置けないと言ったルールは書いていないが、それを追加することもできる。
また、便利そうな述語を追加するたびに、他の述語との関係をこうして追加していくことになりそうだ。
この面倒な作業が必要であるとしたら、解決したい問題に必要のある性質をその場その場で書いていくしかないのであり、そこらへんは数学とは違う点かもしれない。
これをΣのルールとしたとき、P1のようにΣの他のfactと分離して、他のΣにも使えると便利だと思う。
しかし、異なるΣでは少なくともこの例については、次のような点が問題になる。
1) そのルールを満たす述語が違っているかもしれない。
2) ルールの変数がとりうる値の性質が違うかもしれない。
ルールを応用するには、記号の変換であるとか対象集合に対する条件であるとかが必要になるだろう。
Ρ1が何のルールかというと、変数のとりうる値を3つに分けているということを示している。だから、たとえば、Σ100というfactの集合があって、そこでは変数は整数の値を取るとすると、Bをx>0に、Rをx<0に、Eをx=0に変換すれば、整数に関する記述Σ100にこのルールを追加してもよいように見える。それが役に立つかどうかはΣ100で何を書いているかによるが、ルールを移植するという話はこういうことだ。考えるだけで面倒臭い気がするが。
さて、これらはルールとも言えるが、一方で、センサーが新しい状態を観測したとき、そこで作られるΣの各factが、この条件を満たしていなくてはならないという「制約条件」とも考えられる。
例えば、6の位置のセンサーが追加されて +B(6)が得られたら 制約条件Ρ1に従って、-R(6)と-E(6)を自動的に追加するなどの仕組みも考えられるだろう。
実際には冗長なclauseを追加すると必要な証明を発見するノイズのようなものになるので、Ρ1の代わりに、こういうfactを追加すると言うことにするかもしれない。
制約条件を満たしたfact集合だけがセンサーから知らされるのだとすれば、これらのルールがΣの中で真になっていることが保証されるということにもなる。
また、今の例は実験環境のようなもので、この制約条件があらかじめ成り立つような世界を作っているが、観測する対象が現実世界でありこのような条件が成り立つとは限らない場合もある。これまで観察された状態に限ってこのような条件が成り立つと推測するのであれば、これは「仮説」になるだろう。
「ルール」「制約条件」「仮説」は同じ記述でも観点によって役割が違うということだろう。
ルールの限界
ルールΡ1によって、+B(1)から+E(1)が導けるので、+E(5)は不要なのではないだろうか。Σ4としてΣ3から+E(5)を除いたものを考えてみよう。
Σ4 = {+B(1), +B(2), +R(3), +R(4)}
そこで、次のconjectureの証明を考えてみる。
Σ4, Ρ1 ⊢ ∃x+E(x) ?
¬conjは -E(x)になるので
Σ4, Ρ1, -E(x) ⊢ □ ?
という反証を作りたいのだが、これはできない。
その理由は、Σ4には5がないということだ。これではΡ1を使っても -E(5)がでてこないので、矛盾はでてこない。
これは、対象が有限であることによる、面倒臭い事例だと思う。このように、変数のとりうる値が無限で、その性質もありきたりのものであれば、ルールという形で規則を明示するといろいろ楽になるのだが、有限の世界の場合には、書くことが増えたりして大変になるということだ。
この例では、コインの有無ではなく、枡が5つあるということを表現すれば、5がないという問題は解決される。そこからP1の制約条件に従って+E(5)を生成できれば解決できそうに思う。
まとめ
・有限なfactを考えると、定数も有限個になり、∃や∀は有限の式で表せる。
・conjectureが∀xφ(x)の形をしていると、¬conjにはskolem関数/定数が出現し、要素の数だけ Σをつくってすべて反証しなくてはならない。すべての要素に関する主張なのでそれは仕方がない。述語論理で現実のことがらを書くと、factは有限個だからかけなくはないだろうが、その数が膨大になったら現実的ではない。
・変数を含む記述は観点によって「ルール」であったり「制約条件」であったり「仮説」であったりする。