ラッセルのパラドックス：傾向と対策 (3.1.3) : グリシン論理 (3)

最初に一言、グリシンの体系を GL と書いていましたが、実は GS の誤りでした。お詫びして、訂正いたします。
では、今回はグリシン論理上で包括原理を持つ体系 GS において、外延性公理を仮定すると矛盾が導きだされることをご紹介しましょう。この事実はグリシンによって証明されました。

GSにおける同一性の性質

その前に、その証明のキーとなる重要な補題を紹介しましょう。
ライプニッツ同一性に関する論理式 a=b に関しては縮約規則が成立してしまう（つまりライプニッツ同一性は、後述の意味で、「確定的である」）、ということを主張します。ちなみに、ここでの & はmultiprecativeな and を意味します。また¬は否定を表します。

（補題）a=b→(a=b & a=b)

証明：さて、a=b を仮定します。明らかに b∈ {x: x∈{x: x=a} & x∈{x: x=a} } である（a=b の定義は、どんな集合も a と b を区別できないということであり、集合 {x: x∈{x: x=a} & x∈{x: x=a} } も a と b を区別できない：また明らかに{x: x∈{x: x=a} & x∈{x: x=a} } は a を含む）。従って包括原理から a=b & a=b が成立する。（証明終わり）

GSでは外延性公理は矛盾を導く

さて、次に外延性公理を仮定してみましょう。

（定理）GSにおいて、外延性公理を仮定すると、矛盾が導出される。

証明：ラッセル集合 R={x: ¬(x∈x)} に外延性公理が成立すると仮定する。このRと非常によく似た集合 R' を、以下のように定義する。
　　R'={x: x∈R & x≠R}
仮定から、R=ext R' であれば、R=R'が結論できる。さて、

- まず ¬(R∈R)を仮定しよう。
  1. RとR'の含む要素についての違いは R についてだけなので、RがRの元でないと仮定すると、RとR'は外延的に等しいことになる。すなわち、¬(R∈R)→R=ext R' が成立する。
  2. 外延性公理が成立すると仮定すると、R=ext R'ならば R=R' が成立し、上の補題から R=R' ならば R=R' & R=R' が成立する。つまり、¬(R∈R)→ R=R' & R=R' が成立する。
  3. さて、R'は定義から R を要素として含まない (¬(R∈R') )から、R=R' は ¬(R∈R) を導く。当然 R=R' & R=R' は ¬(R∈R) & ¬(R∈R) を導出する。つまり ¬(R∈R)→ ¬(R∈R) & ¬(R∈R) (1)が導出された！この時点でほぼ矛盾の導出は終わりである。
  4. 後はラッセル・パラドックスを導くだけである。
    - 通常のラッセルパラドックスの推論（¬(R∈R) →(R∈R)）より、¬(R∈R) & ¬(R∈R)→(R∈R) & ¬(R∈R)、つまり ¬(R∈R) & ¬(R∈R)→⊥ (2)が導出される。
    - 従って(1)と(2)より ¬(R∈R)→⊥ （つまり ( (R∈R)→⊥)→⊥） (*) が GS+外延性公理という体系の定理となる。
- 同様に、R∈R を仮定しても、(R∈R) →¬(R∈R) (**) が言えるので、上の式 (*) と(**) でカットをとれば、(R∈R)→⊥ が導出される。
- という訳で、 ( (R∈R)→⊥) & ( (R∈R)→⊥)→⊥) も GS+外延性公理という体系の定理となり、これは矛盾を導出する。（証明終わり）

以上の証明の要点は、

x=y の形の式には縮約規則が適用できる（つまりライプニッツ同一性は確定的である）。言い換えれば、x=y の形の式は、何回でもコピーできる。
ラッセル集合 R と微妙に異なる集合 R' をうまく使うことで、¬(R∈R) の形の式にうまく縮約を適用できるようにする。

ということです。

Gordeev's trick

Cantorの時代から、外延性はその集合が対象の「確定的な」あつまりの証拠である、と思われていました。その意味で、ラッセル集合 R のような自己言及的な、不可解な存在が非外延的であると言われても、「そうか、そうだよな」ぐらいにしか思わないかもしれません。
しかし、非外延的な集合は、ラッセル集合のような非常識な集合だけではありません。Cantiniは Gordeevの証明法を応用し、以下の驚くような結果を証明しました。

（定理）空集合に関して外延性公理が成立する（(∀ x) x=ext φ→x=φ）と仮定しても、矛盾が導出される

ちなみにφは空集合 {x:x≠x} を表します。つまりGSでは、ZFなどでは当たり前の空集合の一意性を仮定しただけで、矛盾を導いてしまうことになります。
（証明はそのうち、元気があったら追加します）。
かくして、GSにおける非外延性は、決して一部の集合についての特殊な性質ではないことがわかります。

GSの「集合」は本当に「確定的なもののあつまり」なのか？

というわけで、GSにおいて包括原理によって定義される term {x:P(x)} は、フレーゲのabstraction principle に則った定義を持たず、外延性を仮定できず、従って「確定的なもののあつまり」として持つべき性質を持たないということになりました。では、それらを本当に「集合」と呼んでいいのでしょうか？
一つだけ言えることは、Petersenの結果などが示唆することは、それらは「もののあつまり」である以上に、（計算概念の表現である）λ項、ひいては計算機のプログラムの一般化と見なした方がいいだろう、ということです。