ラッセルのパラドックス：傾向と対策 (3.1.4) : グリシン論理に関して前回の補足

logic

今回は、前回書き忘れた内容を、少々補足したいと思います。
あ、本題に入る前に、歴史について一言追加を。縮約規則がラッセル・パラドックスを導出する上で必要だという点は、1930年代には既に Curry やFitch といった Combinatry logic の研究者には知られていたそうです*1。しかし証明はグリシンまで待つ必要がありました。

グリシンのパラドックス

前回、グリシン論理で包括原理を持つ体系 GS において、外延性公理を仮定すると矛盾が導出される、という話をいたしました。これは、通称「グリシンのパラドックス」と呼ばれます。証明の初出はGS の無矛盾性を示したグリシンの論文*2です。今月初めの引っ越しで、グリシンの原論文を紛失してしまったため、前回の証明はCantiniの証明を参考にしました。
ところで、その定理と関連して、以下を簡単に証明できます。

（定理）GS で外延性公理を仮定すると、縮約規則が導出される。

（証明）前回の証明を少し修正すれば、GS +外延性公理から、任意の集合 s,t に関して、s∈t→s∈t&s∈t が導出される*3。従って、任意の論理式 P に関して、t={x:P(x)} *4とおけば、P→P&P が証明される。（証明終わり）

前回のやり方ではなく、この定理を先に証明してから、「外延性公理を仮定すれば、縮約規則によってラッセル・パラドックスで矛盾が導出される」と話を進めた方が、きれいな進め方だったかもしれません。

Gordeev's trick

前回の「空集合に外延性を仮定すると矛盾する」という結果ですが、一応証明のスケッチだけここでご紹介しましょう。集合 g を以下のように定義します。

(∀ x) x∈ g ⇔ x=g & x=φ

このとき

  1. まず x∈g→x∈g＆x∈g が成立する。また x∈g&x∈g→x∈φ も成立する。従って x∈g→x∈φ 導出され、逆向きは明らかなので、g=ext φ。
  2. 仮定から外延性より g=φ (*)、これがGS+外延性公理という体系の定理として成立する。
  3. 当然 g=g (**) も体系の定理なので、つまり(*)と(**)より g=g & g=φ も体系の定理となる。
  4. ここで g の定義から、g∈g、つまり g∈φ !
  5. 空集合のくせに元を含む、矛盾。

砂山のパラドックス

ちなみに、「砂山のパラドックス」で登場する「砂山」の集合（x ∈θ ⇔ 砂 x 粒は砂山をなす）も、GS 上で外延性を仮定すると矛盾が導出される、というのが私の主張です。GS上だけでなく、古典論理上でもそれは変わりません。
外延性とは集合の確定性の別名であり、多くの場面で曖昧性と関係があるのです。

*1:A coherence space semantics for linear set theory. Masaru Shirahata. による

*2:Gri?sin, V. N. 1982. Predicate and set-theoretic caliculi based on logic without contractions. Math. USSR Izvestija 18: 41-59.

*3:b∈ {x: x∈{x: x=a} & x∈{x: x=a} }の代わりに t∈ {x: s & x∈{t} } を使えば t∈s→t∈ {x: s & x∈{t} } が証明される。

*4:ただし x はダミーの変数：GSでは {x:P(x)} で、Pは x 以外の自由変数も持ってよいことになっています（FV({x:P(X)}=FV(P)-{x})。