ラッセルのパラドックス：傾向と対策　番外編：カリーのパラドックス

logic

昔、某准教授はいいました。

（命題）論理学とは否定（¬）と「ならば」（→）の研究だ。

昔から、「かつ」や「または」はあまり問題を起こさず、難問を招くのは否定と「ならば」がほとんどでした。
ラッセルのパラドックスは否定に関するパラドックスですが、多くの「似た」パラドックスがあります。今回は、ラッセルのパラドックスに対応する、「ならば」に関する「カリーのパラドックス」を（Myhill の論文でも大きく扱っていることもありますし）ご紹介したいと思います。

カリーのパラドックス=否定記号を使わないラッセル・パラドックス

さて、ラッセルのパラドックスでは、R∈R と ¬(R∈R)の両方が証明されるので、そこから R∈R & ¬(R∈R)、つまり矛盾が示されるという構造をしています。つまり、本質的な役割を果たすのは否定記号であり、否定記号に関するルールを変えればその導出が不可能になる（極端な話、否定記号がない論理体系では証明することができない）ように見えます。
では、否定記号さえ使わなければ、包括原理は矛盾を導出しないのか？残念ながらそうではない、というのがこのカリーのパラドックス（の集合論バージョン）です。それでは、早速証明してみましょう。古典論理（もしくはそれから否定記号を除去した部分体系）で包括原理を仮定します。また、任意の論理式 P を選びます。このとき、以下の集合 C を考えます。

C = {x : x∈x→ P}

さて、包括原理によって、集合Cは存在を保証されます。ところが、集合Cの存在は、ラッセル集合 Rに匹敵するような、めちゃくちゃな結論を導出してしまうことが分かります。

定理：Pはこの体系の定理となる。

証明：集合Cを考える。このとき、

  1. 包括原理から、任意の集合 x について、(0) x∈C⇔[x∈x→P]、ここのxにCを代入したら(1) C∈C⇔[C∈C→P]が導出される。
  2. 式(1)の右矢印をとれば (2) C∈C→[C∈C→P] が導出される。
  3. 式(2)と縮約規則より (3) C∈C→P が定理として導出される。
  4. 式(3)は式(0)の右辺に相当し、従って式(0)より (4) C∈C が結論される。
  5. 従って、式(3)と式(4)より、Modus ponensから、P が結論される。（証明終了）

論理式 Pは何でもいいので、つまりこの体系は任意の論理式Pを定理として導出できるということになってしまいます。つまりこの体系は矛盾しているということです。

ラッセルのパラドックスと似ている？

さて、カリーのパラドックスにおいて、結論となる論理式 P は何でもいいというのがミソでした。例えば、矛盾を表す記号 ⊥ *1をもつ体系において、P として ⊥ を取れば、話は非常に簡単となります。で、通常、そういう体系では、論理式Aの否定とは、「Aを仮定したら矛盾を導く」の略記（つまり「¬A」とは「A→⊥」の略記）であると考えることが多いようです。言い換えれば、ラッセルのパラドックスを起こすラッセル集合 R は

R={x : x∈x→⊥}

と書け、この R についてカリーのパラドックスを導出すると、それを「ラッセルのパラドックス」と呼べます。かくして、否定を→を使って定義する限りに置いて、ラッセルのパラドックスはカリーのパラドックスの特殊な例ということになります。

解決？

さて、このパラドックスの導出で使われているのは、包括原理とModus ponensと縮約規則なので、いつものように

  • （古典論理を維持し）包括原理を断念する（ZF、型理論など）
  • （包括原理を維持し）縮約規則を断念する（グリシン論理、多値論理、etc）

というやり方が有名です(Modus ponensを捨てるのはちょっと犠牲が高すぎるような気がします)。もちろん、ラッセルのパラドックスの解決法は全て、カリーのパラドックスも解決できていないといけない訳です。
ところでMyhillのやり方は、→を階層化するという、かなりオリジナルな解決法になっています。

Moh Shaw-Kwei のパラドックスと似ている？

ところで、否定だけなら矛盾は導出しないが、→に関して矛盾が起きてしまうって、どこかで見たことないですか？ウカシェヴィッチ三値論理で、包括原理が矛盾を導くことを示したMSKパラドックスと構造が似ていますね。時々MSKも「Curry-like paradox」と呼ばれます。ついでに、今年の7月に中国で発表したMSKを応用した定理の証明では、カリーのパラドックスの証明もだいぶ参考にさせていただきました。

カリーについて

カリー(Haskell B. Curry)といえば、λ計算や Combinatory logic の大物で、関数のカリー化などで有名ですね。関数型言語Haskellは彼の名前をとったともいわれています。
あまり関係ないですが、某有名な関数型言語の教科書では、関数のカリー化の説明をした後、

なお、カリー化の「カリー」とは人名であり、食べ物のカリーとは関係ない

（手元にないのでうろ覚えですが）というコメントが入っていました（ここ、笑うとこ？）。

*1:もちろん、任意の論理式Bについて、 B&¬B という具体的な矛盾命題を与えれば、記号 ⊥ がなくても話は同じなのですが。