ラッセルのパラドックス：傾向と対策 (3.1.5) : グリシン論理 (4)
ラッセル・パラドックスを回避する方法をご紹介するこのシリーズ、前回までは数学的な話が続いていましたが、今回は話を変えて、以下の問題を考えてみたいと思います。
包括原理も、グリシン論理上ならば無矛盾だということはわかった。
いわゆる「ぬるい」「ざっくりとした」「エセ哲学的な」話題になるのでご注意を。
グリシン論理を考察することの意義って？
グリシンによって、縮約規則のない論理上では、包括原理は矛盾を導かないことは証明されました。しかし、縮約規則ってとても「自然」な論理規則じゃないでしょうか。わざわざ、古典論理を「切り刻み」、「人工的な」論理体系を考察する意味は何なのでしょうか。
こういう質問は、古典論理は一番「自然な」論理 "The logic" であって、それ以外は皆人工的な派生物である、ということを前提にしている様にも見えます。
こういう質問に対する伝統的な反論は、「いや、古典論理こそ不自然だ」というものです。そういう反撃の例は
- ブラウアー時代の直観主義：「排中律は哲学的に正当化できない（数学的真理は時間とともに構成されるものである）」
- ザデーなどの（広い意味の）ファジイ論理：「真理値が 0,1 しかないのは正当化できない（真理とはもっと「曖昧性を許す」もののはずだ）」
などがあげられます。しかし、歴史が示すところ、このような種類の論争は、不毛な結果しか生みませんでした。
現代の論理学者にこういう質問をすると、帰ってくる答えは「我々は古典論理に変わる新しい論理を提案しているのではなく、古典論理の分析をしているのだ」というものでしょう。グリシン論理で包括原理が矛盾を導かないことは、縮約規則がラッセルパラドックスの論証の上でどのような役割を果たしているかということを示すから価値があるのであり、グリシン論理自体が古典論理に代わる "The Logic" だなどと主張したい訳ではない、というものです。グリシン論理を研究することで、古典論理（特に縮約規則）に関して理解を深めることができる。哲学的な正当化は括弧に入れて、対象の数学的性質に注目する、という正しく科学的態度です。
こういう姿勢を前面に押し出した論考の典型としては、線形論理についての照井一成氏の「線形論理の誕生」があります（非常におすすめです）。またHeyting以来の直観主義と構成主義数学の実り豊かな成果も、ブラウアー流の「古典論理の代替物としての直観主義」という立場から脱却し、BHK解釈のような証明と構成という点に集中したおかげである、と言っていいのかもしれません。
私自身も、この主張については何の文句もありません。ただし、個人的には、もう少し強い主張ができるのではないかと思います。
それで、「現実」との関係は？
論理とは、単に論理学の問題ではなく、最近は工学の問題でもあります。経験的な事実として、論理学的な手段は多くの現象を記述する上で有用です。さらに、計算機科学における計算量の問題やソフトウェアの安全性証明、関数型言語のモデルなど、多くの場面で非古典論理が使われています。古典論理ではうまく記述できないが非古典論理でならうまく記述できる現象は多いという点も、経験的な事実でしょう。論理学について、「"The logic" は何か」といった（伝統的な）視点ではなく、「どの論理体系がうまくこの現象を記述できるのか*1」という視点こそ重要になってきているのです（これを "Practical turn of logic" と呼ぶとか呼ばないとか）。
そして以上の考え方は、縮約規則を採用する／しないはすべて個別科学における事情によって左右されるべきでpractical な問題であり、"The Logic" とか言う発想を捨てるべきだ、ということも含意するように思えます。
計算機科学
計算機科学において、自己言及性が重要な役割を果たす点は、いくら強調しても強調しすぎることはないでしょう。ここにあるように、Haskel のような関数型言語では不動点演算子 Y を定義でき、Y は Yf=fYf を満たす（ラッセルパラドックスと全く同じであることに注意！）ため、 f としてもし否定をとれるなら、その関数型言語は古典論理上の体系としては矛盾していることになります。関数型言語としてちゃんと機能しているにもかかわらずです。
しかし、縮約規則のない論理上包括原理を持つ集合論でならば、不動点演算子の存在は矛盾を導びきません。従ってこの集合論は、関数型言語上のプログラムの挙動をうまく記述できる、と結論できます（さらにそのような集合論は、再帰定理により、再帰性を基盤に据えた体系であると言えますが、再帰性は計算概念の基本であり、その意味で関数型言語のモデルであるというにふさわしい、のかもしれません）。
さて、計算機科学において、縮約規則があると記述できない現象があるのはなぜでしょうか。これまでの議論によると、縮約規則は以下の仮定を表現しているもの、と考えられます。
- 計算機のリソースが無限であることを表現する（ジラード）。
- 通信のメッセージにエラーが全くないことを表現する（Renyi-Ulam gameの解釈）。
- 全ての計算は瞬時に答えが出ることを表現する（古典論理において、前提から結論を導出するには時間（証明ステップ）がかかるが、真理値の計算は一瞬で出る）。
このように、古典論理は現実の計算機ではあり得ない理想化された状況を表現しているため、その点で現実に起こる現象の一部を表現できなくなっている、と考えることができるかもしれません。最後の点は、ブラウアーが「証明の本質は時間性である」と言ったことを想起させたりもしますが。
哲学（自然言語の理解）
記述の問題は、計算機科学だけではなく、自然言語の理解についても重要です。自然言語を古典論理で形式化しようという場合、以下の現象をうまく記述できないことが知られています。
そして、論理学の視点に立てば、これら3点は全て縮約規則が矛盾を導く原因であり、縮約規則のない論理上包括原理を持つ集合論で整合的にこれらの現象を表現することができます。
以上の意味において、グリシン論理のような非古典論理の使用は、「それらでないと記述できない現象が存在する」という点において、正当化されるのでは、と思われます。
もちろん、哲学に関して言えば、「記述できるから」で話を終わらせてはいけません。自然言語のどんな性質が縮約規則を排除するのか、どのような性質が縮約規則に対応するのかをちゃんと説明し、縮約規則のない論理の導入を認識論的に正当化しなければなりません（それが難題です）。
