↓これの続きでごんす。
cut-elimination.hatenablog.com
フィルカルの矢田部俊介「哲学的論理学入門」第3回と最終第4回を読みました。
前回ハーモニーが正規化可能性だというのはどういうことかと書いたが、ちょっと解った。証明の迂回路を消せるのは確かにシステムの堅牢さに役立ちそうである。
形式的なハーモニーが崩れたシステムの例から、形式的なハーモニーは堅牢さ（一般的なハーモニー）の必要条件だという事は解った。では形式的なハーモニーさえあればシステムは堅牢になるのかというのはまだ解っていない。これは刊行予定の本を待つ事にする。
全体的な感想として、私は形式的な論理が人間の規範や実践的推論のシミュレーションであるという感じが実はしていない、というのがある。というのはジラール先生と線形論理の影響だが。実は論理というのは自然界(や計算という現象)に予め内在しているのではないか、と。それを人間がシミュレートしてそれをシミュレートしたのが論理体系なのかもしれないが。
本論では量子論理の例が出てきて、量子論理と古典論理でどちらが正しいかという議論は割愛されていたが、ここに関わってくるかもしれない。ジラール先生は化学反応式を例にとって線形論理がこれを上手く表現できるとしている（"Towards a Geometry of Interaction"や"Linear Logic: It's Syntax and Semantics"といった論文で出てくる）。また私には難しくて解らないが、ジラール先生は線形論理と量子力学との統合も目指している。つまり論理を物理学や物理学的事実・現象に基いて作ろうとしている。矢田部先生は量子力学や量子論理は古典論理に基いて作られていると書いていて、古典論理の方がベースになるんじゃないかと示唆しているっぽい（違うかもしれないが）。しかし線形論理において重要なのは、古典論理や直観主義論理が、様相や構造規則を使って線形論理をベースに割と自然に再構築できるという点である。こうなってくると線形論理は強いかも。むしろジラール先生は、有限的な線形論理が自然現象を上手く(正しく？)表現していて、そこに無限を加えた（たぶん悪い意味で）本質主義的な論理が古典論理や直観主義論理だと考えている（特に線形論理の初期は）。また古典論理に関しては(一般的に)構成性がない(とされている)のが証明をベースに論理を考える際にネックになる。
それとおそらく刊行予定の本ではカリー=ハワード同型が出てくる筈だが、論理というか証明は計算という観点からも意味づけできる。線形論理はこれをもっと大胆に行っているっぽい（計算から論理を回収する、とか。超越論的シンタクスについてちょっと読んだので）。論理に対する要請を計算の観点から与えるという事もありうる。それによって構築された論理があら不思議、線形論理だった、みたいな筋書きがあるらしい。
また立証と反証が科学において本質だという話もあったが、ルディクスでは証明と否定の証明を本質的なものとして対置させる（これは勉強中）。
などなど。
本が出るのが楽しみである。矢田部先生には頑張っていただきたい。
↓この本なんかで照井先生は「直観主義者はいても線形主義者はいない」と書いているが、ぶっちゃけジラール先生は線形主義者のような気がしてならない！ そんなジラール先生の本や論文ばかり読んでいる私も線形主義者かも。
