あなたはこの公理を信じますか - 檜山正幸のキマイラ飼育記 (はてなBlog)

信じる者は救われる or 巣食われる

公理というのは、明らかに矛盾があれば別だけど、そうじゃないなら、採用するかしないかの判断基準て特にないんだよね。その公理を信じる人／メリットを感じる人が採用するだけ。

正しさを担保しようにも、論理的にはそれ以上は遡れない*1ので、「正しそう」という状況証拠を積み上げるとか、役に立った事例を並べるとか、コレがないと不便だぞと訴えるとか、そういう行為でしか公理の正当化、いやプロモーション活動はできません。

で、ここ何日かダラダラと話題にしている宇宙公理〈the universe axiom〉だけど、これを受け入れるかどうかも、感覚・感性・感情・心情でしか判断できない。あるいは、信仰〈faith〉の問題、とも言えます。

もう一度宇宙公理を述べますが、二種類に分けましょう。「ZFCの宇宙（ときに大宇宙と呼びます）のなかに、グロタンディーク宇宙（ときに小宇宙と呼びます）が少なくとも1つは存在する」という内容の命題をU（Univereseの'U'）とします。「いくらでも好きなだけグロタンディーク宇宙を取れる」という内容の命題のほうはMU（Multiple-Universe = Multiverse から）としましょう。

[U 単一宇宙公理] ZFCの宇宙Vのなかにグロタンディーク宇宙Uが存在する。
[MU 多宇宙公理] ZFCの宇宙Vの任意の集合x（x∈V）に対して、x∈U となるグロタンディーク宇宙Uが存在する。

到達不能基数（非可算な強到達不能基数）の存在を主張する公理をIとすると、ZFC+UとZFC+Iが同値なことは知られています。同様に、ZFC+MUも基数の言葉で書けますが、基数に興味があるわけじゃないので、宇宙公理は大宇宙と小宇宙に関する命題と捉えます。

宇宙公理（UにしろMUにしろ）を積極的に支持する気になれない／なれなかったのは、「あれば便利だ」以外に、「そうであるべき」理由が見つからないからです。でも、ここ二,三日で心境が変化して、「あれば便利だ」だけでも十分な理由のような気がしてきました。宇宙公理を回避したり代替案を探すのに労力をかける意義も見当たらないし、だったら受け入れて楽になればいいじゃん、と。

ここは楽園か

ここから先のVは、ZFC+UまたはZFC+MUの宇宙とします。つまり、V内にグロタンディーク宇宙Uを取れます。通常の構成や議論はUのなかで行います。必要があれば、Uの外に出て、Uを外からいじってもかまいません。

Uの部分集合は、Uの観点からはクラスです -- U-クラスと呼びましょう。U-クラスが真クラス〈大きい集合〉のときもあるでしょう。しかし、Vから見れば、U-真クラスだろうが何だろうが単なる集合（小さい集合）で、U-クラスの全体Pow(U)もまた単なる集合です。U-クラスを集めたモノの全体Pow(Pow(U))だって単なる集合です。

Uに関するメタ理論が、Vの普通の集合論で行なえます。構文的／論理的な道具は何も追加しないで、U-クラスの理論が作れます。ほぼタダで、メタ理論／クラス理論が手に入るのです。

何も気にすることなく、VのなかでUを操作できます。ZFC+MUを仮定するなら、なにか困ったことが起きてもUより上位の宇宙U'に移れば収拾できるでしょう。

まー、素敵。

楽園なんてない

今年（2018年）に出たレヴィ〈Paul Blain Levy〉（Call-By-Push-Valueの人です）の論文には、僕のような安直な改宗者を愕然とさせることが書いてあります。

Title: Formulating Categorical Concepts using Classes
Author: Paul Blain Levy
Pages: 11p
URL: https://arxiv.org/abs/1801.08528

とにかくうまくいかない！

タプルがうまく作れない。タプルを集めた直積も作れない。
同値関係による商がうまく作れない。
圏の圏がデカルト閉にならない。
米田の補題がうまく定式化できない。
そのくせ、比較的簡単に病的例を作れる。

もう散々ですよ。

レヴィは、ZFC+Uだけを前提としてます。ZFC+MUまで使えば解決できる問題もありますが、ZFC+MUには次の難点があります。

複数の小宇宙を使うので、今どの小宇宙で議論しているかを常に意識しなくてはならない。めんどくさい。
ある小宇宙での議論が、そのまま他の小宇宙でも通用するとは限らない。めんどくさい。
素のZFC上の理論と、複数小宇宙を使った理論との対応関係が複雑化する。めんどくさい。

単一の小宇宙だけなら、Set_U, Cat_U のような小宇宙パラメータ（下付き添字にしている）を省略できます。Uの部分集合を「クラス」と呼び、真クラスも含めたクラス概念で諸々のことをやろう -- それがレヴィの方針です。

この「至極ごもっとも」な方針で、素朴に作業すると上記のような困難に出会うのです。レヴィは、様々な工夫とk-クラスという概念により、トラブルを乗り切って比較的にきれいな定式化を得てますが、「はーっ、楽園じゃなかったわ」とため息が出ます。

サイズ問題へのアプローチは、宇宙公理だけではないので、他の方法を調べる／試すことは意味があるでしょう。しかし、「楽ちんで全てがうまくいく」という方法は期待できないかも知れませんね。これは、そうそうウマい話は転がってないよ、というだけのことで、悲観的になる事じゃないとは思いますが。

*1:既に知られた体系との同値を示すとか、埋め込みを構成して正当性を主張することはできますが、これは信頼できる前例がある場合に限られます。