シリーズ「カット除去定理を考える」その1 カット除去定理 a.k.a. ゲンツェンの基本定理

　完全性定理も中途半端なところで停滞しているのに、新シリーズとしてカット除去定理を考える。カット除去定理もロジックの教科書ではよく登場していて*1、その証明は完全性定理以上に教科書ごとに個性が出ている。そういうのを比較考察していきたいのだけれど、それはまだ準備不足というか実力不足なので書けず、けれどもカット除去定理についていろいろ調べて考えたこともあるので記しておきたいのよ。
　カット除去定理は別名ゲンツェンの基本定理ともいう。それくらい証明論における超重要定理なのである。ではなにがそんなにも重要なのか。ポイントは二つあると思う。
　別名のとおりこれははじめゲンツェンが証明した定理である。ゲンツェンは自然演繹と推件計算*2という二つの証明体系を導入したが、カット除去定理とは推件計算からカット規則を除いてもよいという主張である。直観主義論理や古典論理の推件計算からカット規則を無くしても、無くす前と同じ推件の証明ができるということだ。同じならばカットの除去なぞし無くてもいいのではないかとも思えるのだが、カットというのは厄介な規則で、無いほうが証明体系の見通しが良くなるのである。実用上、カットの無い体系はメタ定理が証明しやすい。無矛盾性などもカット無しの体系では証明しやすく、カット無しで成り立つ無矛盾性はカット有りでも成り立つと言えるからOKということだ*3。ゲンツェンはカット除去定理を利用して算術の無矛盾性を証明している。算術の無矛盾性証明は証明論の原点みたいなもので、いまも竹内の予想などその発展形を研究することが証明論の中心となっている。これがカット除去定理が（証明論の）基本定理と呼ばれる所以であろう*4。そもそもゲンツェンの研究のなかで推件計算の開発と基本定理の証明と無矛盾性証明は一体となっていたと思う確か。つまり、最初に推件計算を開発して、あとからカットが無くていいと気づいて、さらにあとから算術の無矛盾性証明に使えることに気づいて、みたいなことではなかったはず。なのでカット除去定理が基本定理なのは当然といえば当然である。
　カット除去定理についてもう一つ重要な点がある。これはけっこう私の独断偏見が入っている。それは、証明可能性ではなくて証明そのものの性質を議論へと我々を導いている、ということである。カットがあろうがなかろうが証明可能性という点では同じなのだが、別の評価基準*5を設定すればカットありの証明とそうでない証明ではどっちが偉いかとかも考えることができるようになる。カット除去定理はそうした考察の出発点になる。証明可能性という評価基準では変わらないということを保証しているので*6。これと関連して、カリー＝ハワード対応で計算との対応を考える際にも重要である。カリー＝ハワード対応では証明図の書き換えを計算の実行と対応させる。カット除去定理を証明する際、帰納法を行うためにいろいろなカットのある証明図をカットの無いものに書き換えるが*7、このカット除去手続きが計算の実行に対応してくるのである。となるとカット除去手続きがいつかは完了してカット無しの証明図が得られるとするカット除去定理は、計算の実行が終了するという保証と対応してくる。なお、カリー＝ハワード対応というと自然演繹の正規化が計算の実行と対応するという定式化のほうがオーソドックスかもしれないが、推件計算とプログラムの対応を考えたほうが良い場合もある。このあたりも勉強したいところ。
　竹内外史先生の『証明論入門』(共立出版)*8では、MIX*9というカットと同等の推論規則をカットの代わりに入れた体系からMIXを除去するという方法で証明している。MIXがカットと同等であることはただちに証明でき、かつカットよりも除去しやすいということだ。これは伝統的な方法っぽい。戸次大介先生の『数理論理学』(東京大学出版会)でもこの方法だった。

復刊 証明論入門

数理論理学

　対して鹿島亮先生の『数理論理学』(朝倉書店)では「拡張カット」という規則を持った体系からこれを除去するという方法で証明する。拡張カットは文字通りカットの拡張なので、拡張カットが除去できればカットも除去できることになる。この方法のほうがMIXを使うよりも良いというのがもっぱらの噂である。

数理論理学 (現代基礎数学)

　また林晋先生の『数理論理学』(コロナ社)では、カット除去定理*10を自然演繹の正規化定理*11に帰着させて証明しているようだ。まだよくわかっていない。しかしこの方法は先述のカリー＝ハワード対応を考えると非常に興味深い。正規化定理もカット除去定理も同じようなものということを具体的に示す方法であると言えそうだ。

数理論理学 (コンピュータ数学シリーズ)

*1:哲学方面の教科書ではあまり登場しないけど。

*2:sequent calculus（これは英語だけどもとはドイツ語のはず）を「推件計算」と訳すのは名訳だと思う。音が似た漢字を当てているのである。ダルビッシュと樽美酒みたいだ。

*3:無矛盾性は という論理式を証明しないという性質で、こういう証明能力に関するメタ定理はカットの有無と関係なくなる。証明の長さとか複雑さに関する性質はカットの有無で変わる。今回の記事は実はこれが言いたかった。後述。

*4:しかしこの無矛盾性証明というのが私にはまだぜんぜんわかっておらず、何がすごいのかいまいちピンときていない。ちゃんと証明論を専門に扱った英語の教科書なんかを読まなきゃいけない。

*5:例えば計算量なんかが基準になるのかも。

*6:このへんの議論、なんか微妙。

*7:なんかここまで「証明」と「証明図」の区別を蔑ろにして書いてしまっていたかも。

*8:増補した際に八杉満利子先生の執筆した章も加わって共著となったが、カット除去定理（この本では基本定理呼び）の証明のところは竹内先生が書いている。

*9:あだち充先生の漫画じゃないよ。

*10:この本では基本定理呼び

*11:この本では「標準化定理」と呼ぶ。