「現場の集合論としての有界素朴集合論」において、プログラミング言語やデータベースを扱うときは、そんなに立派な集合論は要らないだろう、という話をしました。
プログラミング言語やデータベースを扱うことを現場的日常作業と考えましょう。すると、日常作業にそうたくさんの集合は使わないし、'∈'(所属関係)の階層を無限に昇ることもしません。だったら、全数学を展開できるような強烈な集合論は不要で、小規模で弱い集合論でも足りるでしょう。
小規模で弱い集合論と、そのモデル(意味的世界)である“宇宙”の話をもう少し続けることにします。
内容:
- ZFCの宇宙と小宇宙
- 小宇宙と圏論
- ちょうどよい小宇宙
ZFCの宇宙と小宇宙
ZFC公理的集合論を直接使うことはほとんどないと思いますが、素朴集合論による議論は“頑張れば”ZFC集合論に翻訳できて、合理化できます。ただし、翻訳の労力がハンパない*1ので、やりませんけどね。
一階古典述語論理の上の公理系としてのZFC集合論のモデル(意味的世界)をVとします。Vって何なんだ? にうまく答えることは僕にはできません(苦笑)。ともかく、したいことは何でもできる環境として、Vがあると思ってください。VをZFC宇宙と呼びます*2。
ZFCの宇宙Vが一意的に存在するのかというと、そうでもないようです。ZFC集合論からは決定できない命題Pがあれば、Pが成立する宇宙とPの否定が成立する宇宙は別物です。しかしどちらもZFC集合論のモデルになれます。ここでは、ZFC集合論の定理がすべて成立する宇宙を選んで固定し*3、それをVと呼びます。
Vの部分クラスでVより小さいW(W⊆V、W≠V)が、ZFC集合論のモデルになることはあるだろうし、それは別にかまいません。そのようなWで、W∈V となるものはあるんでしょうか? ちょっと僕には分かりません。もし、そんなWがあるなら、外側のVはもの凄く大きいことになります。
U⊆V という部分クラスUがあって、UがZFC集合論のモデルではなくても、“ある種の集合論”のモデルになっている場合、Uのことも宇宙(ZFC宇宙ではないが)と呼ぶことにします。さらに、U∈V のとき、Uを小宇宙(small universe)と呼びます。小宇宙は、宇宙でありながら、それ自体がZFCの集合であるものです。
小宇宙と圏論
「現場の集合論としての有界素朴集合論」で紹介した有界宇宙は小宇宙の例です。有界な小宇宙Uは、ZFC集合論のモデルにはなれません。ZFC集合論で成立してる定理が、有界なUのなかでは成立しないからです。特に、新しい集合の構成が制限されます。
有界宇宙Uとその集合論は、小さい宇宙と弱い集合論ということになります。いつでもパワフルな集合論が必要なわけではないし、構成の自由さがむしろ邪魔になることもあります。その意味で、小さい宇宙と弱い集合論にも意義と価値があると思います。
さて、圏論を行うのにZFC集合論のフルパワーが必要でしょうか? グロタンディーク宇宙と呼ばれる宇宙のなかで圏論は行えると言われています。しかし、自明でないグロタンディーク宇宙が存在するかどうかはZFC集合論のなかではよく分かりません。
ZFC+αの集合論のなかでグロタンディーク宇宙Uが小宇宙として存在すると、圏論には好都合です。というのも、ZFCの大宇宙Vのなかで圏を定義すると、それをVのなかの集合とみなせることが保証されないからです。例えば、ZFC宇宙Vの集合を対象とする集合圏SetVでは、その対象類|SetV|がV内の集合とはなりません。圏の圏CatVも同様に、V内の集合をベースに捉えることができません。
もし、グロタンディーク宇宙Uが、U∈V として(小宇宙として)存在すれば、 SetU∈|CatV| や CatU∈|2CatV| (2圏の圏)などが言えます。この状況が成立すれば、たまに登場する(せざるを得ない)「必ずしも小さくはない圏の圏CAT」も安心して使えます。
僕は、集合論的な議論はよく知らないし理解できそうにないのですが、CATが存在し、Catに関する議論はCATに対しても適用可能だろう、と楽観的に考えています。なぜ楽観的になるか? というと、そう考えないと不安で、精神衛生上よろしくないからです。
ちょうどよい小宇宙
グロタンディーク宇宙は、大宇宙V内の集合だとはいいながら、そのなかでたいていの事は出来るので、十分に大きな宇宙です。実用上不便を感じることはないでしょう。
一方、「現場の集合論としての有界素朴集合論」で例に出した U = N∪Pow(N)∪{Pow(N)} は、ほんとに小さな宇宙で、不便を感じるかも知れません。
冒頭で言った現場的日常作業の場合、大宇宙Vをほんとに必要とすることはないように思います。目的に応じてちょうどよい小宇宙を作って、そのなかで議論するのも良いんじゃないでしょうか。この方法のメリットは、メタな議論が気兼ねなく自由に出来ることです。
ホントの宇宙Vは、その性格上、外に出ることが出来ません。なにしろホントの宇宙なので、宇宙の外なんて無いんです。この点は、物理的・天文学的大宇宙と同じことです。それに対して小宇宙は、ガジェット(手に取れる小物)ですから、外側から好き放題にいじり倒せます。
宇宙を意識しはじめたのは割と最近なんですが、プログラミング言語/型理論/データベース/証明系が使う論理、などのモデルを考えるときは、宇宙をハッキリさせないとグダグダした感じになっちゃうんですよ。なので、自分が使っている/必要とする宇宙を明示的に定義したほうが良いと感じてるんですわ、ここんとこ。