さらに勢いで↓これの続き。
cut-elimination.hatenablog.com
今回はJean-Baptiste Joinet, Thomas Seiller "From abstraction and indiscernibility to classification and types: revisiting Hermann Weyl’s theory of ideal elements"という論文をちょっと紹介。
Joinet先生は線形論理の世界では昔から有名なベテランである。Seiller先生は前にも論文を紹介したが、GoI(相互作用の幾何学)や超越論的シンタクスなど現代的な線形論理・ジラール理論を研究している人。どちらもフランス人だが、本論文は日本科学哲学会の雑誌『科学哲学』に掲載された。科学哲学会での企画がもとになったらしい。
本論文は「型」についての考え方を論じたもの。前回の規則のパラドクス論文でも前々回の型なし証明論の論文でもそうだったが、ジラール学派では型（あるいは論理定項）を、なんらかの証明(っぽいもの)との相互作用によって定義する。「相互作用」「計算の停止」を表す関係や集合を定め、相互作用して停止するような相手を持っているものが型とされるのである。これについてテクニカルな細部が論じられている。前回の論文でもそうだったが、なぜかテクニカルな議論はどれも相意味論(phase semantics)と同じなので、それを専門にしている私には易しかった*1。
本論文では、そうした型の考え方の根拠をヘルマン・ワイルの哲学的理論に求める。ヘルマン・ワイルは20世紀前半に活躍した数学者・数理物理学者で、数学の哲学への影響も大きい。ヒルベルトの弟子だが直観主義の論者として有名である。そのワイルが「分類(classification)」について論じたものがあり、それがジラール学派の型概念に近いようである。というかワイルの理論がジラール理論によってもっとすっきりと表現できるらしい。私は知らないことだらけだったのでワイル解釈としてどうなのかはわからない。しかしGoIやルディクスや超越論的シンタクスでよくでてくる「相互作用における振る舞いが同じなものは識別できないので同一視する」という考え方がワイルにも見られるらしい。ジラール先生は自説を補強するのによくカントやヘーゲルを持ち出すが、それよりは筋が良さそうである。
歴史についても要勉強であるなあ。
*1:は
を含む最小の型というのは知らなかったので勉強になった……
