ここ最近、グロタンディーク宇宙の話をしています。
- 贅沢主義者のグロタンディーク宇宙 (7月20日)
- 型・インスタンス・宇宙とタルスキ宇宙系列 (7月22日)
- 贅沢なグロタンディーク宇宙とPropositions-As-Types (7月24日)
- ZF宇宙、グロタンディーク宇宙、型宇宙 (7月27日)
今日もグロタンディーク宇宙の話です。
通常のグロタンディーク宇宙は、ZF集合論における普通の集合 $`U`$ です。が、$`U`$ のなかでZF集合論ができる集合です。$`U`$ のなかに閉じ込められても、通常の集合論的な構成はなに不自由なく出来ます。
「なに不自由なく集合論が出来る」ことがグロタンディーク宇宙の要件だとすると、$`U`$ 内の所属関係が“ほんとの所属関係”である必要はないでしょう。外部のZF集合論から継承した所属関係ではない独自の所属関係を持つグロタンディーク宇宙について考えてみます。$`\newcommand{\mrm}[1]{\mathrm{#1} }
%\newcommand{\cat}[1]{\mathcal{#1} }
\newcommand{\mbf}[1]{\mathbf{#1} }
\newcommand{\mbb}[1]{\mathbb{#1} }
\newcommand{\u}[1]{\underline{#1} }
\newcommand{\Imp}{\mathrel{\Rightarrow} }
\newcommand{\In}{\text{ in } }
\newcommand{\op}{\mathrm{op} }
\newcommand{\Uin}{\mathrel{\epsilon} }
\newcommand{\hyp}{\text{－} }
\newcommand{\Iff}{\mathrel{\Leftrightarrow} }
`$
内容：
ZF集合論のモデルとしてのグロタンディーク宇宙
ZF集合論〈ツェルメロ／フレンケル集合論〉の公理達の名前だけを列挙すると：
- 外延性の公理
- 空集合の存在公理
- 順序無しペアの存在公理
- 分出公理図式〈The axiom scheme of separation〉
- 合併の存在公理
- ベキ集合の存在公理
- 無限集合の存在公理
- 置換公理図式
- 正則性公理〈基礎の公理〉
等号と所属関係記号だけを述語記号とする古典論理の形式的体系にこれらの公理を追加すれば、ZF集合論の形式的体系になります。分出公理図式と置換公理図式は、論理式をパラメータとする無限個の公理の集まりです。
$`U`$ がグロタンディーク宇宙とするとき、$`U`$ はZF集合論のモデルになります。$`U`$ はZF集合論のなかの集合だし、二値ブール値集合 $`\mbf{B}`$ や関数集合 $`\mrm{Map}(\hyp, \hyp)`$ は既に在るので、$`U`$ に関するZF集合論の公理は、$`\mbf{B}`$ や $`\mrm{Map}(\hyp, \hyp)`$ を使って書くことができます。もともとのZF集合論とは多少意味合いが変わる公理もあります。
$`\mrm{AMap}(\hyp, \hyp)`$ は、すべての関数の集合ではなくて、許容された関数〈admissible function〉の集合だとします。許容された関数の定義を固定することはしませんが、例えば「具体的に計算可能な関数」とかです。以下は、$`\mrm{AMap}(\hyp, \hyp)`$ を使った $`U`$ に関する分出・合併・置換の公理です。
- 分出公理： $`\forall p\in \mrm{AMap}(U, \mbf{B}). \exists a\in U.[\, \forall y\in U.(\, p(y) = 1 \Iff x\in a\,) \,]`$
- 合併の存在公理：
$`\forall x\in U.\forall f\in \mrm{AMap}(x, U). \exists a\in U.[\, \forall y\in U.(\, (\exists i\in x. y\in f(i) ) \Iff y \in a \,) \,]`$ - 置換公理：
$`\forall x\in U.\forall f\in \mrm{AMap}(x, U).\exists a\in U.[\, \forall y\in U.(\, (\exists i\in x. y = f(i)) \Iff y\in a \,)\,]`$
いずれも関数（述語またはファミリー）をパラメータとする単一の公理になっています。もともとの分出公理／置換公理は、論理式をパラメータとしていたので、意味合いが変わっています。もともとの合併は、インデックス付きファミリー〈indexed family〉を使ってないので、これも少し変更されています。
グロタンディーク宇宙の定義では、所属関係 $`\in`$ は、外側のZF宇宙にある所属関係をそのまま使っていますが、集合 $`U`$ 上の二項関係 $`\epsilon \in U\times U`$ があって、$`\epsilon`$ に関してZF集合論のモデルになっている場合も考えることにします。次は要求しません。
$`\text{For }x, y\in U\\
\quad x\Uin y \Iff x\in y
`$
ただし、等号は外側のZF宇宙と同じ解釈を採用します。$`U`$ 独自の等値性は考えません。例えば、外延性の公理は次のようになります。
$`\quad \forall x, y\in U.[\, x = y \Iff \forall t\in U.(t\Uin x \Iff t\Uin y) \,]`$
以下、グロタンディーク宇宙は独自の所属関係を持ってもいいとします。独自の所属関係を沿えて、「グロタンディーク宇宙 $`(U, \Uin)`$」のように書きます。もちろん、外側のZF宇宙の所属関係をそのまま使ってもかまいません。そのときは $`U = (U, \in)`$ のように書きます。
例を挙げます； $`U = (U, \in)`$ を通常のグロタンディーク宇宙として、$`V := \{1\}\times U`$ とします。$`V`$ は $`U`$ のコピーで、$`U`$ と無交差〈disjoint〉です。$`V`$ の所属関係を次のように定義します。
$`\text{For }(1, x), (1, y)\in V\\
\quad (1, x) \Uin (1, y) :\Iff x\in y
`$
$`(V, \Uin)`$ は $`(U, \in)`$ の（グロタンディーク宇宙としての）無交差なコピーになります。
グロタンディーク宇宙が持つ構造
「ZF宇宙、グロタンディーク宇宙、型宇宙」では、ZF集合論のほんとの宇宙を $`\mbf{ZF}`$ と書き、対応する集合圏を $`\mathbb{SET}_\mbf{ZF}`$ と書きました。ここでは、十分に大きな集合圏を $`\mathbb{SET}`$ と書きます。$`|\mathbb{SET}|`$ は十分に大きな宇宙です。
外部環境となる集合圏 $`\mbb{SET}`$ のなかのグロタンディーク宇宙 $`U`$ について考えます。グロタンディーク宇宙は、ZF集合論のモデルとなる集合ですが、ZF集合論の公理から無限公理は外しておきます。無限を扱えない宇宙（例えば、すべての遺伝的有限集合〈hereditarily finite set〉からなる宇宙）も認めたいからです。
ZF集合論の公理を、$`U`$ の要素（$`U`$-小集合）から $`U`$ の要素を作り出す演算だと解釈すると、次の演算が要求されます。$`\Sigma`$ は、外の集合圏 $`\mbb{SET}`$ のシグマ型構成です。
- 順序なしペアの構成：
$`\{\hyp,\hyp\} : U\times U\to U \In \mbb{SET}`$ - 述語による部分集合の構成（分出公理）：
$`\{\hyp \mid \hyp\} : \Sigma(x\in U \mid \mrm{AMap}(x, \mbf{B}) )\to U \In \mbb{SET}`$ - ファミリーの合併集合の構成：
$`\bigcup(\hyp) : \Sigma(x\in U \mid \mrm{AMap}(x, U) ) \to U \In \mbb{SET}`$ - ベキ集合の構成：
$`\mrm{Pow}(\hyp) : U \to U \In \mbb{SET}`$ - ファミリーの像集合の構成（置換公理）：
$`\{\hyp \vdash \hyp\} : \Sigma(x\in U\mid \mrm{AMap}(x, U)) \to U\In \mbb{SET}`$
これらの演算（集合の構成子）に引数を渡した形は次のようです。
- 順序なしペア：
$`\{x,y\} \:\text{ for } x, y \in U`$ - 述語による部分集合：
$`\{t\in x\mid p(t)\} \:\text{ for } x\in U, p\in \mrm{AMap}(U, \mbf{B})`$ - ファミリーの合併集合：
$`\bigcup(t\in X \mid f(t)) \:\text{ for } x\in U, f\in \mrm{AMap}(x, U)`$ - ベキ集合：
$`\mrm{Pow}(x) \:\text{ for } x \in U`$ - ファミリーの像集合：
$`\{ t\in x \vdash f(t) \} \:\text{ for } x\in U, f\in \mrm{AMap}(x, U)`$
最後のファミリーの像集合は、みやすさから次の形（左右を逆にする）を使うことにします。
$`\quad \{f(t) \dashv t\in x\}`$
$`U`$ の空集合が、$`|\mbb{SET}|`$ の空集合と一致するとは限らないので、定数記号として $`\theta`$ を準備し、$`U`$ の空集合を表すと約束します。
$`\Uin, \theta`$ は別な記号を準備しましたが、5つの演算〈構成子〉には下付きの $`U`$ を付けることにすると、以下のような定数記号、演算記号〈構成子記号 | 関数記号〉によりグロタンディーク宇宙が記述できます。
- $`{\Uin} = {\in_U}`$
- $`\theta = \emptyset_U`$
- $`\{\hyp, \hyp\}_U`$
- $`\{\hyp \mid \hyp \}_U`$
- $`\bigcup_U(\hyp \mid \hyp)`$
- $`\mrm{Pow}_U(\hyp)`$
- $`\{\hyp \dashv \hyp \}_U`$
$`U`$ を構造の名前だとして、台集合は $`\u{U}`$ としましょう。すると、構造としてのグロタンディーク宇宙 $`U`$ は次のように書けることになります。
$`\quad U = (\u{U}, \Uin, \theta, \{\hyp, \hyp\}_U, \{\hyp \mid \hyp \}_U, \bigcup_U, \mrm{Pow}_U, \{\hyp \dashv \hyp \}_U )`$
これはさすがに長過ぎるので、適当に省略します。例えば：
$`\quad U = (\u{U}, \Uin, \theta)`$
$`U`$ 独自の演算〈構成子〉を示すための下付きの $`U`$ も、文脈から明らかなら省略するかも知れません。
非継承的グロタンディーク宇宙の公理系
所属関係を、外の宇宙 $`|\mbb{SET}|`$ からそのまま受け継ぐとは限らないグロタンディーク宇宙を、非継承的グロタンディーク宇宙〈uninherited Grothendieck universe〉と呼ぶことにします。グロタンディーク宇宙の“なかの人”になってしまえば、外の世界は見えない*1ので、所属関係が外と同じかどうかは内部の人には無意味です。内部からの観点では、ZF集合論の公理を満たすかどうかだけが問題で、外部の解釈と一致するかどうかなんて、そもそも問題に出来ないのです。
以下は、ZF集合論の公理達の外部から見たときの記述です。
外延性の公理：
$`\quad \forall x, y\in U.(\, \forall z\in U.( z \Uin x \Iff z \Uin y) \Imp x = y \,)`$
空集合の存在公理：
$`\quad \forall x\in U.\, \lnot(x \Uin \theta)`$
順序無しペアの存在公理：
$`\quad \forall x, y\in U.\, \forall w\in U.(\, w \Uin \{x, y\}_U \Iff w=x \lor w=y \,)
`$
分出公理：
$`\quad \forall x\in U. \forall p\in \mrm{AMap}(x, \mbf{B}).\, \forall w\in U.(\, w \Uin \{ x\mid p\}_U \Iff w \Uin x \land p(w) = 1 \,)
`$
合併の存在公理：
$`\quad \forall x\in U.\forall f\in \mrm{AMap}(x, U).\\
\qquad \forall z\in U.(\, z \Uin \bigcup_U(x\mid f) \Iff \exists w\in U. (w \Uin x \land z \Uin f(w) )\,)`$
ベキ集合の存在公理：
$`\quad \forall x\in U.\,
\forall z\in U.(\, z \Uin \mrm{Pow}_U(x) \Iff \forall w\in U.(w \Uin z \Imp w\Uin x) \,)
`$
置換公理：
$`\quad \forall x\in U.\forall f\in \mrm{AMap}(x, U).\,
\forall w\in U.\\
\qquad w \Uin \{f \dashv x\}_U \Iff
\exists t\in U.\, t\Uin x \land w = f(t)
`$
正則性公理〈基礎の公理〉：
$`\quad \forall x\in U.[\,
x\ne \theta \Imp
\exists y\in U. ( y \Uin x \land \forall z\in U. (z\Uin x \Imp \lnot( z \Uin y)))
\,]
`$
繰り返しますが、分出公理と置換公理は、ZF集合論のもとの公理とは意味合いが違っています。合併の定義も微妙に違います。しかし、$`U`$ のなかに入ると、内部だけで（外部に言及しないで）ZF集合論が出来ます。
ZF集合論が出来ることがグロタンディーク宇宙の条件なので、上記の公理達は非継承的グロタンディーク宇宙の公理系となります。
非継承的グロタンディーク宇宙 $`U`$ では、等号（等値性）以外は、$`U`$ 独自の構造でかまいません。外側の宇宙から継承する義務はありません。このことにより、より柔軟にグロタンディーク宇宙を使えるようになると思います。
*1:[追記]$`\mrm{AMap}(x, \mbf{B})`$ と $`\mrm{AMap}(x, U)`$ の要素は、外部のモノだけど内部からも見えてますね。[/追記]
