[記号論理学]Cut-elimination Theorem について

来春に『はてなダイアリー』がサービスを終わるとのことで、『はてなブログ』にひっこししてみた。結果、なんかTEX表示がところどころ壊れてる...め、めんどくさ。まあ、そのうち直すかもしれない。


さて、久々に記号論理学を勉強している。テキストは、

である。前原昭二先生の著作であるが、なぜかあんまり知られていないようだ。入手性が悪そうなので、お勧めというわけではないが、記述の仕方は気に入っている。もとは私は『Craigの補間定理』の構成的な証明方法が書いてあるとのことで入手した。『Craigの補間定理』については、また記事にするかもしれないが、今日はCut-elimination Theorem(カット除去定理)についての小ネタである(やっぱり小ネタかっ)。


カット除去定理について、竹内外史先生は著作『証明論入門(共立出版)』の中で『この定理は論理について成立する美しい法則であって、現在まで人類が論理について得た法則の中では他に比べるもののないほど偉大なものに思われる.』(同書p.40)と述べている。そんなにすごいかなぁとも思うが、じゃあカット除去定理が成立しないような論理ってどんなものだろうかと逆に想像してみたくなる。カット除去定理はLKやLJで成立するので、成立しないとなると何か奇怪な推論規則を持った論理だろうか? いや、じつは簡単に作れるのである。それに関して、前原テキストに次のような記述があった。

等式の公理(1),(2)を述語論理(LK,LJ)に付け加えると、もはやカット除去定理は成立しなくなってしまう。
(1) \to t=t  ここにtは任意の項
(2) s=t, F(s) \to F(t)  ここにF(x)は任意の論理式

え、なんで? と思ったがテキストではそれ以上の言及がなかったので、カット除去できないカットを含む証明を発見しようと試みてみた。わかってしまうとすごい簡単だった。

\frac{\to s=s \quad s=t,\ s=s\to t=s}{s=t\to t=s}

という等式の対称性{s=t\to t=s}の証明式がそのひとつである。上の式はすべて公理(右式は論理式F(x)x=sとした公理(2))であり、s=sがカットされている式である。これがカット除去できない理由は、終式{s=t\to t=s}は公理ではなく、また、等号以外の論理記号を含んでいない。するとカット規則以外だと推論規則のうち構造に関する規則しか適用されえない。もちろん構造規則だけでは証明できないため、証明にはカットを使うしかないのである。
『一般的に公理を付け加えるとカット除去定理は成立しなくなる』という事実はよく知られているそうで、線型論理で有名なGirardが指摘したそうだ。推論規則をいじる必要すらないのである。


ところがこの話には続きがあって、

公理(2)の換わりに次の推論規則を導入するとカット除去定理が成立する。

\frac{\Gamma \to \Theta,\ s=t \quad \Gamma \to \Theta,\ F(s)}{\Gamma \to \Theta,\ F(t)}

と公理を推論規則に定式化しなおすだけで、カット除去定理が復活するのである(まあ、これはカット規則の特殊な形を別の推論規則として導入したことになってると思う)。しかも、先の公理系とこの公理系は同値、つまり証明可能な命題の集合がまったく同じとなっており、このことは『カット除去定理』が成立するかどうは、その公理系で何が証明できるかではなく、どういった形で定式化されているかに依存しているというわけである。非常にデリケートな概念であると言える。ただ、『カット除去定理』の成立で、たとえば矛盾\ \to \ の証明不可能性といった『何が証明できるか』の部分を知ることができるという点がとても面白いところだと思う。(小ネタその2へ続く...)