命題論理

MGTP の基本動作を説明するために、まず、 一階述語論理の特殊ケースとして、 命題論理の定理証明について考えてみることにしよう。 実は、基本的な処理の流れは、一階述語論理であっても 命題論理であっても全く変わらない。

たとえば、命題論理式

p ∧(p⊃q) ∧ ¬q

を考えてみよう。

この命題論理式は充足不能、恒偽である。 すなわち、命題変数p,qがどんな真理値をとっても この式を真とすることはできない。 真理値表を書いてみれば(書くまでもなく)明らかである。

MGTPでは、この命題論理式をどう表現し、 それが充足不能であることをどのようにして判定するのであろうか?

まず、上の命題論理式は次のようなMG節集合で表される。

(C1) : true → p.
(C2) : p → q.
(C3) : q → false.

次に、``このMG節集合が充足不能である'' という判定をMGTPはどのようにして行うかを説明する。

  1. まず、(C1)により、無条件にpが成り立つと知る。
  2. pが成り立った以上は、次に(C2)により、qが成り立たなければならないと知る。
  3. ところが、この時点で(C3)によれば、qが成り立つと偽が導かれる (すなわち、矛盾が生じる)と知る。

このように、一般にMGTPは、 (1)まず正節によって無条件に成り立つアトムを見つけ、 (2)すでに成り立つとしたアトムが前件と照合するような非負節を見つけ、 その節の後件に現れているアトムをすでに成り立つとしたアトムの集合に加える、 (3)最後は、すでに成り立つとしたアトムが前件と照合するような負節を見つけて 矛盾を知る、 という手続きを踏んでMG節集合が充足不能であることを知る。

では、上の論理式が

p ∧(p⊃q)

であったとしたらどうなるであろうか?

この場合、MG節集合は次のようになる。

(C1) : true → p.
(C2) : p → q.

すなわち、負節(C3)がない。

このとき、MGTPは、 「{p,q} は成り立つアトムの集合である」 という答えを出す。 論理学の言葉で言えば、 {p,q} は上の節集合のモデル''である。

実は、MGTPはそもそも充足可能な節集合 に対して、そのモデル(成り立つアトムの集合)を 実際に作ってみせることを第一義とする システムなのである。

※ 論理学(モデル論)の言い方では、むしろあるアトム集合が先に 天下りに与えられ、節集合の``解釈''(エルブラン解釈)などと呼ばれる。 そして、そのある解釈のもとで節集合が充足される/されない、 という判定が行われる。 ある解釈が節集合を充足しているとき、その解釈をその節集合の モデルという。


戻る