ルディクスに興味があるのだけれどあんまりよくわからない*1。わかったことをメモしておく。
ジラール先生が最初に提案したのは1999年の論文らしいのだが、本格的に論じられているのは2001年の"Locus Solum"という長い論文である。こちらのほうが基本文献として参照される。ルディクスというのは恐らくジラール先生の造語だが、論文のタイトルの「ロクス・ソルム」というのも小説の『ロクス・ソルス』から取られた造語で、論文の中身もとにかく造語や新概念が多い。故になかなか読みづらい論文なのだが、巻末に付録としてジラール流論理学版「悪魔の辞典」みたいなのが載っていてこれがおもしろい。
私は「ロクス・ソルム」が難しそうだと思って"From foundations to ludics"という別の論文を読んでいたのだが、読むうちにやっぱり「ロクス・ソルム」のほうが良さそうだな、となってなんか要領の悪いことになっている。こういうことを私はよくやらかしてその度にもっとじっくりと一つのものを読みなさいと思うものである。
そんふうにいろんな文献をチラチラ見てわかったこと。
- ルディクスは構文論(これは証明論も含む)と意味論の対立を超えるものという触れ込みだが、どう超えているのかはいまいちわからない*2。構文論は証明を与え、意味論は反例を与える、という話は出てくるが、それに尽きるのかどうか。
- それよりも"syntax-as-syntax"とも書かれていてこちらのほうがピンとくる。構文論は意味論の要請によって与えられているようにも思えるが、自然演繹の正規化定理やカット除去定理のような構文論特有の現象もある。よって逆に
- カット除去(正規化)をベースに構文論を作り、意味論をその性質から導く、というような方針であるらしい。 と は矛盾すると考えるのではなく、 と でカットしたら空シーケントが出てくると考えるべきらしい。
- なので証明の本質はカット除去であり命題の正当化ではないと考える。よって正しくない命題を導いてしまうことも許す。それゆえ公理(のようなもの)としてなんでもありな「ダイモーン」が設定されている。
- ピッチフォークという特殊なシーケントを作り、そこからデザインという特殊な証明を作る。
- と を根とするデザイン(とカウンターデザイン)でカット除去をする。普通の線形論理ではカット除去は必ず成功するが、ルディクスではダイモーンに頼らずにカット除去に成功するかどうかは分らない。プレイヤーは極性の正と負で、ダイモーンに頼らずカット除去に成功すれば勝ち、というゲームができる。 ※証明探索がゲームだと勘違いしていたので修正
- 命題という意味論ぽいものや論理式という構文論ぽいものは本当は出てこない。カット除去において重要なのはカット論理式とその部分論理式の位置(locus)なので、それを表す記号と番号が出てくるのみ。
その内TeXで書きまっせ。