テーマ 「矛盾からは任意の論理式が証明できる」のか?

古典論理では「矛盾から任意の論理式明される」は驚きを含む定理として扱われていると思う。

最近の大学の論理学のテキストをネット上で参照すると、矛盾から任意の論理式を導出するのは推論規則として導入されているようなので、証明さえ不要になっている。ただ、以前はこのような推論規則はなく、証明されていた定理である。詳細はここでは触れない。任意のBについて、A⇒A∨Bが導出されるのがポイントかなと思う。とはいえ、証明の仕方でいろいろな焦点はあるかもしれない。

[Resolutionの場合]

「矛盾から任意の論理式を証明できる」ということをResolutionで解釈すると、二種類の理解の仕方があると思う。


(1) □⊢A という証明を構成できるか

まず、「Σ ⊢ □が存在する場合に、任意の論理式Aについて □ ⊢Aという証明が存在するか」という問いであると理解できる。

この場合、まず、矛盾は0個のliteralを持つclauseであることと、resolutionが少なくとも1つのliteralを持つ、2つのclauseに対して適用される規則であることから、resolutionベースのシステムでは、矛盾からは何も証明できないので、問いは否定できるだろう。

　　任意のclauseAについて、□⊢Aは存在しない。

(2) Σ, ¬A⊢□ ?

次は、反証によってAを証明することを考える。

まず、clause 集合Σから矛盾が証明できているとする。

Σ⊢□

このとき、任意の論理式として、clause Aを考える。これは、Σに出現しない述語記号だけを使ってで書かれているものを考える。つまり、Σと無関係な論理式ということになる。もしも任意の論理式が証明できるなら、このAも証明できなくてはならない。

ここで

Σ⊢A
という証明をするために、

Σ, ¬A ⊢ □
を作ることを考える。Σ'=Σ∪{¬A}とする。

記法) A⊢Bの証明のすべてをΠ(A,B)と書くことにする。

Π(Σ',□)には前提としているΣ⊢□が含まれるので、確かにΣ'⊢□という証明は存在する。

ここで、反証法によってA, ¬B ⊢□からA⊢Bが正しいということをいうとき、具体的に前者の証明を変形して後者の証明を構成するという方法を取るだろう。

しかし、Σ'⊢Aに対してこれと同じ議論をしようと考える。しかし、証明p∈Π(Σ,□)を変形してもΣ'⊢Aを構成することはできない。なぜなら、Aを構成する述語がΣには存在しないから、pのどの推論ステップでもその述語とresolveする相手となるclauseは出現しないからである。つまり、一般的に、Σ, ¬A⊢□からΣ⊢Aの存在は言えない。

もちろん、Σ'⊢□という証明の中で、¬Aを介在させたものは存在するかもしれないが、それはΣ⊢□が存在するからといって導ける結論ではない。

以上のように、Resolutionベースで、反証法に基づくシステムでは、Σから矛盾が導かれたからといって任意の論理式が証明できるわけではない。

古典論理の場合は、議論したいことが違うから、矛盾から任意の論理式が証明できるということになるのかなと漠然と思う。そもそも矛盾がどういうものなのか分かっていないのではないかという気がする。
古典論理詳しくないので正確なところはわからない。