カット消去定理。

LKのカット消去定理に関しての疑問。

今『入門数学基礎論』を使って基礎論の初歩を勉強中。

で、やっとLKの基本定理のカット消去定理の証明をじっくりと読んでいって一通り納得がいく形になったのですが、その証明『自体』を眺めて疑問に思うことが、（というか、証明論における定理の証明全般でだけど）「帰納法」を当然のように使って証明しているということ。

ヒルベルトのHにしろゲンツェンのLKにしろ、その公理（あるいは推論の形式）に「帰納法」は含まれていない（「帰納法」の公理は自然数論に含まれている。よくよく考えれば、「任意の自然数について」というのを証明するものなのだから、論理の体系自体には含まれないのは当然）のにそれを使って定理を証明するっていうのはＯＫなのかなぁ・・・？

LKの定理がLKでは証明できない、というのであれば、LKの定理を証明するために使った「体系」が本当に無矛盾なのかが問題となるわけです。
んで、それじゃ困るからと「帰納法」もLKに含めたとしたら、新しい推論の形式がLKに付け加わるわけだけれども、それを付け加えたときにもともとあったLKの性質は変わってしまわないのか、というのも気になるところ。

後者の場合、LKの推論の形式というものを「論理式」として扱っていく（表現する）必要が出てくるわけだけれども、それは可能なのか、という問題もあるし。

まぁ、ここらへんが二階の述語論理っていうのに関係して来るんだと思うので、もうちょい勉強してみたいと思います。