ラッセルのパラドックス：傾向と対策 (3.1.6) : 補足

logic

さて、ラッセル・パラドックスの知られざる解決法を紹介するこのシリーズ、長々と書いてきましたが、やっと縮約規則のない論理で包括原理を持つ集合論の話まで終わりました。
今回は、証明論的アプローチについて書ききれなかったことを補足し、次回から意味論的アプローチ（つまり多値論理）をご紹介したいと思います。

グリシン論理をもっと弱くする(BCK論理)

古典論理から縮約規則を除去したグリシン論理では包括原理が矛盾を導かないという事実は、当然、グリシン論理より証明力が弱い論理では包括原理を仮定しても全く問題がないということを含意します。というわけで、その代表例としてBCK論理をご紹介しましょう。
BCK論理は、グリシン論理から排中律を除去した（もしくは直観主義論理から縮約規則を除去した）体系です。当然包括原理を仮定しても無矛盾です。包括原理を持つ BCK集合論では、再帰定理が成り立ち、非決定的です。くわしくは "Logics without the contraction rule"*1とかをどうぞ*2。

線形論理

ご存知、線形論理です。線形論理についての概説は、昨日ご紹介した照井一成氏の「線形論理の誕生」をどうぞ。線形論理はいろいろなバージョンがあり、ややこしいです。オペレーターがあるもの、ないもの、multipricativeなだけの断片、additiveだけの断片、断片、断片・・・。
線形論理上の包括原理を持つ集合論に関しては、白旗優氏の研究が有名です*3。彼の博士論文はこちら（線形論理のPhase Semanticsを応用した意味論を導入しています）、線形論理で再帰定理が成り立つことを示した論文はこちら、ついでに線形論理の集合論の宇宙の中で、ZFの宇宙が構成できることを示した論文はこちらです。
線形論理上で包括原理のある集合論を考えることの意義の一つは、計算量理論との関係です。（オペレーターによって拡張された）線形論理の部分論理にあたるLight Linear Logic (LLL) で縮約規則を持つ集合論を考えると、その体系での証明は、多項式時間で計算可能な関数に（カリー・ハワード対応の意味で）「対応」します。これはジラードが提唱し *4、照井一成氏が LAST*5として形式化し証明しました*6。
個人的な興味の観点からも、LASTは興味深い存在です。LASTでは様相オペレータを使い自然数全体の集合を定義するのですが、そこでは数学的帰納法（の弱いバージョン）が定理として証明されます。私の専門の、ファジイ論理上で包括原理を持つ集合論では、数学的帰納法を仮定すると矛盾が起こるので、両者の違いがどこからくるのかが不思議です。

縮約規則のない論理上の論理定項を持つ型なしλ-計算

以前お話ししたように、包括原理によって定義される集合は、型理論的には、型なしλ-項の一種と考えることができます。通常のλ-項は論理定項（論理記号を表す定数）をもたず、そのおかげで矛盾が導出されません。歴史的には、

  1. チャーチが最初にλ項を導入した際、その体系は論理定項を含んでいた（チャーチは「集合論に代わる数学の基礎理論」を提供する気がマンマンだったらしい）。
  2. おかげで、ラッセル・パラドックスとほぼ同じ「カリーのパラドックス」を導出し、その体系は矛盾してしまう。
  3. しかし、ラッセル・パラドックスと同じく、チャーチの体系は古典論理ベースで形式化されていたから矛盾を導くのであって、縮約規則がない論理ベースに変更すれば矛盾は起きない。
  4. というわけで、BCK論理ベースの論理定項を持つ型なしλ-計算とかが提案されています。

上記の概説は、おそらく古森先生の日本数学会の特別講演で聞いた内容のupdate版だと思います。私がこの分野への興味を持つことになったきっかけがその特別講演だったので、今読み直してみると、非常に懐かしく感じます。

*1: H. Ono and Y. Komori. Journal of Symbolic Logic, 50(1). pp.169?201, 1985.

*2:余談ですが、BCK論理の最大の欠点は「まとまったサーベイ論文がない」ということで、チェコ人のC氏に「いい論文知らないか」と聞いたところ、スペイン人の書いた学位論文のファイルをもらいました。中身はスペイン語です・・・読めるか。

*3:白旗氏の体系にも、コメント欄で述べたようにオペレーターによって拡張された線形論理上で、オペレーターなしの論理式について包括原理を認めるとか、いろいろなバージョンがあります。

*4:J.Y. Girard. Light linear logic. Information and Computation, 14(3):175?204, 1998. 論文はこちら

*5:Light Affine Set Theory

*6:K. Terui. Light affine set theory: a naive set theory of polynomial time, Studia Logica, Vol. 77, pp. 9-40, 2004. 論文はこちら