破壊的な矛盾と穏健な矛盾

数理論理学には、おおざっぱに言って、2つの流派がある。
ひとつはGentzen流といわれて、推論規則の集合について研究する。
もうひとつはHilbert流といわれて、こちらは数学における証明、つまり定義定理を導く証明というものを研究するので、推論規則としては三段論法(cut)だけを使って定理を導くことがらについて研究する。たぶんこういう理解でいいのではないかと思う。

よく、矛盾があったらすべての命題が証明できるから、矛盾がでたらだめだみたいな話をするけれど、これはGentzen流の推論規則の研究の立場からの発言であって、そこでは推論規則の集合が矛盾を導いてしまうと確かになんでも証明できるということになる。

一方で、Hilbert流では、推論規則は三段論法(cut)と一階なら変数の代入しか使わないので、推論規則によって矛盾が発生するということはまず考えられない。明日のことは知らないけど。
だから、ある公理の集合から矛盾が導かれたとしたとき、その原因は公理の選び方にあり、推論規則にはない。
そして、公理の選び方が矛盾の原因であるならば、その公理の集合だけが矛盾しているのであり、任意の論理式を証明することなどできない。
もちろん、その公理の集合に何か論理式を追加した場合、その集合からは矛盾が生まれるので、そんなことはしてはいけないということはわかる。

そういうことだと思う。
ちなみにResolutionはHilbert流で、論理式はclause formのみ。

以上