↓これの続き
cut-elimination.hatenablog.com
今回は内容的には「その1」の続きです。
cut-elimination.hatenablog.com
↑の「その1」で、証明ネットはusineの実例だというようなことを書いた。しかしジラール的には、証明ネットはまだまだ「偏見」から逃れられていない。私の読解によると。以下のような問題がある。
- 命題記号という論理を前提したようなモノを使ってしまっている。
- スイッチングの定義は論理結合子の存在を前提している。
- コレクトネス基準は乗法的線形論理の規則から導かれた恣意的なものである。
たぶん上のような事情があるからだろう。ジラール先生は"Transcendental syntax I"で「星座(constellation)」という理論装置を導入する。これが超越論的シンタクスの最初の具体的ステップである。星座は証明ネットの一般化であり、上のような偏見をなるべく避けた中立な概念のみでできている。
- 命題記号は、図のなかでそれが出現する場所(location、ルディクスでいうlocus)によって置き換えられている。
- 論理結合子を廃止し、むしろスイッチングの一種として論理結合子を定義している。
- コレクトネス基準は星座の正規化から定義される。星座の特殊ケースとして乗法的線形論理の規則が得られる。
スイッチングや正規化といった、論理を前提としない概念だけで体系を構築し、後から線形論理が再構成される。テクニカルにはここがおもしろい点である。また論理プログラミングとの関係も興味深いが、この点はまだ勉強中。
哲学的には、果たして場所やスイッチングや正規化が偏見を逃れた中立なものと言えるかが気になるところである。また、星座における正規化は、計算理論なんかで言われる一般的な正規化と同じものとみなしてよいのか、この点も調べ中。
