↓これの続き
cut-elimination.hatenablog.com
超越論的シンタクスの目的として、ジラール先生は「システムから自由な論理学」の構築を挙げている。第四論文"Transcendental syntax IV : logic without systems"のタイトルにもそれが表れている。
システムから自由な論理学の手掛かりがカット除去定理とBHK解釈だという。カット除去定理から帰結する部分論理式特性により、たとえば論理式Aの証明に証明体系(システム)すべては必要なく、Aの部分論理式だけでよいとわかる。これはなるほどだが、ただしカット除去ができなくても部分論理式特性が示せる場合はあるので、カット除去にこだわる意義は難しい。カットを使う証明自体がシステム依存な複雑なものという感じはするが。もう一つのBHK解釈の重要性もまた難しい。証明が関数とみなせるのが大事らしいが、これをシステムから自由というのとどう結びつけるか。わからなくもないが。
システムをなぜ批判するのかというと、それもやはり「偏見」の産物だからということになる。ここでいうシステムは「公理的写実主義(axiomatic realism)」によるものだとジラール先生はいう。公理的写実主義は構文論(シンタクス)/意味論/メタの三位一体のことで、つまり現実から真理を決定し公理を設定する、というメタ的な取り決めのことらしい。純粋な論理学を作るには、現実という偏見とそれに基く意味論を取り除かなければならない。しかもジラール先生は証明論こそ論理学の第一のテーマと考えている。純粋に構文論的な証明論を作ろう、というのが超越論的シンタクスである。こんな感じだと思う。
で、公理的写実主義は論理学1.0の特徴であり、そこから自由になるのが論理学2.0とのこと。
まだ続きます。
追記：↓続きはこちら
