今日は有名なラッセルのパラドックスが起きるメカニズムを考えてみます。
ラッセルのパラドックスは数学の基礎である集合論に対する重要な問題提起となったものですが,ラッセルのパラドックスが起きるメカニズム自体には集合論は関係ないというお話です。
ラッセルのパラドックス
ラッセルのパラドックスとは「自分自身を含まない集合全体を考えると矛盾が生じる」というものです。
証明
排中律より, または
だが,
とすると
の定義より
となり矛盾,
とすると
の定義より
となり矛盾。いずれにしても矛盾することが示された。
証明終
ラッセルのパラドックスから得られる教訓は「 という形のものを何でもかんでも集合を思うと痛い目を見るぞ!」ということです。集合の扱いを明確に規定しない素朴集合論を数学の基礎とするのは危険だ,ということで,現代では公理的集合論というものが使われています。
公理的集合論でのラッセルのパラドックス
公理的集合論の代表選手であるZFC集合論において,ラッセルのパラドックスはどのような扱いになるのか見てみましょう。
ZFCは1階述語論理の上に構築された公理系です。ZFCでは項の型は1種類しかいないので「○○は集合である」という文を表すための記号はありません。項の型が1種類なので「出てくるものは何でもかんでも集合である」と思ってもいいですが,そもそも集合以外のものがないので,「集合である」という概念自体が必要ありません。
「山田さんは日本人である」という命題が必要なのは世の中にイタリア人もベトナム人もいるからで,もし世の中に日本人しかいない世界ならば,「日本人である」という概念そのものが必要ないのと同じことです。
1階述語論理では個体変項・ 個体定項・述語記号・関数記号といった文字(記号)と,論理記号 を使います。
は「矛盾」を表す記号です。ZFCにおける
は2項述語記号の一種で,普通の記法
に合わせるなら
と書くべきかもしれませんが,慣習により
と書かれます。
は
を省略したものです。
は
を省略したもの,
は
を省略したものとします。
ZFCにおいて,ラッセルのパラドックスに出てくる「集合 の存在」を表す論理式は\begin{align}\exists y~\forall x~ (x\in y \leftrightarrow x \not\in x)\end{align}になります。この論理式を仮定すると矛盾が導かれる,というのがZFCにおけるラッセルのパラドックスです。
1階述語論理の推論体系として,自然演繹を採用しましょう。詳しくは次のpdfファイルを見てください。
http://abelard.flet.keio.ac.jp/person/takemura/class/2011/print-folnat.pdf(日本大学 竹村亮准教授の講義資料 pdf file)
推論規則として,いくつかの導入規則・除去規則,そして背理法が定義されています。論理式の集合 から,自然演繹で論理式
が導出されることを
で表します。
除去規則は,いわゆる場合分けによる証明を形式化したものです。特別な場合として
が共に
の場合を考えると
を得ることができます。
除去規則で
が
の場合を考えると
が得られます。これは例えば「ある
が存在して
が成り立つ」ことが示されているとき,その存在するという
を
とおき,「
」とするといった,存在が示されたものに固有の記号を割り当てる操作を形式化したものです。
証明
個体定項の記号として が用意されているとする。
[
除去規則]
[
除去規則]
[
の定義]
[
の定義]
[5 に
除去規則]
[6 に
除去規則]
[5 に
除去規則]
[8 に
除去規則]
[9, 7 に
導入規則]
[
除去規則]
証明終
この証明をよく見てみると,ZFCの公理は一切出てきません。1階述語論理の推論規則だけから矛盾を導くことができるのです。述語記号 を集合論の記号として性格付けしているのは ZFC の公理系なので,この証明は集合論とは何の関係もないと言っていいでしょう。
もちろん集合論の公理系と全く無関係という訳でなく「 が導かれてしまうような強すぎる公理は採用したらダメ」ということを教えてくれています。
1階述語論理でのラッセルのパラドックス
ラッセルのパラドックスの証明に集合論の公理は何の関係もありませんでした。 という集合論の述語記号でなくても,任意の述語記号
に対して同じように矛盾を導くことができます。繰り返しになりますが証明も一応書いておきましょう。
証明
個体定項の記号として が用意されているとする。
[
除去規則]
[
除去規則)]
[
の定義]
[
の定義]
[5 に
除去規則]
[6 に
除去規則]
[5 に
除去規則]
[8 に
除去規則]
[9, 7 に
導入規則]
[
除去規則]
証明終
ZFCはラッセルのパラドックスを回避できているか?
ラッセルのパラドックスなどのパラドックスを回避することが公理的集合論ができる動機の1つだったのは間違いないでしょう。Wikipedia:公理的集合論の中には以下のような記述があります。
パラドックスの回避
ツェルメロが ZF の元となる公理系を1908年に発表した最大の動機は、実数が整列可能だとする彼の証明を弁護することであった。しかし、同時に彼はその当時すでに知られていたパラドックスを回避しなければいけないこともわかっていた。代表的なものとしては、 ラッセルのパラドックス、リシャールのパラドックス、ブラリ=フォルティのパラドックスがある。 これらのパラドックスは、集合を構成する方法に制限を付けている ZFC の中では展開できない。 例えば、ラッセルのパラドックスで用いられる\begin{align}{\displaystyle \{x\mid x\notin x\}}\end{align}という集まりは ZFC の中では構成できないし、 リシャールのパラドックスで用いられる構成は論理式で記述できない。
ZFCではラッセルのパラドックスを回避できていると言っているように読めますが本当でしょうか?問題はZFCの公理系から自然演繹でラッセルのパラドックスを表す \begin{align}\exists y~\forall x~ (x\in y \leftrightarrow x \not\in x)\end{align}という論理式を導出できるかどうかです。
から矛盾
が導かれるのですから,もしZFCが無矛盾なら当然この論理式は導出されません。一方でもしZFCが矛盾しているなら,矛盾している公理系からはどんな論理式も導出できるので,この論理式も導出できることになります。つまりZFCがラッセルのパラドックスを回避できているかどうかはZFCの無矛盾かどうかに依ります。しかし,ZFCの無矛盾性は証明されていないので,ZFCがラッセルのパラドックスを回避できていることもまだ証明されていない事になります。
まあ,これはちょっとひねくれた見方ですかね。「ZFC集合論では素朴集合論のような単純な形ではラッセルのパラドックスは起きない。ZFCの無矛盾性は多くの人が信じているので,ZFCがラッセルのパラドックスを回避できていることも多くの人が信じている」といったところでしょうか。
ラッセルのパラドックスの応用
定理を証明したら,何かおもしろい応用がないか考えてみることは大切です。せっかくなのでラッセルのパラドックスの応用も考えてみました。
有限集合 の要素数を
で表すことにします。
このとき,次の条件1, 2 を満たす
かつ
ならば,
。
かつ
ならば,
。
証明
に対して,
1 の条件は「 ならば
」 と同値で,
2 の条件は「 ならば
」と同値となる。
に対し,命題「
」 を
で表すことにすると,条件1, 2を満たす
が存在するという命題は\begin{align}\exists A\in X~(\lnot P(B,B) \Leftrightarrow P(A,B))\end{align}と書くことができる。
定理の主張を背理法で示す。条件1, 2 を満たす が存在したと仮定する。
論理式の集合 を考える。
を定義域とし,2変数述語記号
を命題
と解釈すると,これは
のモデルになっている。しかし,
だったので,1階述語論理の健全性により
はモデルを持たない。これは矛盾。
よって,背理法により条件1, 2 を満たす は存在しない。
証明終
もちろんこんな持ってまわった証明をせずに, のとき条件1より
となり矛盾,
のとき条件2より
となり矛盾,というやり方でも証明できます。素朴集合論でのラッセルのパラドックスの証明と同じやり方です。ラッセルのパラドックスで起きる矛盾は割と素朴なものなので,あまり複雑な例は作れないですね。