たいていの公理系はミニマリスト・アプローチで定義されていて、無駄な（他の公理達から導出可能な）公理は入れないで、必要最小限の公理達から構成されています。しかし、導出可能な命題を最初から公理系に入れておくのが絶対にダメなわけではないです。「この贅沢者めが」という誹りを受けるだけです。
導出可能な定理も含まれる公理系（冗長な公理系、独立ではない公理系）は節約と経済性の原則には反しますが、使い勝手は向上することがあります。グロタンディーク宇宙の公理系を節約と経済性の原則を無視して再定義してみます。$`\newcommand{\mrm}[1]{\mathrm{#1} }
\newcommand{\In}{\text{ in }}
\newcommand{\mbf}[1]{\mathbf{#1} }
\newcommand{\Imp}{\Rightarrow}
\newcommand{\hyp}{\text{－} }
\newcommand{\dtimes}{\mathop{!\!{\times}} }
\newcommand{\dto}{\mathrel{!\!{\to}} }
\newcommand{\LB}{ \{\!( }
\newcommand{\RB}{ )\!\} }
`$
内容：
グロタンディーク宇宙
グロタンディーク宇宙〈Grothendieck universe〉 $`U`$ の通常の公理系は次のようです。
- $`U`$ は、所属関係に関して推移的である： $`\forall x, y.\; x\in U \land y\in x \Imp y\in U`$
- $`U`$ は、順序なしペアに関して閉じている： $`\forall x, y.\; x, y\in U \Imp \{x, y\}\in U`$
- $`U`$ は、ベキ集合構成に関して閉じている： $`\forall x.\; x\in U \Imp \mrm{Pow}(x)\in U`$
- $`U`$ は、族〈ファミリー〉の合併構成に関して閉じている： $`\forall x, f.\; x\in U \land f\in \mrm{Map}(x, U) \Imp \bigcup(f)\in U`$
公理に出てくる論理式はZFC集合論のなかで解釈されます。集合に関する演算子／構成子達
$`\quad \{\hyp,\hyp\}, \mrm{Pow}(\hyp), \mrm{Map}(\hyp, \hyp), \bigcup(\hyp)`$
は、事前に（ZFC集合論により）定義されているとします。
自然数と自然数全体の集合がないと無限を扱えないので、次の条件も入れておきます。
- $`U`$ は、自然数全体の集合を要素として含む： $`\mbf{N}\in U`$
これだけ（合計で5つ）の公理があれば、必要なモノは組み立てることができます。例えば、$`x, y\in U`$ に対して直積集合 $`x\times y`$ は $`U`$ 内で作れます。
「最小限の素材さえあれば、必要なモノは後から組み立てればいい」がミニマリスト／節約主義者の発想です。一方、「必要なモノは最初から入っていたら便利なんじゃないの」が贅沢主義者の発想です。次節で贅沢主義者の観点からグロタンディーク宇宙の公理系を設計してみます。
贅沢なグロタンディーク宇宙
贅沢主義者のグロタンディーク宇宙の公理を述べます。次の2つは前節と同じです。
- $`U`$ は、所属関係に関して推移的である。
- $`U`$ は、自然数全体の集合を要素として含む。
自然数はノイマン流に定義されているとします。なので、$`0 = \emptyset`$ です。
上記2つの公理から次が言えます。
- $`0 \in U`$
- $`1 \in U`$
- $`2 \in U`$
- $`\cdots`$
- $`n \in U\; \text{ for } n\in \mbf{N}`$
$`U`$ の要素だと考えた自然数 $`n`$ を $`\bar{n}`$ と書くことにします。特に、$`\bar{0}, \bar{1}`$ は太字でも書くことにします。
$`\quad \mbf{0} = \bar{0} = 0 = \emptyset\\
\quad \mbf{1} = \bar{1} = 1 = \{\emptyset\}
`$
ここで、贅沢品を導入します。$`U`$ はシグマ型構成とパイ型構成に関して閉じているとします。前節の「族〈ファミリー〉の合併構成に関して閉じている」に似た形の公理になります。
- $`U`$ は、シグマ型構成に関して閉じている： $`\forall x, f.\; x\in U \land f\in \mrm{Map}(x, U) \Imp \Sigma(f)\in U`$
- $`U`$ は、パイ型構成に関して閉じている： $`\forall x, f.\; x\in U \land f\in \mrm{Map}(x, U) \Imp \Pi(f)\in U`$
$`\Sigma(\hyp), \Pi(\hyp)`$ も、事前に（ZFC集合論により）定義されているとします。シグマ型／パイ型を公理的に定義することも出来ますが、ここでは外側のZFC集合論でチマチマ頑張って作ったモノだとします。シグマ型／パイ型には幾つかの書き方があります。
$`\quad \Sigma(f) = \Sigma(x \mid f) = \sum (x \mid f) = {\displaystyle \sum_{t\in x} f(t) }\\
\quad \Pi(f) = \Pi(x \mid f) = \prod (x \mid f) = {\displaystyle \prod_{t\in x} f(t) }
`$
圏論的に言えば、シグマ型は以下の図式がプルバック四角形〈デカルト四角形〉になるという特徴を持ちます（詳細は割愛）。
$`\quad \xymatrix{
\Sigma(x \mid f) \ar[r] \ar[d]_{\pi^f}
\ar@{}[dr]|{\text{p.b.} }
& \widetilde{U} \ar[d]^p
\\
x \ar[r]_f
& U
}\\
\quad \In \mbf{SET}
`$
このようなシグマ型の特徴付けは後知恵です。贅沢主義者の公理系とは、後知恵に基づき“最小限”の基準を大幅に引き上げてしまった条件一式のことです。
パイ型は、シグマ型に出てくる写像 $`\pi^f`$ のセクションの集合です。
$`\quad \Pi(x \mid f) := \mrm{Sect}(\pi^f : \Sigma(x \mid f) \to x)`$
もうひとつ、ご都合主義的な贅沢品として、集合の内包的記法に相当するオメガ型構成〈omega type construction〉を入れておきます。
$`\text{For } x \in U\\
\text{For } f \in \mrm{Map}(x, U)\\
\quad \Omega(f) = \Omega(x \mid f) := \{t\in x\mid f(t)\ne \emptyset\}
`$
「オメガ型」という言葉は、今僕がでっち上げたものです。トポスの部分対象分類子に大文字オメガを使う習慣があるので、それにちなんだものです。オメガ型構成は暗黙に使っているのですが、型構成子（集合を作る演算）と意識したほうがいでしょう。
この場合、ファミリー $`f`$ は述語として使っています。$`f(t)\ne \emptyset`$ は、述語とみなした $`f`$ の値が“偽ではない”ということです。
オメガ型も贅沢なグロタンディーク宇宙〈luxury Grothendieck universe〉の装備品のひとつです。
- $`U`$ は、オメガ型構成に関して閉じている： $`\forall x, f.\; x\in U \land f\in \mrm{Map}(x, U) \Imp \Omega(f)\in U`$
シグマ型、パイ型、オメガ型を構成する演算子記号として、次の短縮記号を使うと簡潔に書けます。
$`\text{For } x \in U\\
\text{For } f \in \mrm{Map}(x, U)\\
\quad x \dtimes f := \Sigma( x \mid f)\\
\quad x \dto f := \Pi( x \mid f)\\
\quad \LB x \mid f \RB := \Omega(x \mid f)
`$
右に感嘆符を添える記号は、「型理論で出てくる射影の整理と約束」「アロー圏 ＝ バンドルの圏」で導入・使用したものです。
贅沢主義のメリット・デメリット
贅沢なグロタンディーク宇宙の条件は次のようにまとめられます。
- 所属関係に関して推移的で、自然数全体の集合を要素として含み、シグマ型構成・パイ型構成・オメガ型構成に関して閉じている集合
これは実際、強力な機能性を最初から備えた構造です。ミニマリスト／節約主義者のグロタンディーク宇宙と比べて、自分で準備をすることなく、やりたいことがいきなり出来ます。シグマ型構成・パイ型構成・オメガ型構成は、強力なだけでなく使い勝手が快適です。
デメリット／問題点は、最初から必要なモノ一式が備わった環境しか知らないと、何もない所から必要なモノを自作するサバイバル能力が鍛えられないことでしょう。しかし、何もない所から自作するのに時間と労力を使い過ぎるのもどうなのかな？ と思ったりします。
