論理学をそこそこ勉強すると遭遇するのがラッセルのパラドクスの議論である。このパラドクスは有名なので、あるいはここから論理学に入った人も多いかもしれない。確か私はそうだった気がする。もうあんまり覚えてないけど。
このパラドクスは現在の標準的な数学ではZF集合論の分出公理というので回避されている。しかしここでは『プリンキピア・マテマティカ』（以下：プリンキピア）におけるラッセル*1自身の回避術と部分構造論理を使った考察をメモしておく。
※なんかうまく書けた感じがしないので、そのうち書き直します。
素朴に古典論理で考えてみる
一般にパラドクスの原因は包括原理を素朴に使いすぎることにあるとされている。なのでまずは素朴な包括原理からどのように矛盾が導かれるかを見ておく。
包括原理の形式化
包括原理を一階述語論理で書くと以下のようになる。
みたいなのは命題関数と呼ぶことにする。
実はこれはプリンキピア（で批判されるもの）とは違った定式化であるということを後述する。
ラッセルのパラドクスの形式化
ラッセル集合の存在を表す命題は以下のようになる。
このようなある に
とか名前を付けたものをラッセル集合という。ことにする。
それで、ラッセルのパラドクスの矛盾の導出は自然演繹でやると以下のようになる（いろいろ省略してるけど）。
と仮定しても
と仮定しても矛盾するので矛盾、という論証もよく見るが、それだと排中律を使ってしまうので、直観主義論理でも成り立つことを示すためにこうした。
古典的なパラドクス回避術
ラッセルはパラドクスが悪循環から生じると考え、この悪循環を禁ずるとした。これを悪循環原理という。悪循環原理のもっとちゃんとした定式化（なんてのはないのだけど）は後回しにして、悪循環原理から導かれる型と階の階層を見る。
注意すべきなのは以下の回避術は論理の制限というより言語の制限であるという点である。つまり、論理規則をいじっているわけではない。言語が修正されることで包括原理の形式が変って、矛盾を導かない安全なものに変るのである。
この章は以下の本の訳者解説を参考にしています。
型（タイプ）
命題関数によって定義された集合を再び命題関数の変項に代入したのが悪循環なのではなかろうか。とすると命題関数の項になんらかの制限を設ければよいことになる。そこで提案されたのが型（タイプ）の階層である。
実はラッセルの理論のなかには集合（クラス）というものが本質的には存在しない。それは糖衣的なものである。プリンキピアは命題関数を基本単位としたもので、そこから定義される集合に関する命題はそれを含まない命題関数に関する命題へと書き換えられる。よってプリンキピアの方策は我々の形式化したラッセルのパラドクスにはそのまま適用できない。我々の形式に活かすには、量化の範囲を制限することになると思う。
包括原理の と
は異なるドメインを持ち、しかも排反とするのである。なので、自然演繹の導出中で
-除去を使うために
を
にしてその後
-除去で
の
を
にしたが、これはできない。何故なら、
が
のドメインの要素ならば、
のドメインの要素ではないからである。これは命題関数
によって定義された集合はこの命題関数の
に代入できないということをうまく表現できているんじゃなかろうか。よってこの導出は不可能であり、ラッセルのパラドクスは回避される。
階（オーダー）
実は普通は量化といったら型よりも階（オーダー）である。何かを定義あるいは構成する際にすでにあるものを使った場合、定義あるいは構成されたものはすでにあるものより上の階のものになる、という発想で、この「すでにあるものを使う」というのは「全体への量化が可能」ということだとされる。その際に定義される当のものも含んでしまっていたら変なわけだ（なんかうまく書けない）。
プリンキピアでは、集合を定義する命題関数に含まれる量化の範囲に階層を設ける。これを階という。詳しくはⅠ型悪循環原理のところで述べる。こちらも集合が本質的には存在しないプリンキピアの定義をそのまま我々の議論に適用できない。
包括原理の と
の内側の左辺の
だが、右辺の命題関数によって作られる集合
（
など任意の名前）はそれ自体の要素にはならない。すると矛盾の導出のなかで
-除去をして
を
にしているところがあるが、これはできない。よって矛盾は導出できず、ラッセルのパラドクスは回避される。
包括原理では、すべての集合が定義される集合に入るかどうかで集合を定義する。しかし、定義される集合と分類される集合で階層が分かれるのが階である。そうすると定義される集合は「すべての集合」に入らなくなる。「すべて」はあくまで各階層ごとの話なので。
ベリーのパラドクス
階は意味論的パラドクスというのを回避するために導入されている。意味論的パラドクスの代表とされるのがベリーのパラドクスである。それは以下のようなものである。
100文字以下で定義できない最小の自然数があるとしよう。その自然数を とする。しかし「100文字以下で定義できない最小の自然数」は100文字以下なので、
は100文字以下で定義できている。これは変である。
なのだけれども、今回は話を集合論と包括原理に限っているので、この話をうまく形式化できない。アカン。集合のメンバーシップ関係ではなく、個体とか項とかいうものの定義を与える包括原理とは別の何かが必要なんじゃなかろうか。項の話と集合の話を同じ階の階層で議論するのは変な話なのかもしれない。
Ⅰ型悪循環原理
プリンキピアには悪循環原理というのがあると述べた。実はラッセルはこれをちゃんと厳密に定式化してはいないらしい。そして案の定ラッセルのいう悪循環原理は3つの意味があって曖昧だという批判がある。ゲーデルによる批判である。ゲーデルによればそのうち1つ目が解釈として妥当であり、そしてその意味での悪循環原理を批判して退ける。その1つ目というのは以下である。
Ⅰ 或る集まりが全体をもつと仮定するとその全体によってしか定義できないような要素を含むことになってしまう場合、その集まりは全体を持たない。（『プリンキピア・マテマティカ序論』訳者解説、322ページより引用）
これは非可述的定義を禁止しており、それでは通常の数学ができないとゲーデルは批判する。そしてこれを形式的にやろうとすると上のような感じになると思う。非可述的定義というのは、何かを定義する際にそれを含む全体に量化する定義で、これが禁止されるのは悪循環原理と階の階層から容易に導ける。そして実際にプリンキピアは非可述的定義ができなくなりそうになったが、ゲーデルのいうとおりこれはマズく、還元公理というさらなる公理を導入せざるをえなくなった。
型と階の関係と構成主義
型と階のそれぞれ議論を比べてみて欲しい。動機は異なるが、結局は同じことになる。どちらも悪循環ぽい が禁止するのが目的で、それが達成されているので。何故そうなるのかはぶっちゃけわからないのだが、話を集合の定義（というか構成）に限っているからかもしれない。
ラッセルの意味論的パラドクス回避術に見え隠れする「すでにあるものから新しいものを作る」という発想は構成主義的なものである。
そもそも、あらゆる集合の存在を前提してその分類によって新しい集合を作るという考え方を取らない。構成主義は。そうではなく、ある集合から別の集合を作るということを繰り返す。これが構成というものである。ゲーデルは構成主義と対立するプラトニズムという思想だったとされている。つまり数学的対象は順次構成されるのではなくあらかじめ存在するという思想である。
ラッセルの構成主義に関しては、以下の本に収録されている戸田山和久「悪循環原理、分岐タイプ、そして「ラッセルの構成主義」」という論文に詳しい。一般にラッセルは構成主義的傾向があるとされるが、そうではないという反論もあり、その反論をさらに検討する論文である。
現代的に整備された型理論
前原昭二『数学基礎論入門』（以下、前原基礎論と略す）はとても良い教科書である。「数学基礎論入門」というタイトルではあるが、不完全性定理の証明に照準を絞って解説してある。
その際、形式体系として型理論を採用しているのも特徴的である。これはそもそもゲーデルの不完全性定理のオリジナル論文がプリンキピアの体系（に関連する体系）であったことによる。
この前原基礎論で導入される型理論は以下のようなものである。
まず対象式（term）が導入される。まず自然数 がある。そして不特定な自然数
もある。下添えの
は階数で、自然数と上の不特定な自然数を総称して1階の対象式という。論理式の定義は、
が
階の対象式で
が
階の対象式ならば
は論理式である、というふうになる。これに論理定項を付けて帰納的に定義するが、この形の論理式は基本論理式という。
包括原理（内包の公理）は以下である（記法は改めている）。
こう書くと同じだが、 は
よりも階数が一つ上でなければならない。
つまり前原基礎論では型と階は同じなのである。そして、これまで述べてきたような型と階の階層がちゃんと同時に導入されている。
また、「高階論理」といったときの「階」も、型と同じであるところの階である。
悪循環原理と可述的数学
ラッセルは悪循環原理から型の階層と階の階層を導いた。しかるにゲーデルは、悪循環原理から導かれるのは非可述的定義の禁止であるとした。プリンキピアでは非可述的定義は階の階層によって禁止される。ということは、ラッセルの悪循環原理理解とゲーデルのそれとでは明確に異なっている。ラッセルにとっては型の階層もあるのだから、悪循環原理は非可述的定義の禁止以上のものである。型を悪循環原理から導く論証は先程の戸田山先生の論文で。
ベリーのパラドクスは意味論的パラドクスの例だと述べたが、ラッセルのパラドクスは論理的パラドクスであると言われる。そして型というのは論理的パラドクスを回避するために導入されている。なので型は命題関数のように論理的言語に関する制限であり、階は集合のような言語に対応するモノに関する制限である*2。型と階は導入の動機が以上のように異なっている。
ところがこれまで見てきたとおり、包括原理を冒頭のように定式化すると、パラドクス回避術としては階の階層も型の階層も同じようなものとなってしまう。
プリンキピアにおいて集合は本質的には存在しないのだから、包括原理に現れるすべての集合上の量化というのはなくてもよい（これは構成主義的な考え方とはまた別である。禁止というよりなくても良いということだと思う。しかし直観主義型理論のような構成主義的体系と相性の良い発想だと思う）。命題関数を集合とみなすような方法をとれば、包括原理に量化は現れないのである。となると階の階層はラッセルのパラドクスの回避とは関係なくなる。
なんでこんなことを細かく述べるのかというと、「ラッセルのパラドクスは非可述的な定義を禁止することで回避される」という論をよく見るからである。しかしこれはちょっと違う。あくまで包括原理をここでやっているように定義すればの話で、歴史的にはラッセルのパラドクスと可述性は別問題であった。型理論が整備されるうちにうまいこと合流したんじゃないかと思う。特に、直観主義型理論のような体系は型によって可述性を実現した構成的数学体系なのでややこしい。
非古典的なパラドクス回避術
これまでの回避術はどれも包括原理を制限するものであった。しかし、そこからの矛盾の導出を制限するというやり方もある。論理のほうを改変するわけだ。そうすれば包括原理は維持できる。それくらい包括原理は魅力的なのである。
BCK論理
古典論理から縮約を除いたものをBCK論理という。構造規則は推件計算に出てくるもので自然演繹では隠れてしまうのだが、導出図を見るとどこで暗黙理に使っているかわかる。
例えば -導入則で消去される
という仮定は、消去されるまでに2回使われている。同じ仮定を2回使っても1回しか使わないのと同じ、というのが縮約規則である。
ただしこの段階では、この導出が下手なだけで実は仮定を1回ずつしか使わない導出も存在するという可能性を否定できない。しかしそうではなく、BCK論理による集合論は無矛盾であるということはちゃんと証明されているらしい。つまり、同じ仮定を何度も使えるという性質は、ラッセルのパラドクスの論証にとって本質的なのである。
型の階層は包括原理の量化の内側の の右辺の制限で階の階層は左辺の制限であると述べた。対して縮約の制限というのは、これ自体は維持しつつ両辺が同時に成立しないようにする方策だといえる。
BCK論理と包括原理とラッセルのパラドクスの関係については照井一成「素朴集合論とコントラクション」を参照。
線形論理の思想
縮約だけでなく弱化も除いていろいろいじった論理が線形論理である。線形論理には「仮定は資源である」という思想が背景にある。
ラッセルのパラドクスの回避ということであればBCK論理で十分なのだが、思想面を考えると線形論理も興味深い。線形論理では命題は永続的なものではないとみなされ、古典論理や直観主義論理の命題は様相を持っていると考えられる。縮約や弱化は様相を持った命題にだけ適用される。BCK論理だとアドホックな感じがするが（照井先生の論文を読むとそうは思えないが）、線形論理は他にも正当化の理屈があるので、その副産物としてパラドクスが回避されるなら素晴しい。
線形論理とラッセルのパラドクスの関係は岡田光弘「矛盾は矛盾か」を参照。照井先生の論文も岡田先生の論文もここで取り上げている岡本賢吾先生の包括原理とカリー=ハワード同型対応の論文も、雑誌「科学哲学」の同じ号に収録されている。ラッセル特集だったようだ。
その他
直観主義型理論というのを現在勉強中で、これは可述的な体系の例なのでここでラッセルのパラドクスがどうなるかはそのうち勉強が進んだら検討したい。直観主義型理論ははじめジラールのパラドクスという論理的パラドクスが生じたので可述的になるように修正したらしい。この「論理的パラドクスに対処するために可述的にする」というのが変に感じたので調べた結果が本記事である。構成主義の思想でいくと我々の定式化した包括原理のような「すべての集合が定義される集合に入るかどうかで集合を定義する」という発想をとらない。「すべての集合」などあらかじめないので。
また Peter Aczel 先生が導入したフレーゲ構造という体系(?)もある。これは を命題と認めないことで矛盾を回避するらしい。まだよく知らない。要チェックである。以下の本に解説がある。
