古典命題論理は決定可能である。すなわち、与えられた命題(あるいはシークエント)が任意のモデルで真どうか、もしくは証明可能かどうかを判定するアルゴリズムが存在する。わが研究室ではこれを↓の小野寛晰先生の解説論文で勉強するのが伝統らしいので読んだ。
シークエント計算を使った、ゲンツェンによる伝統的な手法らしい。
対して古典述語論理は決定不能である。これはチャーチやチューリングが証明した。決定可能性はアルゴリズムを与えれば証明できるが決定不能性の証明はもうちょっと難しい。小野先生の論文でも証明は与えられていない。しかしゲンツェンの手法だとどこで行き詰まるかは書いてあってなるほどと思う。
で、線形論理である。線形論理は、命題線形論理の時点で決定不能になることがわかっている。1990年の論文で示されて、次の教科書にも証明が載っている。
なのだけれど、ゲンツェンの手法を応用してみたら命題線形論理の決定可能性が証明できてしまう感じで辛い。私の証明のどこかが間違っている筈なのだが、どこなのかまったくわからない。これについて考え出したら何も手につかなくなってしまった。生活がめちゃくちゃである。
というわけで、他の人に意見を伺うためにちゃんと証明を書きます。そうすると穴がわかるかもしれないし。それと決定不能性の証明ももうちょっと詳しく追ってこれもちゃんと書きますね。そうすればどこでゲンツェンの手法が躓くかわかろうし。
