ラッセルのパラドックス：傾向と対策 (2) : Restriction of syntax
ラッセル・パラドックスのいろいろな解決法を紹介しようというこのシリーズ、前回までは古典論理を保持しつつ包括原理を弱めようという Restriction of basic principles に分類される集合論(ZFC/ZFAなど)を紹介しました。今回は、基本原理である包括原理はそのままに、言語の構文論(syntax)を変更することで、矛盾を起こす集合を定義する自己言及的な論理式を排除し、それによって整合的な理論を建設しようという Restriction of syntax の試みをご紹介します。
ラッセルの単純型理論
さて、ここでは簡単のために、ラッセルによって開発され、ラムジーによって簡略化された単純型理論(simple type theory または ramified type theory) をご紹介します。
型：
この言語は、加算無限個の型 0,1,2, ... を持つ。
言語：
- 出発点になる言語L0の論理式や項を、type 0と呼ぶ。
- 任意の自然数 n に対し、type n+1の言語 Ln+1 は、以下を満たす。
- 「n+1階の変数」 x(n+1), y(n+1), ..... を持つ。
- P( x(n) ) が論理式のとき、項 {x(n) : P( x(n) )} はtype n+1の項となる。
- 項τに対し、あるn が存在して、項σがtype n であり、項τが type n+1を持つ時のみ、論理式 σ∈τ は有意味な論理式となる。
公理：
外延性公理の他に、任意の n について以下の公理図式と公理がを持ちます。
- 包括原理 ∀x(n) [x(n)∈ {y(n) : P( y(n) )} ⇔P( x(n) ) ]
- 外延性公理 ∀x(n) [x(n)∈a(n+1) ⇔x(n)∈b(n+1)]⇒ a(n+1)=b(n+1)
包括原理そのものは生き残っていますが、適用される式の形が制限され、結果的に包括原理を制限したものになっています。
ラッセル集合の定義不可能性
この定義の下では式 x∈x は typeを持てないことがすぐわかります。ポイントは
σ∈τのとき、τ の type= σ の type +1
となることです。従ってもし式 x∈x がtype付け可能な論理式であるならば、 xのtype= xのtype +1 となりますが、これは矛盾です。
つまり、その否定 ¬(x∈x) も、type を持てない、つまりラッセルの型理論においては文法違反なので考慮の対象外となる訳です。以上よりラッセル集合は定義できず、ラッセル集合は存在できないので、この体系は無矛盾ということになります。
型理論の言葉で言い換える
hatenaには型理論に詳しい方も多いと思いますので、型理論の言葉で言い直すと、以下のようになります。
- フレーゲの集合論において、包括原理で定義される集合は、型理論の言葉では、型無し(type-free)な λ-項 の一種だと考えられる。
- ラッセル・パラドックスは、Type-free な λ-項の理論「フレーゲ」では深刻なエラーがおこるということを示した。
- このエラーを、型がないことにより、この言語上では自己言及文が書けてしまうことが原因である、と考える。
- というわけで、型付けをすることで、自己言及エラーを排除しようというのがラッセルの型理論である。
この階層ωの型理論は、ラッセル・パラドックスの解決法としては非常に典型的なもので、マーティン・ガードナーの「ゴッチャ」vol.1 や、「ゲーデル・エッシャー・バッハ」でも論理学におけるパラドックス解決法の典型として取り上げられています。
ちなみのこの単純型理論の整合性はZFCで証明できます（ZFCの宇宙内で簡単にモデルが構成できます・・・なんたって、階層ωですから）。
真理論との関連
前回指摘したように、集合論におけるラッセル・パラドックスの解決法と真理論における嘘つきパラドックスの解決法はシンクロしています。この場合、
- ラッセルの型理論 ⇔ タルスキの "object language/metalanguage" の区別による真理論
- ZFなどの反復的集合観（「集合全体の集合」などが存在しない） ⇔ 部分的真理述語を使用した真理論（PA上でのpartial truth predicateの定義など）
が対応しているといえるのかもしれません。
言語全体が階層化しているかわりに基本原理（包括原理・T-scheme）は単一なまま（ラッセル・タルスキ）か、言語は一つだが対象が全域的でないのかの違いといえるでしょうか。
数学の基礎としての型理論
ラッセルによって考案された型理論は、これまで多くの体系が考案され、特に計算機科学で重要な役割を果たしています。また、多くの型付きのプログラム言語の先祖ともいえる存在なのかもしれません。ただし、ラッセル自身の体系は、数学の基礎を提供するという目的がありましたが、
- type理論に徹している部分は証明力が弱すぎて解析学等が十分展開できず、数学の基礎というには力不足だった
- そのため、強力な還元公理を付け加えたところ、そのあまりの不自然さに非難が殺到し、構成主義者から見放された
という事情があり、支持を集めませんでした。数学の基礎として最近研究が進んでいる型理論の体系としては、構成的数学の基礎としてマーティン=レフらの直観主義的タイプ理論がありますが、もはや「ラッセル・パラドックスの解決」という問題意識からは遠いところにあるように見えるので、ここでは扱いません。
アクゼルの「フレーゲ構造」：型がない（type-free な）Restriction of syntax アプローチ
次に、Type-free でありながら Restriction of syntax によってラッセル・パラドックスを克服しようという試みを紹介します。そのいい例がアクゼル (Aczel) によるフレーゲ構造で、これは最近邦訳も出ました*1。もともとフレーゲ構造は、マーティン=レフの直観主義的型理論をλ-項で解釈するやり方として考案されたものです。
この体系の要点は
- 命題は関数で表現される。命題（関数）f に対し、包括原理によって定義される集合は λx.fx で表現される。
- 逆に集合は全て λx.fx の形で表現されるものである。またbが集合であれば、任意の対象 a について (a∈b)は命題となる。
- a∈λx.fx は f(a) として表現される。従って包括原理は、(∀ f)(∃ b)(∀ x) [x∈b が真 ⇔ f(a) が真] と表現され、フレーゲ構造の公理である。
- この枠組みでは、ラッセル集合 R について、全ての対象 a について a∈R が真⇔¬(a∈a) が真⇔ a∈a が真ではない が成立するはずであり、それがいえるためには、まずなによりも全ての対象 a について、文字列 a∈a が命題にならなければならない。しかし、この体系においていえることは、高々「a が集合ならば a∈a は命題である」ということだけである*2。
- 従ってラッセル集合 R が集合でない場合、 a∈R は命題にはならず、従って矛盾も導かない。
ちなみにRが集合とならないことは、「内部的定義可能性」に関する議論で証明されます（詳細は原論文をどうぞ）。というわけで、フレーゲ構造においては
ラッセル集合 R は「集合」ではない（内部定義可能性に関して矛盾を導く）
⇒だから ¬(x∈x) も命題ではない（命題だったらこの文でRを集合として定義できるはず）
⇒だからラッセル・パラドックスの矛盾を表現する [R∈R ⇔ ¬(R∈R)] は命題ではない
⇒だからこの体系が矛盾する命題を導出することはあり得ない
という形でパラドックスが回避されます。この構造も、包括原理を保持し、そして集合および命題の定義の仕方（という構文論的構造）で、ラッセル・パラドックスを排除するので、 Restriction of syntax に分類できるのではないかと思います（が、自信がありません、ご意見・ご批判をいただければ幸いです）。
