日本で証明論的意味論（PTS, Proof-Theoretic Semantics）を研究している人、やたらと多くないだろうか！？ という感じがしているが、どうもそうでもないらしい。後述する大西先生の講義によると、大西先生の博論以降の10年弱でも研究の進展はそれほどないとか。京大周辺に特に多い気がするが、京大周辺の方々が執筆や情報公開に積極的で検索にかかりやすいということなのかもしれない。
それで、検索したら出てくるいろいろな証明論的意味論の文献を収集して見たり読んだりしてみたのでここに記録する。
大西琢朗「証明論的意味論と双側面説」
大西琢朗「証明論的意味論と双側面説」
大西先生の博論で、証明論的意味論に関する日本語文献ではもっとも詳しいものであろう。私はまったく通読できていないのだが、これを解説した講義動画がYouTubeにある。それを見た。
双側面説というのを詳しく扱っている点がポイント。これが私にはけっこう難しかった……。
矢田部俊介「証明論的意味論入門」
矢田部俊介「証明論的意味論入門」
矢田部先生は論理の哲学・哲学的論理学の日本一の論客である（こうやって書くとなんだか馬鹿にしているように受け取られかねないが本当である）。
これは京都大学の講義資料となっていて、証明論の基礎から解説されている。自然演繹とシーケント計算（推件計算）と。構造規則についても詳しい説明なんかもある。（私はすべてをちゃんと読んではいません。）
関連した内容の講義動画がYouTubeにある。
鈴木佑京「証明論的意味論への招待/あるいは/哲学はなぜ論理を語るのか」
名古屋大学の数学・ロジック同人サークル"The Dark Side of Forcing"の同人誌vol.6より。公開していたHPが見れなくなっていたようなのだが、探せば見つかる。
哲学の門外漢（数学者、数学徒）に向けて哲学の議論を披露するというていで書かれている。ソーカル事件なんかにも触れている。哲学者が論理や数学を使うのは、ソーカルに批判されたようなメタファーや装飾としてではなく、哲学的アイデアを論理や数学を使って具現化しているのだ、というおもしろいことが述べられている。証明論的意味論は言語の使用説を論理・数学で具現化したものだと。
局所的ピークの簡約と調和についてわかりやすい説明がある。
伊藤遼「証明論的意味論とその課題」
伊藤遼「証明論的意味論とその課題」
ダメットの議論がまとめられている。ダメットを読んでいない私には良いまとめかどうかわからないが、ダメットを知らない私でもなるほどと思える良い論文である。反転原理、保存的拡大、tonk、調和など重要な概念がわかりやすく述べられている。
近年の証明論的意味論の議論は検証主義的意味理論よりも自然演繹の推論規則を調和という観点から拡張して正当化することに傾いていると指摘されている。
マーティン＝レーフの名前も一瞬だけ出てくる。
豊岡正庸「証明論的意味論における原子ベースと完全性の連関」
豊岡正庸「証明論的意味論における原子ベースと完全性の連関」
言っていいのかわからないが、私の研究室の先輩である。わずか一年の先輩であるがこのような素晴しい論文を書いておられ、たいへん尊敬している。
大西動画ではあまりしっかりとは扱われていなかった原始ベースについてのサーベイである。正直いって私にはけっこう難しい論文で、あまりわかっていない。ただし前半に証明論的意味論の要点が短く纏まっていて勉強になる。
豊岡正庸「異なる論理の共存と証明論的意味論における調和概念について」
豊岡正庸「異なる論理の共存と証明論的意味論における調和概念について」
直観主義論理の結合子と古典論理の結合子をひとつの体系のなかで共存させよう、という内容である。証明能力という観点で見てしまうとたいしておもしろくない結論しか出ないが、しかしこれに証明論的意味論の調和概念を使う（ために規則を操作する）といろいろと違いが出てくるらしい。
まとめ
証明論的意味論とは何か！？ というのがこれまでずっとわからずモヤっとしていたのだが、少しわかった気がする。モデルを使わずにどうやって意味が与えられるのか？ と思っていたが、大西先生によると証明論を使ってモデルっぽいことをやるのだとか。あとは導入則は意味を与えているものと考え、除去則も反転原理でそのようにみなせると考えるとか、なるほどとなりつつある。
