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

logic

さて、前回はラッセル・パラドックスを導出するよく知られたやり方では、縮約規則が必要だという話をご紹介いたしました。では、本当に縮約規則がない場合、ラッセル・パラドックスは矛盾を導かないのか？この問題を解決したのがグリシンです。

体系 GS

さて、以下のように定義を与えます。

  1. 古典論理から縮約規則を除去した体系をグリシン論理（もしくはCFLew*1）と呼ぶ*2。
  2. また、グリシン論理上で包括原理のみを持つ体系を GS と呼ぶ。

このとき

（定理） GSは無矛盾である

証明：GSはカット除去が可能である（詳細はCantiniの論文をご覧ください）。従って無矛盾である。
注意として、グリシン論理上のカット除去は、古典論理上のカット除去より遥かに簡単だという点があげられます*3。
ちなみにグリシンの原論文*4、英語に訳されたのが1982年ですので、旧ソ連ではもっと早く出されていたはずです。が、どういう文脈で彼の仕事が出てきたのか、全く不明です。

自己言及性の楽園

さて、この体系のすばらしい点は、包括原理がある訳ですから、ラッセル集合が集合として存在することです。「集合全体の集合」などもしかり。それだけでなく、以下のような強烈な定理が成立します。

（再帰定理） GLにおいて、任意の論理式 P(x,y) に関して以下が成立する。
　　　∃z∀x [x∈z ⇔ P(x,z)]

証明：対角化によって z を構成してみせる。

つまり、集合 z を定義するときに、パラメーターとして、集合 z 自身を使用してよい、ということです。 再帰定理は、グリシン論理については Cantini が証明しています。というわけで、再帰定理のおかげでありとあらゆる自己言及的集合を定義することができます。

例：自然数の定義

この再帰定理を使用することで、通常の数学で使用する対象をある程度構成できます。

  • まず、空集合 φ={x:x≠x} として定義し、これを自然数 0 だと見なします（必然性はないんですが、面倒なので）。今後はこのエントリーでも（自然数を表現する場合は）0 と表記します。
  • 次に、自然数 n が定義されているとき、n+1 を {x: x=n} で表現します。

このとき自然数全体の集合ωは、「0を含み、+1に関して閉じている要素の集合」

ω={ x: x=0 ∨ (∃y) y∈ω ∧ x=y+1}

として定義されます。また、例えば足し算を表す関係 plus(x,y,z) は

∈Plus ⇔ x,y,z ∈ ω ∧ <0,y,y>∈Plus ∧ (∃x',y',z'∈ω)[∈Plus ∧ ( (x=x'+1∧y=y'∧z=z'+1)∨(x=x'∧y=y+1'∧z=z'+1) ) ]

と定義できます。もうちょっとわかりやすく書くと、

∈Plus ⇔
either

  • y=0 & x=z
  • or x=x'+1 & z=z'+1 for some ∈Plus
  • or y=y+1' & z=z'+1 for some ∈Plus

と、関数型言語における関数の定義と全く同じ方法で可能です。実際、GLで関数のグラフを定義する方法は、関数型言語でプログラムを書くのと全く同じです。というわけで、Cantiniは任意の部分的帰納関数がこの集合論で表現できることを証明しました*5。

本日のまとめ

という訳で、本日の結果をまとめましょう。グリシン論理上の集合論*6 GS の利点は

  1. 公理が少ないので単純、わかりやすい。
  2. 再帰定理により、あらゆる種類の自己言及的集合をこの体系で定義できる。また、再帰定理よりある程度の算術を展開できる。
  3. 包括原理を持つ。そのためGSはフレーゲが夢想した論理主義者の楽園となり、「集合や自然数はいかなる意味で存在するか」なんて難問に、数学の哲学の研究者は頭を悩ませなくても良い
  4. GSはカット除去が簡単といった証明論的によい性質を持つ。

ではGSの欠点は？時間が遅くなったので、本日はここまで。

*1:Classical Full-Lambek calculus with exchange and weakening rule, ただしclassicalは「排中律を持つ」の意味

*2:ただし、縮約規則がないため、andとorが二種類（additive/multiprecative）に分裂する。詳しい話は線形論理の話の際にでも。

*3:通常のカット除去の証明では、場合分けがややこしくなる最大の原因が、縮約規則を適用した場合でした。例えばラッセル・パラドックスの場合、証明された式 R∈R→⊥ の形を見ても、証明図の上にある論理式の数が、R∈R, R∈R が二個含まれていることはわからないため、証明された式の形だけから証明図全体を推定するのが困難でした。縮約がない場合、証明された式さえ見れば、証明図全体の構造がすぐ想像できます

*4:Gri?sin, V. N. 1982. Predicate and set-theoretic caliculi based on logic without contractions. Math. USSR Izvestija 18: 41-59. 大学等ならばこちらから pdf がとれます

*5:だからこの集合論の決定問題はundecidableです

*6:と呼ぶには語弊がありそうなんですが、その話は次回。