2008年 11月 21日 ( 1 )

命題論理の形式システムLPの公理の独立性

命題論理LPの公理系は次の3つが立てられていた。

公理
1 A→(B→A)
2 (A→(B→C))→((A→B)→(A→C))
3 (~B→~A)→(A→B)

これに次の推論規則

mp AとA→Bが成立しているとき、Bの成立をいうことが出来る。

を使って命題を生成するシステムがLPということになる。このLPにおいて3つの公理が独立しているというのは、それぞれが他の2つの公理から、公理のA,B,Cの命題の置き換えとmpという推論規則の両方を使っては、決して生成できないものになっているということを意味する。これは、この公理系の無矛盾性と完全性が証明されていることと合わせて考えれば、この3つの公理が必要最小限のものになっているということを意味する。

この独立性の証明は、きわめて構造というもののとらえ方にかかわっているもののように感じる。この生成システムは、どんなにがんばって生成をし続けても、2つの公理と推論規則からでは、もう一つの公理を生成することが出来ない。しかし、それが現実の計算において出来ていないからといって、システム全体として未来永劫にそれが出来ないと結論することが出来ない。今は出来ないけれど、あるとき偶然に出来るかもしれないという可能性は、ただ計算をしてみるだけ(文字列を生成し続けるだけ)では結論できないからだ。規則に従って文字列を生成するだけでは、現実にはそれが生成できないという否定が正しいという結論を導くことが出来ない。

More
[PR]
by ksyuumei | 2008-11-21 23:32 | 論理