先日、一橋大学で↓こういうイベントがあった。
講演者の豊岡正庸さんは私の直の先輩にあたる。たいへん優秀な方で、分析哲学・哲学的論理学の世界では注目の存在である。
豊岡さんの講演のなかで線形論理やジラール先生に触れた箇所があり、それに関連する文献は私が少しお教えした。そうしたら豊岡さんは謝辞で私の名前を挙げてくだすった。それに対する私の気持ちが↓こちら。
きのう豊岡さんに謝辞で名前を挙げていただいて、売れてない芸人が売れてる先輩にテレビで名前を出してもらったときの気持ちがわかりました……
— 鈴木盲点潤(線形論理) (@cut_elimination) 2025年1月26日
きのう豊岡さんに謝辞で名前を挙げていただいて、売れてない芸人が売れてる先輩にテレビで名前を出してもらったときの気持ちがわかりました……
— 鈴木盲点潤(線形論理) (@cut_elimination) 2025年1月26日
このトゥイートはけっこうウケた。
で、私が豊岡さんにお教えして講演のなかで触れられていた文献にAlberto Naibo, Mattia Petrolo, Thomas Seiller "On the Computational Meaning of Axioms"というのがある（論文ではなくブックチャプターらしい）。今回の記事はこれをちょっと紹介する。どこかで発表or論文化するかもしれないので、ちょっとだけ。文献はSeiller先生の個人ページからダウンロード可。
全体のテーマは、ダメット=プラウィッツの推論主義（証明論的意味論）を乗り越えよう、ということになる。ダメット=プラウィッツの路線には、タイトルにあるような公理の意味を上手く扱えないという難点がある。ここでいう公理とは非論理的公理のことで、例としてペアの算術の公理なんかが挙げられている。こうした公理はいわば恣意的なものなので、「カノニカルな証明」などダメット=プラウィッツの道具が通用しないわけだ。
じゃあどうするかというと、計算論的な振る舞いを意味として与える。その際に取る方針が相互作用(interaction)としての計算の概念と「型なし証明論(untyped proof theory)」である。
ダメット=プラウィッツは論理的公理や推論規則を中心概念に据えて、論理定項の意味を考えていく。こうすると証明はトップダウンな規則適用で作られ、その一つ一つの規則と論理定項の意味とは切り離せない（たぶん）。
対して本文献は、論理定項や証明をプリミティブとしない。証明以前の構造であるパラ証明(paraproof)なるものを許し、パラ証明同士の相互作用によって起こる結果から、証明が定義される。カリー=ハワード同型対応により、証明はプログラムと、証明される論理式はプログラムの型と同一視できる*1。パラ証明は「なんの証明か」が定まっていない。つまり型=論理式が定まっていない。しかしそのおかげで、非論理的公理という破格なものも表現できる。またこの文献が示すのは、型がなくても計算における意味が定まるということである。それもトップダウン的でない相互作用的な計算を考えることによって定まる。
これらは線形論理の証明ネットを使って理論化される。ジラール先生のGoI (Geometry of Interaction)プロジェクトの後期やルディクス、最近の超越論的シンタクスといった理論も線形論理の証明論の応用として型なし証明論と同様の考え方が見られる。このあたりの解説はこの前の記事↓を参照。
cut-elimination.hatenablog.com
これらの理論では、証明ネット(証明構造)公理リンクをパラ証明、公理リンク以外の部分をテストすなわち反証の試みとみなす。型が事前に決まっていたらテストはひと通りに定まるが、型なしなので、テストはいくらでも変えられる。パラ証明とテスト(反証の試み)の相互作用を数学的に定義して、そこから型を定めるのである。
本文献は非論理的公理も扱うので、証明ネット(証明構造)の公理リンクだけではパラ証明に足りない。これを扱うために、興味深いことに、ルディクスのダイモーン規則を取り入れている（ダイモーンについても↑の記事を参照）。確かにダイモーン規則は非論理的公理とみなせる。ルディクスにおいてダイモーンが導入された動機は説明しがたいが、非論理的公理にまで議論が拡張できるのだなあと合点が言った。
本文献の後半では、Krivineの古典論理の実現可能性やダメットの哲学との比較がさらに検討されている。このへんは難しくてよくわかっていない。ただし、ジラール理論によく現れる「意味や真理はもとからあるのではなく、主張や反論(パラ証明とテスト)のやりとりのなかでできていく」という言語・論理観が論じられているのがありがたい（ジラールの哲学として論じられているわけではないが）。ジラール先生はヘーゲルを使ってそうした議論を補強しているが、もっとダメットのような英語圏の人との比較も気になるところなのである。ジラール先生は英語圏の論者にはめったに言及しないので。
