矛盾から任意の論理式が証明できる件

ワタシは論理学の専門家ではありませんが、論理学は面白いのでいろいろ考えたりします。矛盾からは任意の論理式が証明できるという、直感的にあやしいことがらについて、すこし考えたので書いておきます。

Gentzen(G)系は推論規則の、Hilbert(H)系は数学の議論の研究が目的のようだ。

論理には、定義/公理と推論規則の二つの部分がある。

Gでは、公理はA⇛A(スキーマとかシェーマと呼ばれるやつ)のみで、論理演算さえも推論規則で決めてる。

その世界で、矛盾から任意の論理式が導けるというのは、推論で矛盾がでたとしたら、公理に咎はありえないので、推論規則がまちがってるということを意味する。それは推論規則に対するテストの役割をもつ。

矛盾したということは、推論規則にバグがあるのだから、そこから先の任意の命題の証明には意味がない。とも言える。


Hでは、数学の議論を研究しようとしていて、Gとは逆に、推論規則はcutのみとし、公理や定義とそこから導かれる定理の関係に焦点があてられる。

この場合、定義の集合Σにそこから導出される定理を次々追加していった(Σ*)とき、矛盾が含まれたとすると、cutは間違いなさそうだから、Σに原因があると言うことになる。

このとき、矛盾はΣ*の一部でしかなく、Σの定理には、無関係な述語の論理式は出現しないから、任意の言明を証明できるわけではない。