これまで完全性定理やカット除去定理についてごちゃごちゃ書いてきて気づいたことがある。他の分野の数学の定理ではあまりないのかもしれないが、ロジックのメタ定理というのは、独特の語りにくさ？ みたいなのがある。完全性定理だとかカット除去定理だとかいうのは体系によって相対的に成り立つもので、なんというか「これこそが完全性定理だ！」みたいなものはないともいえる。常に「古典一階述語論理の」みたいなのが付くのだから。また、恣意的に作った体系で成り立つかどうかを調べて、成り立ったら偉い！ みたいなバロメーターにもなっている。最初はドラゴンボールを集めることが目的で旅をしていたのに途中から死者を生き返らせるためのただの手段になっていくあの感じに似ているかもしれない*1。カット除去定理も。
というようなことを林晋先生の『数理論理学』を読んでいて「あっそういえば」と気づいた。標準化定理*2について定義する際、「これを標準化定理という」というふうではなく、「〜であるとき、標準化定理が成り立つという」という具合に書いている*3。この書き方は良い。この書き方はNJとかNKに限らずどんな体系にも応用できそうだ。
完全性定理の場合は健全性定理と合わせて、証明することを「完全性証明」という。ここにも、完全性定理は体系の箔付として証明されるというニュアンスがあると思う。証明体系と意味論を定義したら、次は完全性証明だ、という、その個別の体系ごとの次の段取りみたいな意味合いが強い。よって意味論的完全性自体を数学の普遍的な定理とみなしたような書き方は変に見える。「〜の」は必須。カット除去定理も。
完全性定理やカット除去定理と並んで重要な不完全性定理だとどうなのだろう。不完全性定理は算術のメタ定理だから算術の公理の強さによって成り立ったり成り立たなかったりを議論されるだろうけど、成り立つかどうかの境目はわりと解明されているからあまり触れられないかも。しかし非古典論理や部分構造論理で不完全性定理が成り立たなくなることはあるはずで、このへんは岡田光弘先生の「矛盾は矛盾か」でも述べられていておもしろそうだ。線形論理ですよ。
こういう語りづらさというのはロジックが数学や論理の体系をメタ的に調べる分野だからなのかなとも思ったが、いわゆる準同型定理も事情は似ている。数学のいろんな分野で準同型定理というのが出てきて、「これこそが準同型定理だ！」というのは特にない。そういう意味では準同型定理もメタ的な定理である。ただし圏論では準同型写像は関手というものの一種として捉えられたりする。思うに圏論というのはこういうメタ的な定理をうまく統一的に扱えるのでしょうな。カット除去定理や不完全性定理はわからないが、完全性定理に関しては準同型定理と似たところがあり、圏論をやると今回のようなことにも何か知見が得られるのかもしれない。
