ラッセルのパラドックス：傾向と対策 (3.1.0) : 古典論理を制限するラッセル・パラドックスへの証明論的アプローチ（縮約規則！）

このアプローチは、

• 古典論理の上で、包括原理からラッセル・パラドックスを導出する際、どのようなルールを使っているかを調べる。
• 古典論理からそのルールを除去した部分論理体系を構成し、そこで包括原理が矛盾を起こさないことをチェックする。

ということを目指します。このことで、包括原理と古典論理の性質についてもっとよく知ることができるのでは、と期待されます。
注意ですが、このエントリーの記号の使い方として、記号 ⊥ は矛盾を表します。また、論理式 P の否定 ?P は、実は P→⊥ の略記であると考えることとします。

パラドックスの導出課程（古典論理）

では、ラッセル・パラドックスの導出課程をおさらいしてみましょう。

1. R={x: ?(x∈x)} は包括原理のより存在を保証され、 任意のx について x∈R ⇔ ? (x∈x) を満たす。xにR自身を代入すれば R∈R ⇔ ? (R∈R) となる。 つまり R∈R ⇔ R∈R→⊥ である。
2. ⇔の片側をとり、 R∈R→( R∈R→⊥) が導出される*1。
3. 古典論理上の縮約規則 (the contraction rule) より、R∈R→⊥ が導出される。

というわけで、R∈R を仮定すると矛盾が導出されました。さて一方、

1. R∈R ⇔ ?(R∈R) より、 (R∈R→⊥)→ R∈R が導出される。
2. 二重否定付加より、R∈R→( (R∈R→⊥)→⊥) *2が成立するので、 (R∈R→⊥)→ ( (R∈R→⊥)→⊥)が成立する。
3. 古典論理上の縮約規則 (the contraction rule) より、(R∈R→⊥)→⊥ が導出される。

というわけで、?(R∈R) を仮定しても矛盾が導出されました。以上により、古典論理上では R という集合が存在する限り、どちらにしても矛盾が導出されることが示されました。

パラドックスの導出課程（直観主義論理）

ラッセル・パラドックスは、古典論理だけでなく、例えば直観主義論理でも導出されます。

1. 以下の2式の導出には、どこにも排中律を使っていません。従って、以下は直観主義論理（もちろん縮約規則を含む）+包括原理での定理となります。
   • R∈R→⊥
   • (R∈R→⊥)→⊥
2. ですので、定理同士を & でむすんだ以下の式も、直観主義論理+包括原理という体系での定理となります。
   • (R∈R→⊥) & ((R∈R→⊥)→⊥)　 (*)
3. もちろん (*) で、modus ponens より結局 ⊥ が導びかれる。

つまり直観主義論理上で包括原理を持つ集合論が矛盾を導出することが示されたことになります。

縮約規則とそのパラドックス内での役割

ちなみに、縮約規則とは古典論理上の構造規則の一種で、

A→(A→B) という前提から A→B を結論してよい *3

というものです。この縮約規則が、パラドックスにおける矛盾の導出に大きな役割を果たしていることはすぐにわかります。

1. ラッセル・パラドックスで実際に証明しているのは以下の二つ
   • R∈R→( R∈R→⊥)
   • (R∈R→⊥)→ ( (R∈R→⊥)→⊥)
2. ところが、縮約規則によって以下が（包括原理を持つ集合論の定理として）導出される
   • R∈R→⊥
   • (R∈R→⊥)→⊥
3. 従って、2の上式と下式から、modus ponens より矛盾が導出される。

ということです。この証明のやり方で矛盾を導出するには、縮約規則は不可欠です。

次回の予告

しかし、縮約規則がなしでは、本当に矛盾が導出不可能なのでしょうか？何か別の矛盾を導出するような証明はないのでしょうか？ついでに、縮約規則がなければ矛盾を導かないと仮定しても、縮約規則ってあまりに当たり前に正しい論理規則のように見えるのですが、そういう規則のない論理を考えることに、何の意味があるのでしょうか。
・・・今日はもう遅いので、これで終わりとし、次回はグリシンによる集合論をご紹介します（今週末までにはなんとか書き終えたいものです）。
文中、不正確な点やわかりにくい点が多々あると思いますので、ご意見・ご批判・ご感想をいただければ幸いです。

*1:これと同値な論理式として R∈R&R∈R→⊥ の形があります。

*2:A→??Aのこと：このルールは直観主義でも成立することに注意

*3:もしくは、A&A→B から A→B を結論してよい。