「名前の解釈： 正確なコミュニケーションのために」の続きです。$`\newcommand{\In}{\text{ in }}
\newcommand{\BR}[1]{ \left[\!\left[ {#1} \right]\!\right] }
\newcommand{\hyp}{ \text{－} }
\newcommand{\mbf}[1]{ \mathbf{#1} }
\newcommand{\mrm}[1]{ \mathrm{#1} }
\newcommand{\mbb}[1]{ \mathbb{#1} }
\newcommand{\BRP}[1]{ \left[ !\, {#1} \,! \right] }
\newcommand{\BRG}[1]{ \langle\!\langle {#1} \rangle\!\rangle }
\newcommand{\BRR}[1]{\left[\!\left( {#1} \right)\!\right] }
\newcommand{\T}[1]{\text{#1} }
\newcommand{\parto}{ \supset\!\to }
`$
内容：
グロタンディーク宇宙
「名前の解釈： 正確なコミュニケーションのために」で意味関数〈解釈 | 意味割り当て〉を導入しました。意味関数も関数なので、域と余域を持ちます。まず余域を考えます。意味関数の余域はグロタンディーク宇宙（と呼ばれる集合）と考えます。ひとつのグロタンディーク宇宙で足りないときは、幾つかのグロタンディーク宇宙を一緒に考えます。グロタンディーク宇宙の直積やベキ集合も使ってかまいません。
グロタンディーク宇宙に関しては以下の過去記事で述べています。
- グロタンディーク宇宙って何なんだ？（導入的解説）
- 贅沢主義者のグロタンディーク宇宙 （追加の操作）
- ZF宇宙、グロタンディーク宇宙、型宇宙 （型理論との関係）
デフォルトのグロタンディーク宇宙を $`\mbb{U}`$ とします*1。$`\mbb{U}`$ はZFC集合論（現在主流の集合論）におけるひとつの集合に過ぎません。したがって、次のような集合を構成することは許されています。
- 直積 $`\mbb{U}^2 = \mbb{U}\times \mbb{U}`$
- ベキ集合 $`\mrm{Pow}(\mbb{U} )`$
- 関数集合 $`\mrm{Map}(X, \mbb{U} ) \:\text{ for some }X \in \mbb{U}`$
デフォルトのグロタンディーク宇宙 $`\mbb{U}`$ の要素を小さい集合〈small set〉と呼びます。
グロタンディーク宇宙の性質（推移性）から、「$`x\in \mbb{U}`$ ならば $`x\subseteq \mbb{U}`$」は言えますが、「$`x\subseteq \mbb{U}`$ ならば $`x\in \mbb{U}`$」は一般には言えません。$`x\subseteq \mbb{U}`$ である“ZFC集合論の集合”を $`\mbb{U}`$ のクラス〈class | 類〉と呼びます。定義から、$`\mbb{U}`$ の小さい集合は、必ず $`\mbb{U}`$ のクラスです。$`\mbb{U}`$ の小さい集合ではない $`\mbb{U}`$ のクラスを、$`\mbb{U}`$ の真のクラス〈proper class〉と呼びます。
$`\mbb{U}`$ の真のクラスを、もっと大きなグロタンディーク宇宙 $`\mbb{U'}`$ 内の小さい集合として扱うことがあります。$`\mbb{U}\in \mbb{U'}`$ です。必要なら、次のようなグロタンディーク宇宙達の系列を考えます。
$`\quad \mbb{U} \in \mbb{U'} \in \mbb{U''}\in \cdots`$
意味論のメタレベルで使う用語達「集合」、「小さい集合」、「大きい集合」の意味・用法がそもそも曖昧なので、ここで曖昧性を説明しておきます。
集合
- ZFC集合論の集合は「集合」と呼ぶ。
- デフォルトのグロタンディーク宇宙 $`\mbb{U}`$ の小さい集合を単に「集合」と呼ぶかも知れない。
- 考えている範囲内のグロタンディーク宇宙達の系列の、どれかのグロタンディーク宇宙の小さい集合を単に「集合」と呼ぶかも知れない。
小さい集合
- デフォルトのグロタンディーク宇宙 $`\mbb{U}`$ の小さい集合は「小さい集合」と呼ぶ。
- 考えている範囲内のグロタンディーク宇宙達の系列の、どれかのグロタンディーク宇宙の小さい集合を「小さい集合」と呼ぶかも知れない。
大きい集合
- デフォルトのグロタンディーク宇宙 $`\mbb{U}`$ のクラスを「大きい集合」と呼ぶ。
- デフォルトのグロタンディーク宇宙 $`\mbb{U}`$ の真のクラスを「大きい集合」と呼ぶこともある。
- デフォルトのグロタンディーク宇宙 $`\mbb{U}`$ より上のレベルのグロタンディーク宇宙の小さい集合を「大きい集合」と呼ぶかも知れない。
- ZFC集合論の集合を「大きい集合」と呼ぶかも知れない。
- デフォルトのグロタンディーク宇宙 $`\mbb{U}`$ には属さないZFC集合論の集合を「大きい集合」と呼ぶかも知れない。
ここでは、「集合」はZFC集合論の集合か、またはデフォルトのグロタンディーク宇宙 $`\mbb{U}`$ の小さい集合です（曖昧なまま使う）。「大きい集合」は $`\mbb{U'}`$ の小さい集合のことです。「とても大きい集合」は $`\mbb{U''}`$ の小さい集合のことです。この用法だと、「小さい集合は大きい集合である」は正しい命題なので注意してください。
名前の意味関数とは？
名前の集合を $`\mrm{Name}`$ とします。集合 $`\mrm{Name}`$ は特定の状況では特定の具体的な集合になります。
意味関数をスコット・ブラケットで書くことにして、意味関数は次のような関数でしょうか？
$`\quad \BR{\hyp} : \mrm{Name} \to \mbb{U} \In \mbf{SET}`$
残念ながら、事情はそれほど単純ではありません。
「名前の解釈： 正確なコミュニケーションのために」で述べたように、名前の種類を考えないと解釈〈意味割り当て〉はできないので、名前の種類〈name sort | sort of name〉の集合を $`\mrm{NameSort}`$ として、スコット・ブラケットは名前の種類も引数に取ります。
$`\quad \BR{\xi, s} \:\text{ where }\xi\in \mrm{Name}, s\in \mrm{NameSort}`$
読みやすくするために、$`\BR{\xi, s}`$ を $`\BR{\xi \text{ as }s}`$ と書くことにします。
「名前の解釈： 正確なコミュニケーションのために」では、名前の種類ごとに括弧の形を変えることにしました。
$`\quad \BRP{\alpha} := \BR{\alpha \text{ as }\T{固有名}}`$
$`\quad \BRG{\beta} := \BR{\beta \text{ as }\T{一般名}}`$
$`\quad \BRR{\xi\T{の}\gamma} := \BR{\xi\T{の}\gamma \text{ as }\T{構成素役割り名}}`$
我々は、$`\mrm{NameSort} = \{\T{固有名}, \T{一般名}, \T{構成素役割り名}\}`$ としていたので、括弧の形を変えるのは便利な書き方ですが、名前の種類が10も20もあると、括弧の形を変えるのは現実的ではなくなります。
さて、名前の種類を考慮した意味関数は次のようでしょうか？
$`\quad \BR{\hyp} : \mrm{Name}\times\mrm{NameSort} \to \mbb{U} \In \mbf{SET}`$
そうもいきません。
例えば、「モノイド」は一般名なので $`\BRG{\T{モノイド}}`$ は意味を持ちます（解釈可能です）が、固有名ではないので $`\BRP{\T{モノイド}}`$ は意味不明（解釈不可能）です。「円周率」は固有名なので $`\BRP{\T{円周率}}`$ は意味を持ちますが、構成素役割り名ではないので $`\BRR{\T{モノイドの円周率}}`$ は意味不明です。
つまり、意味関数〈スコット・ブラケット〉は、通常の関数〈全域関数〉ではない、ということです。意味不明とは、関数値が未定義なことです。未定義を許す関数は部分関数〈partial function〉です。部分関数を記号 '$`\parto`$' で表すことにして、意味関数（まだ暫定的）は次のようです。
$`\quad \BR{\hyp} : \mrm{Name}\times\mrm{NameSort} \parto \mbb{U} \In \mbf{SET}`$
なお、これは以下の図式の $`D`$ （部分関数の定義域）を暗黙化して略記したものです。部分関数である意味関数〈スコット・ブラケット〉は、包含パート（$`\BR{\hyp}{_\mrm{incl}}`$）と全域パート（$`\BR{\hyp}{_\mrm{total}}`$）に分解されます。
$`\quad \xymatrix{
{}
&{D} \ar@{_{(}->}[dl]_{\BR{\hyp}{_\mrm{incl}} } \ar[dr]^{\BR{\hyp}{_\mrm{total}} }
&{}
\\
{\mrm{Name}\times\mrm{NameSort}}
&{}
&{\mbb{U}}
}\\
\quad \In \mbf{SET}
`$
文脈の考慮
「名前の解釈： 正確なコミュニケーションのために」において、文脈によって名前の解釈が変わると言いました。「文脈とは何か？」と聞かれると、これはよく分かりません。一般論として答えるのは難しいですが、特定の場面ごとに文脈の定義をすることは可能かも知れません。文脈達の集合を定義可能な状況を想定して、文脈達の集合〈set of contexts〉を $`\mrm{Ctx}`$ とします。
文脈を考慮するなら、意味関数〈スコット・ブラケット〉は次のようになるでしょう。
$`\quad \BR{\hyp} : \mrm{Name}\times\mrm{NameSort}\times \mrm{Ctx} \parto \mbb{U} \In \mbf{SET}`$
名前の解釈においては「まず文脈ありき」だと考えるなら、$`\mrm{Ctx}`$ （文脈達の集合）を第一引数にすべきでしょう。が、引数の順番は変更できる*2ので、今は引数の順番は気にしないことにします。
文脈を $`V, W`$ などの変数で表すことにすると、意味関数〈スコット・ブラケット〉に引数を渡すと次の形です。
$`\quad \BR{\xi, s, V} \:\text{ where }\xi\in \mrm{Name}, s\in \mrm{NameSort}, V\in \mrm{Ctx}`$
読みやすくするために、$`\BR{V, \xi, s}`$ を $`\BR{\xi \text{ as }s \text{ w.r.t } V}`$ と書くことにします。$`\text{ w.r.t}`$ は "with respect to" の略記です。
コミュニケーションの特定時点において、その時の文脈を取り出して曖昧性なく正確に書き下すのは難しいことです。文脈の共有と合意は「なんとなく」「雰囲気的に」「暗黙に」行われているからです。文脈を書き下す手段も通常は用意されていません。でも、文脈達に（その正体はよく分からなくても）名前を付けて、文脈 $`V`$ と $`W`$ は同じか違うか、という程度の議論はできるでしょう。
意味領域の考慮
意味関数〈スコット・ブラケット〉の余域は、デフォルトのグロタンディーク宇宙 $`\mbb{U}`$ でよいでしょうか？ 例えば、文脈 $`V`$ において「用語『集合』は『小さい集合』の意味で使う」と合意されていたとします。すると、次が成立します。
$`\quad \BR{\T{集合} \T{ as 一般名 w.r.t }V } = \BR{\T{集合} \T{ w.r.t }V } = \mbb{U}`$
意味関数の値は、余域〈意味領域〉の要素でなくてなりません。しかし、$`\mbb{U}\in \mbb{U}`$ とは出来ない*3ので、余域〈意味領域〉を $`\mbb{U}`$ とするのではダメです。もっと広い余域が必要です。
デフォルトのグロタンディーク宇宙 $`\mbb{U}`$ より広い（レベルが上の）グロタンディーク宇宙 $`\mbb{U'}`$ を余域とすればどうでしょう。
$`\quad \BR{\hyp} : \mrm{Name}\times\mrm{NameSort}\times \mrm{Ctx} \parto \mbb{U'} \In \mbb{SET}`$
$`\mbb{U'}`$ には $`\mbb{U}`$ が入っているし、$`\mbb{U}`$ の真のクラスも入っています。$`\mbb{U}`$ のすべてのクラスの集合 $`\mrm{Pow}(\mbb{U})`$ でさえ $`\mbb{U'}`$ に入っています。意味関数〈スコット・ブラケット〉の余域である意味領域には、$`\mbb{U'}`$ を取ればたいてい間に合います。$`\mbb{U'}`$ からもはみ出してしまう巨大な集合を扱うなら、$`\mbb{U''}`$ を余域に設定します。
必要に応じて大きなグロタンディーク宇宙を余域に使えばいいでしょう。グロタンディーク宇宙は集合論的な概念なので、圏論的な世界観が欲しいときは、圏論的世界（の一部）を意味領域と考えてもかまいません。以下の表は「曖昧性を減らす： Diag構成を事例として // 世界の構造」からの（わずかに変更した）コピーで、圏論的世界のグリッド構造を表しています。$`d`$ はデフォルトのレベルです。
| $`r = d `$ | $`r = d + 1`$ | $`r = d + 2`$ | |
| $`\mbb{U}`$ | $`\mbb{U'}`$ | $`\mathbb{U''}`$ | |
| $`n = 0`$ | $`{\bf Set}`$ | $`{\bf SET}`$ | $`\mathbb{SET}`$ |
| $`n = 1`$ | $`{\bf Cat}`$ | $`{\bf CAT}`$ | $`\mathbb{CAT}`$ |
| $`n = 2`$ | $`2{\bf Cat}`$ | $`2{\bf CAT}`$ | $`2\mathbb{CAT}`$ |
