雑記帳
自然数対象を持つトポスで「1+1」を圏論的に計算してみる
目次
•
•
•
普遍性の観点から 1+1 を計算してみる
目的
自然数対象の記事で行った加法の定義の正当性を少しでも理解してほしい！
自然数対象の記事で
\[
(+_{{\mathbb{N}}}) = ({\rm rec}_{{\mathbb{N}}}({\rm arrToEl}({\mathbb{N}}),\lambda[{\rm ev} {\sf \, ⨟ \,} {\rm succ}])\times {\mathbb{N}}){\sf \, ⨟ \,} {\rm ev}
\]
といった感じに自然数の足し算 \((+_{{\mathbb{N}}}):{\mathbb{N}}\times {\mathbb{N}}\rightarrow {\mathbb{N}}\) の定義を行ったが、何の説明もなく定義が漠然と提示されただけでは「それが本当に足し算として機能するのか」という疑念を抱くのが普通だろう。
ということで、このページではまず「その射が足し算として本当に機能しているのかもしれない」という様子を1人でも多くの人に垣間見てもらえたらいいな～なんてことを期待しながら「純粋圏論的な普遍性を駆使した 1+1 の計算のデモンストレーション」を紹介していく。
(そして「圏論が数学基礎を提供する」という点についても、これを通して納得してくれる人が増えてくれたらな。)
余談
因みにしっかりと一般論から、そのようにして構成される射が「自然数の足し算としての意味を持ち、交換法則や結合法則が成立する」というところまで全て厳密に示すことはできるのだが、純粋圏論的な部分対象の取り扱いを始めとする従来の集合論的な考え方とは乖離のある、慣れないと少しわかりにくい理論展開となっている。つまるところ「それが本当に足し算として機能するのか」という疑念を払拭する第一歩として、その込み入った一般論を紹介するのは相応しくないだろうと思い、まずは具体的な計算デモを紹介することにした。
圏論でも「自然数の足し算」という超絶具体的なことができてしまうことを知ってほしい！
圏論というと「しゃれた専門用語を沢山使って物事をただ意味もなく複雑に説明し直すだけで、具体的なことは何もできない」という偏見を持つ人も少なくないとは思うが、実は「数の加法・乗法」のような具体的な計算も純粋圏論的に処理できるということをそういった人たちに確認してほしい。
具体的な計算の一連の流れ
まずは計算の全体像を大まかにでも把握していただくため、\(1+1\) が \(2\) になるまでの計算の一連の流れを一気に書き下す。(式変形の際に、どの公理を使用しているのかは次節で詳しく説明する。)
\[
\begin{align}
1+1 &= 1_{{\mathbb{N}}}+1_{{\mathbb{N}}} \\
&= \langle 1_{{\mathbb{N}}},1_{{\mathbb{N}}} \rangle {\sf \, ⨟ \,} (+_{{\mathbb{N}}}) \\
&= \langle {\rm zero} {\sf \, ⨟ \,} {\rm succ}, {\rm zero} {\sf \, ⨟ \,} {\rm succ} \rangle {\sf \, ⨟ \,} (+_{{\mathbb{N}}}) \\
&= \langle {\rm zero} {\sf \, ⨟ \,} {\rm succ}, {\rm zero} {\sf \, ⨟ \,} {\rm succ} \rangle {\sf \, ⨟ \,} (({\rm rec}_{{\mathbb{N}}}({\rm arrToEl}({\mathbb{N}}),\lambda[{\rm ev} {\sf \, ⨟ \,} {\rm succ}])\times {\mathbb{N}}){\sf \, ⨟ \,} {\rm ev}) \\
&= \langle {\rm zero} {\sf \, ⨟ \,} {\rm succ}, {\rm zero} {\sf \, ⨟ \,} {\rm succ} \rangle {\sf \, ⨟ \,} ({\rm rec}_{{\mathbb{N}}}({\rm arrToEl}({\mathbb{N}}),\lambda[{\rm ev} {\sf \, ⨟ \,} {\rm succ}])\times {\mathbb{N}}){\sf \, ⨟ \,} {\rm ev} \\
&= (\langle {\rm zero} {\sf \, ⨟ \,} {\rm succ}, {\rm zero} {\sf \, ⨟ \,} {\rm succ} \rangle {\sf \, ⨟ \,} ({\rm rec}_{{\mathbb{N}}}({\rm arrToEl}({\mathbb{N}}),\lambda[{\rm ev} {\sf \, ⨟ \,} {\rm succ}])\times {\mathbb{N}})) {\sf \, ⨟ \,} {\rm ev} \\
&= (\langle ({\rm zero} {\sf \, ⨟ \,} {\rm succ}) {\sf \, ⨟ \,} {\rm rec}_{{\mathbb{N}}}({\rm arrToEl}({\mathbb{N}}),\lambda[{\rm ev} {\sf \, ⨟ \,} {\rm succ}]), ({\rm zero} {\sf \, ⨟ \,} {\rm succ}) {\sf \, ⨟ \,} {\mathbb{N}} \rangle) {\sf \, ⨟ \,} {\rm ev} \\
&= (\langle {\rm zero} {\sf \, ⨟ \,} ({\rm succ} {\sf \, ⨟ \,} {\rm rec}_{{\mathbb{N}}}({\rm arrToEl}({\mathbb{N}}),\lambda[{\rm ev} {\sf \, ⨟ \,} {\rm succ}])), {\rm zero} {\sf \, ⨟ \,} {\rm succ} \rangle) {\sf \, ⨟ \,} {\rm ev} \\
&= (\langle {\rm zero} {\sf \, ⨟ \,} ({\rm rec}_{{\mathbb{N}}}({\rm arrToEl}({\mathbb{N}}),\lambda[{\rm ev} {\sf \, ⨟ \,} {\rm succ}]) {\sf \, ⨟ \,} \lambda[{\rm ev} {\sf \, ⨟ \,} {\rm succ}]), {\rm zero} {\sf \, ⨟ \,} {\rm succ} \rangle) {\sf \, ⨟ \,} {\rm ev} \\
&= (\langle ({\rm zero} {\sf \, ⨟ \,} {\rm rec}_{{\mathbb{N}}}({\rm arrToEl}({\mathbb{N}}),\lambda[{\rm ev} {\sf \, ⨟ \,} {\rm succ}])) {\sf \, ⨟ \,} \lambda[{\rm ev} {\sf \, ⨟ \,} {\rm succ}], {\rm zero} {\sf \, ⨟ \,} {\rm succ} \rangle) {\sf \, ⨟ \,} {\rm ev} \\
&= (\langle ({\rm zero} {\sf \, ⨟ \,} {\rm rec}_{{\mathbb{N}}}({\rm arrToEl}({\mathbb{N}}),\lambda[{\rm ev} {\sf \, ⨟ \,} {\rm succ}])) {\sf \, ⨟ \,} \lambda[{\rm ev} {\sf \, ⨟ \,} {\rm succ}], ({\rm zero} {\sf \, ⨟ \,} {\rm succ}) {\sf \, ⨟ \,} {\mathbb{N}} \rangle) {\sf \, ⨟ \,} {\rm ev} \\
&= (\langle {\rm zero} {\sf \, ⨟ \,} {\rm rec}_{{\mathbb{N}}}({\rm arrToEl}({\mathbb{N}}),\lambda[{\rm ev} {\sf \, ⨟ \,} {\rm succ}]), {\rm zero} {\sf \, ⨟ \,} {\rm succ} \rangle {\sf \, ⨟ \,} (\lambda[{\rm ev} {\sf \, ⨟ \,} {\rm succ}]\times {\mathbb{N}})) {\sf \, ⨟ \,} {\rm ev} \\
&= \langle {\rm zero} {\sf \, ⨟ \,} {\rm rec}_{{\mathbb{N}}}({\rm arrToEl}({\mathbb{N}}),\lambda[{\rm ev} {\sf \, ⨟ \,} {\rm succ}]), {\rm zero} {\sf \, ⨟ \,} {\rm succ} \rangle {\sf \, ⨟ \,} ((\lambda[{\rm ev} {\sf \, ⨟ \,} {\rm succ}]\times {\mathbb{N}}) {\sf \, ⨟ \,} {\rm ev}) \\
&= \langle {\rm zero} {\sf \, ⨟ \,} {\rm rec}_{{\mathbb{N}}}({\rm arrToEl}({\mathbb{N}}),\lambda[{\rm ev} {\sf \, ⨟ \,} {\rm succ}]), {\rm zero} {\sf \, ⨟ \,} {\rm succ} \rangle {\sf \, ⨟ \,} ({\rm ev} {\sf \, ⨟ \,} {\rm succ}) \\
&= \langle {\rm arrToEl}({\mathbb{N}}), {\rm zero} {\sf \, ⨟ \,} {\rm succ} \rangle {\sf \, ⨟ \,} ({\rm ev} {\sf \, ⨟ \,} {\rm succ}) \\
&= \langle \lambda[{\rm prj}_2 {\sf \, ⨟ \,} {\mathbb{N}}], {\rm zero} {\sf \, ⨟ \,} {\rm succ} \rangle {\sf \, ⨟ \,} ({\rm ev} {\sf \, ⨟ \,} {\rm succ}) \\
&= \langle \lambda[{\rm prj}_2], {\rm zero} {\sf \, ⨟ \,} {\rm succ} \rangle {\sf \, ⨟ \,} ({\rm ev} {\sf \, ⨟ \,} {\rm succ}) \\
&= \langle 1 {\sf \, ⨟ \,} \lambda[{\rm prj}_2], ({\rm zero} {\sf \, ⨟ \,} {\rm succ}) {\sf \, ⨟ \,} {\mathbb{N}} \rangle {\sf \, ⨟ \,} ({\rm ev} {\sf \, ⨟ \,} {\rm succ}) \\
&= (\langle 1, {\rm zero} {\sf \, ⨟ \,} {\rm succ} \rangle {\sf \, ⨟ \,} (\lambda[{\rm prj}_2]\times {\mathbb{N}})) {\sf \, ⨟ \,} ({\rm ev} {\sf \, ⨟ \,} {\rm succ}) \\
&= \langle 1, {\rm zero} {\sf \, ⨟ \,} {\rm succ} \rangle {\sf \, ⨟ \,} ((\lambda[{\rm prj}_2]\times {\mathbb{N}}) {\sf \, ⨟ \,} {\rm ev}) {\sf \, ⨟ \,} {\rm succ} \\
&= \langle 1, {\rm zero} {\sf \, ⨟ \,} {\rm succ} \rangle {\sf \, ⨟ \,} {\rm prj}_2 {\sf \, ⨟ \,} {\rm succ} \\
&= (\langle 1, {\rm zero} {\sf \, ⨟ \,} {\rm succ} \rangle {\sf \, ⨟ \,} {\rm prj}_2) {\sf \, ⨟ \,} {\rm succ} \\
&= ({\rm zero} {\sf \, ⨟ \,} {\rm succ}) {\sf \, ⨟ \,} {\rm succ} \\
&= {\rm zero} {\sf \, ⨟ \,} {\rm succ} {\sf \, ⨟ \,} {\rm succ} \\
&= 2_{{\mathbb{N}}} \\
\end{align}
\]
計算プロセスの解説
以下、上で紹介した「圏論的な 1+1 の計算デモ」をステップバイステップで詳細に噛み砕きながら説明していく。
曖昧さの除去
\(1+1\) という記号は、
\[
\begin{align}
1+1 &:= 1_{{\mathbb{N}}}+1_{{\mathbb{N}}} \\
1+1 &:= 1_{{\mathbb{Z}}}+1_{{\mathbb{Z}}} \\
1+1 &:= 1_{{\mathbb{Q}}}+1_{{\mathbb{Q}}} \\
1+1 &:= 1_{{\mathbb{R}}}+1_{{\mathbb{R}}} \\
\end{align}
\]
といった感じに、様々な射に対して重複して割り当てられることになるのだが、今考えているのはその中の「自然数同士の間の足し算 \(1_{{\mathbb{N}}}+1_{{\mathbb{N}}}\)」 である。
以上の話から察しがつくと思うが、最初の式変形
\[
1+1 = 1_{{\mathbb{N}}}+1_{{\mathbb{N}}} \\
\]
は、単にその「今想定している \(1+1\) が、その内のどれを指しているのか」という曖昧な部分を明確化しているだけである。
糖衣構文 m+n の de-sugar
続いて
\[
\begin{align}
& 1_{{\mathbb{N}}}+1_{{\mathbb{N}}} \\
=\:& \langle 1_{{\mathbb{N}}},1_{{\mathbb{N}}} \rangle {\sf \, ⨟ \,} (+_{{\mathbb{N}}}) \\
\end{align}
\]
という式変形だが、これは単に記号 \(1_{{\mathbb{N}}}+1_{{\mathbb{N}}}\) を de-sugar しているだけである。
より具体的には、2つの自然数 \(m:1\rightarrow {\mathbb{N}}\), \(n:1\rightarrow {\mathbb{N}}\) に対して \(m+n\) という記号は「\(\langle m,n \rangle {\sf \, ⨟ \,} (+_{{\mathbb{N}}})\)」の糖衣構文として与えている。
端的にいうと
\[
m+n := \langle m,n \rangle {\sf \, ⨟ \,} (+_{{\mathbb{N}}})
\]
ということだが、この \(m\) と \(n\) にそれぞれ \(1_{{\mathbb{N}}}\) と \(1_{{\mathbb{N}}}\) を当てはめてみてほしい。
先ほどの式が得られるはずである。
自然数を「アラビア数字の記号」を用いずに表す
\(1_{{\mathbb{N}}}\), \(2_{{\mathbb{N}}}\), \(3_{{\mathbb{N}}}\) などといった記号を自然数に割り当てているが、結局はそれらも
\[
\begin{align}
0_{{\mathbb{N}}} &= {\rm zero} \\
1_{{\mathbb{N}}} &= {\rm zero} {\sf \, ⨟ \,} {\rm succ} \\
2_{{\mathbb{N}}} &= {\rm zero} {\sf \, ⨟ \,} {\rm succ} {\sf \, ⨟ \,} {\rm succ} \\
3_{{\mathbb{N}}} &= {\rm zero} {\sf \, ⨟ \,} {\rm succ} {\sf \, ⨟ \,} {\rm succ} {\sf \, ⨟ \,} {\rm succ} \\
4_{{\mathbb{N}}} &= {\rm zero} {\sf \, ⨟ \,} {\rm succ} {\sf \, ⨟ \,} {\rm succ} {\sf \, ⨟ \,} {\rm succ} {\sf \, ⨟ \,} {\rm succ} \\
5_{{\mathbb{N}}} &= {\rm zero} {\sf \, ⨟ \,} {\rm succ} {\sf \, ⨟ \,} {\rm succ} {\sf \, ⨟ \,} {\rm succ} {\sf \, ⨟ \,} {\rm succ} {\sf \, ⨟ \,} {\rm succ} \\
\end{align}
\]
というようにして与えられる「特定の射」に割り当てている便宜的な記号に過ぎない。
以下の式変形は単に、そういった記号を、その記号が割り当てられている本体となる射で置き換えているだけである。
\[
\begin{align}
& \langle 1_{{\mathbb{N}}},1_{{\mathbb{N}}} \rangle {\sf \, ⨟ \,} (+_{{\mathbb{N}}}) \\
=\:& \langle {\rm zero} {\sf \, ⨟ \,} {\rm succ}, {\rm zero} {\sf \, ⨟ \,} {\rm succ} \rangle {\sf \, ⨟ \,} (+_{{\mathbb{N}}}) \\
\end{align}
\]
余談
\({\rm zero} {\sf \, ⨟ \,} {\rm succ}\) という形の直接的な自然数の取り扱いを行う場合、「何進数表記であるのか」という問題が付きまとわない。
例えば、自然数 \({\rm zero} {\sf \, ⨟ \,} {\rm succ} {\sf \, ⨟ \,} {\rm succ}\) は、十進数表記だと \(2\), 二進数表記だと \(10\) というように違った記号によって表記されるが、表記が異なろうがそれらは常に同一の射を参照しなければならないため、表記ではなく実体となる射の方を圏論的に直接操作することにより「\(1+1\) は \(2\) ではなく \(10\) である」といったようなある種の揚げ足取りをされる心配も必要なくなる。
足し算の定義式の展開
\[
\begin{align}
& \langle {\rm zero} {\sf \, ⨟ \,} {\rm succ}, {\rm zero} {\sf \, ⨟ \,} {\rm succ} \rangle {\sf \, ⨟ \,} (+_{{\mathbb{N}}}) \\
=\:& \langle {\rm zero} {\sf \, ⨟ \,} {\rm succ}, {\rm zero} {\sf \, ⨟ \,} {\rm succ} \rangle {\sf \, ⨟ \,} (({\rm rec}_{{\mathbb{N}}}({\rm arrToEl}({\mathbb{N}}),\lambda[{\rm ev} {\sf \, ⨟ \,} {\rm succ}])\times {\mathbb{N}}){\sf \, ⨟ \,} {\rm ev}) \\
\end{align}
\]
は、単に足し算の定義式を展開し、具体的な射の構成を数式上で直に見えるようにしているだけである。
合成射の結合性公理の適用
\[
\begin{align}
& \langle {\rm zero} {\sf \, ⨟ \,} {\rm succ}, {\rm zero} {\sf \, ⨟ \,} {\rm succ} \rangle {\sf \, ⨟ \,} (({\rm rec}_{{\mathbb{N}}}({\rm arrToEl}({\mathbb{N}}),\lambda[{\rm ev} {\sf \, ⨟ \,} {\rm succ}])\times {\mathbb{N}}){\sf \, ⨟ \,} {\rm ev}) \\
=\:& \langle {\rm zero} {\sf \, ⨟ \,} {\rm succ}, {\rm zero} {\sf \, ⨟ \,} {\rm succ} \rangle {\sf \, ⨟ \,} ({\rm rec}_{{\mathbb{N}}}({\rm arrToEl}({\mathbb{N}}),\lambda[{\rm ev} {\sf \, ⨟ \,} {\rm succ}])\times {\mathbb{N}}){\sf \, ⨟ \,} {\rm ev} \\
=\:& (\langle {\rm zero} {\sf \, ⨟ \,} {\rm succ}, {\rm zero} {\sf \, ⨟ \,} {\rm succ} \rangle {\sf \, ⨟ \,} ({\rm rec}_{{\mathbb{N}}}({\rm arrToEl}({\mathbb{N}}),\lambda[{\rm ev} {\sf \, ⨟ \,} {\rm succ}])\times {\mathbb{N}})) {\sf \, ⨟ \,} {\rm ev} \\
\end{align}
\]
は、圏の公理の1つである合成射の結合性公理を使った式変形である。
積対象の要素と射の積との合成に関する関係式の適用
- \(a:1\rightarrow A\) を \(A\) の要素
- \(b:1\rightarrow B\) を \(B\) の要素
- \(f:A\rightarrow A'\) を \(A,A'\) 間を結ぶ射
- \(g:B\rightarrow B'\) を \(B,B'\) 間を結ぶ射
としたとき、
\[
\begin{align}
\langle a,b \rangle {\sf \, ⨟ \,} (f\times g) &= \langle a,b \rangle {\sf \, ⨟ \,} \langle {\rm prj}_1 {\sf \, ⨟ \,} f, {\rm prj}_2 {\sf \, ⨟ \,} g \rangle \\
&= \langle \langle a,b \rangle {\sf \, ⨟ \,} ({\rm prj}_1 {\sf \, ⨟ \,} f), \langle a,b \rangle {\sf \, ⨟ \,} ({\rm prj}_2 {\sf \, ⨟ \,} g) \rangle \\
&= \langle (\langle a,b \rangle {\sf \, ⨟ \,} {\rm prj}_1) {\sf \, ⨟ \,} f, (\langle a,b \rangle {\sf \, ⨟ \,} {\rm prj}_2) {\sf \, ⨟ \,} g \rangle \\
&= \langle a {\sf \, ⨟ \,} f, b {\sf \, ⨟ \,} g \rangle \\
\end{align}
\]
より
\[
\langle a,b \rangle {\sf \, ⨟ \,} (f\times g) = \langle a {\sf \, ⨟ \,} f, b {\sf \, ⨟ \,} g \rangle
\]
という関係式が成立する。
このことを踏まえて以下の式変形を見れば、単にこの関係式通りにそのまま変形しているだけであることに気付ける。
\[
\begin{align}
& (\langle {\rm zero} {\sf \, ⨟ \,} {\rm succ}, {\rm zero} {\sf \, ⨟ \,} {\rm succ} \rangle {\sf \, ⨟ \,} ({\rm rec}_{{\mathbb{N}}}({\rm arrToEl}({\mathbb{N}}),\lambda[{\rm ev} {\sf \, ⨟ \,} {\rm succ}])\times {\mathbb{N}})) {\sf \, ⨟ \,} {\rm ev} \\
=\:& (\langle ({\rm zero} {\sf \, ⨟ \,} {\rm succ}) {\sf \, ⨟ \,} {\rm rec}_{{\mathbb{N}}}({\rm arrToEl}({\mathbb{N}}),\lambda[{\rm ev} {\sf \, ⨟ \,} {\rm succ}]), ({\rm zero} {\sf \, ⨟ \,} {\rm succ}) {\sf \, ⨟ \,} {\mathbb{N}} \rangle) {\sf \, ⨟ \,} {\rm ev} \\
\end{align}
\]
因みに、上の関係式を導く過程で用いている
\[
a{\sf \, ⨟ \,} \langle h,k \rangle = \langle a{\sf \, ⨟ \,} h,a{\sf \, ⨟ \,} k \rangle
\]
という関係式は、
\[
\begin{align}
(a{\sf \, ⨟ \,} \langle h,k \rangle) {\sf \, ⨟ \,} {\rm prj}_1 &= a {\sf \, ⨟ \,} h \\
(a{\sf \, ⨟ \,} \langle h,k \rangle) {\sf \, ⨟ \,} {\rm prj}_2 &= a {\sf \, ⨟ \,} k \\
\end{align}
\]
という事実と、積の普遍性からくる
\[
\begin{align}
x {\sf \, ⨟ \,} {\rm prj}_1 &= a {\sf \, ⨟ \,} h \\
x {\sf \, ⨟ \,} {\rm prj}_2 &= a {\sf \, ⨟ \,} k \\
\end{align}
\]
を満足する射 \(x\) の一意性から直ちに従う。(その一意的な射 \(x\) は既に説明の通り、\(\langle a{\sf \, ⨟ \,} h,a{\sf \, ⨟ \,} k \rangle\) と書かれる)
合成射の結合性公理 & 恒等射の公理 の適用
\[
\begin{align}
& (\langle ({\rm zero} {\sf \, ⨟ \,} {\rm succ}) {\sf \, ⨟ \,} {\rm rec}_{{\mathbb{N}}}({\rm arrToEl}({\mathbb{N}}),\lambda[{\rm ev} {\sf \, ⨟ \,} {\rm succ}]), ({\rm zero} {\sf \, ⨟ \,} {\rm succ}) {\sf \, ⨟ \,} {\mathbb{N}} \rangle) {\sf \, ⨟ \,} {\rm ev} \\
=\:& (\langle {\rm zero} {\sf \, ⨟ \,} ({\rm succ} {\sf \, ⨟ \,} {\rm rec}_{{\mathbb{N}}}({\rm arrToEl}({\mathbb{N}}),\lambda[{\rm ev} {\sf \, ⨟ \,} {\rm succ}])), {\rm zero} {\sf \, ⨟ \,} {\rm succ} \rangle) {\sf \, ⨟ \,} {\rm ev} \\
\end{align}
\]
という部分は、合成射の結合性公理により得られる関係式
\[
({\rm zero} {\sf \, ⨟ \,} {\rm succ}) {\sf \, ⨟ \,} {\rm rec}_{{\mathbb{N}}}({\rm arrToEl}({\mathbb{N}}),\lambda[{\rm ev} {\sf \, ⨟ \,} {\rm succ}]) = {\rm zero} {\sf \, ⨟ \,} ({\rm succ} {\sf \, ⨟ \,} {\rm rec}_{{\mathbb{N}}}({\rm arrToEl}({\mathbb{N}}),\lambda[{\rm ev} {\sf \, ⨟ \,} {\rm succ}]))
\]
と恒等射の公理により得られる関係式
\[
({\rm zero} {\sf \, ⨟ \,} {\rm succ}) {\sf \, ⨟ \,} {\mathbb{N}} = ({\rm zero} {\sf \, ⨟ \,} {\rm succ})
\]
を同時に適用しているだけである。
自然数対象公理に関する可換図式からくる関係式の適用
自然数対象の定義より、仲介射 \({\rm rec}_{{\mathbb{N}}}({\rm arrToEl}({\mathbb{N}}),\lambda[{\rm ev} {\sf \, ⨟ \,} {\rm succ}])\) は以下の関係式を満たす。(自然数対象の定義の中に登場する可換図式を数式で表したもの。)
\[
\begin{align}
{\rm zero} {\sf \, ⨟ \,} {\rm rec}_{{\mathbb{N}}}({\rm arrToEl}({\mathbb{N}}),\lambda[{\rm ev} {\sf \, ⨟ \,} {\rm succ}]) &= {\rm arrToEl}({\mathbb{N}}) \\
{\rm succ} {\sf \, ⨟ \,} {\rm rec}_{{\mathbb{N}}}({\rm arrToEl}({\mathbb{N}}),\lambda[{\rm ev} {\sf \, ⨟ \,} {\rm succ}]) &= {\rm rec}_{{\mathbb{N}}}({\rm arrToEl}({\mathbb{N}}),\lambda[{\rm ev} {\sf \, ⨟ \,} {\rm succ}]) {\sf \, ⨟ \,} \lambda[{\rm ev} {\sf \, ⨟ \,} {\rm succ}] \\
\end{align}
\]
この2番目の関係式を使うことで以下の式変形が実現する。
\[
\begin{align}
& (\langle {\rm zero} {\sf \, ⨟ \,} ({\rm succ} {\sf \, ⨟ \,} {\rm rec}_{{\mathbb{N}}}({\rm arrToEl}({\mathbb{N}}),\lambda[{\rm ev} {\sf \, ⨟ \,} {\rm succ}])), {\rm zero} {\sf \, ⨟ \,} {\rm succ} \rangle) {\sf \, ⨟ \,} {\rm ev} \\
=\:& (\langle {\rm zero} {\sf \, ⨟ \,} ({\rm rec}_{{\mathbb{N}}}({\rm arrToEl}({\mathbb{N}}),\lambda[{\rm ev} {\sf \, ⨟ \,} {\rm succ}]) {\sf \, ⨟ \,} \lambda[{\rm ev} {\sf \, ⨟ \,} {\rm succ}]), {\rm zero} {\sf \, ⨟ \,} {\rm succ} \rangle) {\sf \, ⨟ \,} {\rm ev} \\
\end{align}
\]
合成射の結合性公理 & 恒等射の公理 の適用
再度、合成射の結合性公理と恒等射の公理を用いると以下の式変形ができる。
\[
\begin{align}
& (\langle {\rm zero} {\sf \, ⨟ \,} ({\rm rec}_{{\mathbb{N}}}({\rm arrToEl}({\mathbb{N}}),\lambda[{\rm ev} {\sf \, ⨟ \,} {\rm succ}]) {\sf \, ⨟ \,} \lambda[{\rm ev} {\sf \, ⨟ \,} {\rm succ}]), {\rm zero} {\sf \, ⨟ \,} {\rm succ} \rangle) {\sf \, ⨟ \,} {\rm ev} \\
=\:& (\langle ({\rm zero} {\sf \, ⨟ \,} {\rm rec}_{{\mathbb{N}}}({\rm arrToEl}({\mathbb{N}}),\lambda[{\rm ev} {\sf \, ⨟ \,} {\rm succ}])) {\sf \, ⨟ \,} \lambda[{\rm ev} {\sf \, ⨟ \,} {\rm succ}], {\rm zero} {\sf \, ⨟ \,} {\rm succ} \rangle) {\sf \, ⨟ \,} {\rm ev} \\
=\:& (\langle ({\rm zero} {\sf \, ⨟ \,} {\rm rec}_{{\mathbb{N}}}({\rm arrToEl}({\mathbb{N}}),\lambda[{\rm ev} {\sf \, ⨟ \,} {\rm succ}])) {\sf \, ⨟ \,} \lambda[{\rm ev} {\sf \, ⨟ \,} {\rm succ}], ({\rm zero} {\sf \, ⨟ \,} {\rm succ}) {\sf \, ⨟ \,} {\mathbb{N}} \rangle) {\sf \, ⨟ \,} {\rm ev} \\
\end{align}
\]
積対象の要素と射の積との合成に関する関係式の適用
先ほど示した
\[
\langle a,b \rangle {\sf \, ⨟ \,} (f\times g) = \langle a {\sf \, ⨟ \,} f, b {\sf \, ⨟ \,} g \rangle
\]
という関係式を使うと以下の式変形が得られる。
\[
\begin{align}
& (\langle ({\rm zero} {\sf \, ⨟ \,} {\rm rec}_{{\mathbb{N}}}({\rm arrToEl}({\mathbb{N}}),\lambda[{\rm ev} {\sf \, ⨟ \,} {\rm succ}])) {\sf \, ⨟ \,} \lambda[{\rm ev} {\sf \, ⨟ \,} {\rm succ}], ({\rm zero} {\sf \, ⨟ \,} {\rm succ}) {\sf \, ⨟ \,} {\mathbb{N}} \rangle) {\sf \, ⨟ \,} {\rm ev} \\
=\:& (\langle {\rm zero} {\sf \, ⨟ \,} {\rm rec}_{{\mathbb{N}}}({\rm arrToEl}({\mathbb{N}}),\lambda[{\rm ev} {\sf \, ⨟ \,} {\rm succ}]), {\rm zero} {\sf \, ⨟ \,} {\rm succ} \rangle {\sf \, ⨟ \,} (\lambda[{\rm ev} {\sf \, ⨟ \,} {\rm succ}]\times {\mathbb{N}})) {\sf \, ⨟ \,} {\rm ev} \\
\end{align}
\]
合成射の結合性公理の適用
再度、合成射の結合性公理を用いると以下の式変形ができる。
\[
\begin{align}
& (\langle {\rm zero} {\sf \, ⨟ \,} {\rm rec}_{{\mathbb{N}}}({\rm arrToEl}({\mathbb{N}}),\lambda[{\rm ev} {\sf \, ⨟ \,} {\rm succ}]), {\rm zero} {\sf \, ⨟ \,} {\rm succ} \rangle {\sf \, ⨟ \,} (\lambda[{\rm ev} {\sf \, ⨟ \,} {\rm succ}]\times {\mathbb{N}})) {\sf \, ⨟ \,} {\rm ev} \\
=\:& \langle {\rm zero} {\sf \, ⨟ \,} {\rm rec}_{{\mathbb{N}}}({\rm arrToEl}({\mathbb{N}}),\lambda[{\rm ev} {\sf \, ⨟ \,} {\rm succ}]), {\rm zero} {\sf \, ⨟ \,} {\rm succ} \rangle {\sf \, ⨟ \,} ((\lambda[{\rm ev} {\sf \, ⨟ \,} {\rm succ}]\times {\mathbb{N}}) {\sf \, ⨟ \,} {\rm ev}) \\
\end{align}
\]
指数対象公理に関する可換図式からくる関係式の適用
指数対象の定義より、仲介射 \(\lambda[{\rm ev} {\sf \, ⨟ \,} {\rm succ}]\) は以下の関係式を満たす。
\[
(\lambda[{\rm ev} {\sf \, ⨟ \,} {\rm succ}]\times {\mathbb{N}}){\sf \, ⨟ \,} {\rm ev} = ({\rm ev} {\sf \, ⨟ \,} {\rm succ}) \\
\]
この関係式を使うことで以下の式変形が実現する。
\[
\begin{align}
& \langle {\rm zero} {\sf \, ⨟ \,} {\rm rec}_{{\mathbb{N}}}({\rm arrToEl}({\mathbb{N}}),\lambda[{\rm ev} {\sf \, ⨟ \,} {\rm succ}]), {\rm zero} {\sf \, ⨟ \,} {\rm succ} \rangle {\sf \, ⨟ \,} ((\lambda[{\rm ev} {\sf \, ⨟ \,} {\rm succ}]\times {\mathbb{N}}) {\sf \, ⨟ \,} {\rm ev}) \\
=\:& \langle {\rm zero} {\sf \, ⨟ \,} {\rm rec}_{{\mathbb{N}}}({\rm arrToEl}({\mathbb{N}}),\lambda[{\rm ev} {\sf \, ⨟ \,} {\rm succ}]), {\rm zero} {\sf \, ⨟ \,} {\rm succ} \rangle {\sf \, ⨟ \,} ({\rm ev} {\sf \, ⨟ \,} {\rm succ}) \\
\end{align}
\]
自然数対象公理に関する可換図式からくる関係式の適用
先ほど説明した通り、仲介射 \({\rm rec}_{{\mathbb{N}}}({\rm arrToEl}({\mathbb{N}}),\lambda[{\rm ev} {\sf \, ⨟ \,} {\rm succ}])\) について、以下の関係式が成立する。
\[
\begin{align}
{\rm zero} {\sf \, ⨟ \,} {\rm rec}_{{\mathbb{N}}}({\rm arrToEl}({\mathbb{N}}),\lambda[{\rm ev} {\sf \, ⨟ \,} {\rm succ}]) &= {\rm arrToEl}({\mathbb{N}}) \\
{\rm succ} {\sf \, ⨟ \,} {\rm rec}_{{\mathbb{N}}}({\rm arrToEl}({\mathbb{N}}),\lambda[{\rm ev} {\sf \, ⨟ \,} {\rm succ}]) &= {\rm rec}_{{\mathbb{N}}}({\rm arrToEl}({\mathbb{N}}),\lambda[{\rm ev} {\sf \, ⨟ \,} {\rm succ}]) {\sf \, ⨟ \,} \lambda[{\rm ev} {\sf \, ⨟ \,} {\rm succ}] \\
\end{align}
\]
ここで、この1番目の関係式を使うと以下の式変形が実現する。
\[
\begin{align}
& \langle {\rm zero} {\sf \, ⨟ \,} {\rm rec}_{{\mathbb{N}}}({\rm arrToEl}({\mathbb{N}}),\lambda[{\rm ev} {\sf \, ⨟ \,} {\rm succ}]), {\rm zero} {\sf \, ⨟ \,} {\rm succ} \rangle {\sf \, ⨟ \,} ({\rm ev} {\sf \, ⨟ \,} {\rm succ}) \\
=\:& \langle {\rm arrToEl}({\mathbb{N}}), {\rm zero} {\sf \, ⨟ \,} {\rm succ} \rangle {\sf \, ⨟ \,} ({\rm ev} {\sf \, ⨟ \,} {\rm succ}) \\
\end{align}
\]
糖衣構文 arrToEl(f) の de-sugar
糖衣構文 \({\rm arrToEl}(f)\) は
\[
{\rm arrToEl}(f) := \lambda[{\rm prj}_2{\sf \, ⨟ \,} f]
\]
として与えているので、この通りに \({\rm arrToEl}({\mathbb{N}})\) を de-sugar することで以下の式変形が行える。
\[
\begin{align}
& \langle {\rm arrToEl}({\mathbb{N}}), {\rm zero} {\sf \, ⨟ \,} {\rm succ} \rangle {\sf \, ⨟ \,} ({\rm ev} {\sf \, ⨟ \,} {\rm succ}) \\
=\:& \langle \lambda[{\rm prj}_2 {\sf \, ⨟ \,} {\mathbb{N}}], {\rm zero} {\sf \, ⨟ \,} {\rm succ} \rangle {\sf \, ⨟ \,} ({\rm ev} {\sf \, ⨟ \,} {\rm succ}) \\
\end{align}
\]
恒等射の公理の適用
恒等射の公理を適用すると以下の式変形ができる。
\[
\begin{align}
& \langle \lambda[{\rm prj}_2 {\sf \, ⨟ \,} {\mathbb{N}}], {\rm zero} {\sf \, ⨟ \,} {\rm succ} \rangle {\sf \, ⨟ \,} ({\rm ev} {\sf \, ⨟ \,} {\rm succ}) \\
=\:& \langle \lambda[{\rm prj}_2], {\rm zero} {\sf \, ⨟ \,} {\rm succ} \rangle {\sf \, ⨟ \,} ({\rm ev} {\sf \, ⨟ \,} {\rm succ}) \\
=\:& \langle 1 {\sf \, ⨟ \,} \lambda[{\rm prj}_2], ({\rm zero} {\sf \, ⨟ \,} {\rm succ}) {\sf \, ⨟ \,} {\mathbb{N}} \rangle {\sf \, ⨟ \,} ({\rm ev} {\sf \, ⨟ \,} {\rm succ}) \\
\end{align}
\]
(一応補足しておくと、3行目の頭に登場している \(1\) は「終対象 \(1:1\rightarrow 1\)」、つまりは「恒等射」である。)
積対象の要素と射の積との合成に関する関係式の適用
再び
\[
\langle a,b \rangle {\sf \, ⨟ \,} (f\times g) = \langle a {\sf \, ⨟ \,} f, b {\sf \, ⨟ \,} g \rangle
\]
という関係式を使うと以下の式変形が得られる。
\[
\begin{align}
=\:& \langle 1 {\sf \, ⨟ \,} \lambda[{\rm prj}_2], ({\rm zero} {\sf \, ⨟ \,} {\rm succ}) {\sf \, ⨟ \,} {\mathbb{N}} \rangle {\sf \, ⨟ \,} ({\rm ev} {\sf \, ⨟ \,} {\rm succ}) \\
=\:& (\langle 1, {\rm zero} {\sf \, ⨟ \,} {\rm succ} \rangle {\sf \, ⨟ \,} (\lambda[{\rm prj}_2]\times {\mathbb{N}})) {\sf \, ⨟ \,} ({\rm ev} {\sf \, ⨟ \,} {\rm succ}) \\
\end{align}
\]
合成射の結合性公理の適用
再度、合成射の結合性公理を用いると以下の式変形ができる。
\[
\begin{align}
& (\langle 1, {\rm zero} {\sf \, ⨟ \,} {\rm succ} \rangle {\sf \, ⨟ \,} (\lambda[{\rm prj}_2]\times {\mathbb{N}})) {\sf \, ⨟ \,} ({\rm ev} {\sf \, ⨟ \,} {\rm succ}) \\
=\:& \langle 1, {\rm zero} {\sf \, ⨟ \,} {\rm succ} \rangle {\sf \, ⨟ \,} ((\lambda[{\rm prj}_2]\times {\mathbb{N}}) {\sf \, ⨟ \,} {\rm ev}) {\sf \, ⨟ \,} {\rm succ} \\
\end{align}
\]
指数対象公理に関する可換図式からくる関係式の適用
指数対象の定義より、仲介射 \(\lambda[{\rm prj}_2]\) は以下の関係式を満たす。
\[
(\lambda[{\rm prj}_2]\times {\mathbb{N}}){\sf \, ⨟ \,} {\rm ev} = {\rm prj}_2 \\
\]
この関係式を使うことで以下の式変形が実現する。
\[
\begin{align}
& \langle 1, {\rm zero} {\sf \, ⨟ \,} {\rm succ} \rangle {\sf \, ⨟ \,} ((\lambda[{\rm prj}_2]\times {\mathbb{N}}) {\sf \, ⨟ \,} {\rm ev}) {\sf \, ⨟ \,} {\rm succ} \\
=\:& \langle 1, {\rm zero} {\sf \, ⨟ \,} {\rm succ} \rangle {\sf \, ⨟ \,} {\rm prj}_2 {\sf \, ⨟ \,} {\rm succ} \\
\end{align}
\]
合成射の結合性公理の適用
再度、合成射の結合性公理を用いると以下の式変形ができる。
\[
\begin{align}
& \langle 1, {\rm zero} {\sf \, ⨟ \,} {\rm succ} \rangle {\sf \, ⨟ \,} {\rm prj}_2 {\sf \, ⨟ \,} {\rm succ} \\
=\:& (\langle 1, {\rm zero} {\sf \, ⨟ \,} {\rm succ} \rangle {\sf \, ⨟ \,} {\rm prj}_2) {\sf \, ⨟ \,} {\rm succ} \\
\end{align}
\]
積対象公理に関する可換図式からくる関係式の適用
積対象の定義より、仲介射 \(\langle 1, {\rm zero} {\sf \, ⨟ \,} {\rm succ} \rangle\) は以下の関係式を満たす。
\[
\begin{align}
\langle 1, {\rm zero} {\sf \, ⨟ \,} {\rm succ} \rangle {\sf \, ⨟ \,} {\rm prj}_1 &= 1 \\
\langle 1, {\rm zero} {\sf \, ⨟ \,} {\rm succ} \rangle {\sf \, ⨟ \,} {\rm prj}_2 &= {\rm zero} {\sf \, ⨟ \,} {\rm succ} \\
\end{align}
\]
この2番目の関係式を使うことで以下のように式変形がされる。
\[
\begin{align}
& (\langle 1, {\rm zero} {\sf \, ⨟ \,} {\rm succ} \rangle {\sf \, ⨟ \,} {\rm prj}_2) {\sf \, ⨟ \,} {\rm succ} \\
=\:& ({\rm zero} {\sf \, ⨟ \,} {\rm succ}) {\sf \, ⨟ \,} {\rm succ} \\
\end{align}
\]
合成射の結合性公理の適用
再度、合成射の結合性公理を用いると以下の式変形ができる。
\[
\begin{align}
& ({\rm zero} {\sf \, ⨟ \,} {\rm succ}) {\sf \, ⨟ \,} {\rm succ} \\
=\:& {\rm zero} {\sf \, ⨟ \,} {\rm succ} {\sf \, ⨟ \,} {\rm succ} \\
\end{align}
\]
自然数を「アラビア数字の記号」を用いて表し直す
始まりの方で話した
\[
\begin{align}
0_{{\mathbb{N}}} &= {\rm zero} \\
1_{{\mathbb{N}}} &= {\rm zero} {\sf \, ⨟ \,} {\rm succ} \\
2_{{\mathbb{N}}} &= {\rm zero} {\sf \, ⨟ \,} {\rm succ} {\sf \, ⨟ \,} {\rm succ} \\
3_{{\mathbb{N}}} &= {\rm zero} {\sf \, ⨟ \,} {\rm succ} {\sf \, ⨟ \,} {\rm succ} {\sf \, ⨟ \,} {\rm succ} \\
4_{{\mathbb{N}}} &= {\rm zero} {\sf \, ⨟ \,} {\rm succ} {\sf \, ⨟ \,} {\rm succ} {\sf \, ⨟ \,} {\rm succ} {\sf \, ⨟ \,} {\rm succ} \\
5_{{\mathbb{N}}} &= {\rm zero} {\sf \, ⨟ \,} {\rm succ} {\sf \, ⨟ \,} {\rm succ} {\sf \, ⨟ \,} {\rm succ} {\sf \, ⨟ \,} {\rm succ} {\sf \, ⨟ \,} {\rm succ} \\
\end{align}
\]
という記号の割り当てを適用すると以下が得られる。
\[
\begin{align}
& {\rm zero} {\sf \, ⨟ \,} {\rm succ} {\sf \, ⨟ \,} {\rm succ} \\
=\:& 2_{{\mathbb{N}}} \\
\end{align}
\]
後書き
圏論的に自然数を取り扱う場合、このように表記とは独立に足し算を1つの形ある具体的な矢印として構成することが可能となる。("表記とは独立に" が仄めかしているのは、「変数」という表記の上では形ある図形 (記号) として認識できるが、純粋圏論的な実体を持たない何かが、足し算の定義の中でしっかりと使用されていないという点である。)
さらに以上の議論を追いかけてきたのであればわかると思うが、そのように構成される射は絵に描いた餅ではなく、普遍性や圏の公理を駆使することで、具体的な数の計算へと繋げていくことも事実可能である。
(型理論において、自然数の足し算はしばしば自己参照を伴う変数を用いた形式的な表記上の記号操作のルールを与えることによって定義されるわけだが、圏論はそういった一見形骸的に見える表記上の記号操作に対する数学的な上手い意味付けをしばしば提供する。)
また、式変形の流れから「射の合成に課される結合性」が如何に重要な公理であるのかを読み取ることもできるだろう。
従来の自己参照を伴う再帰的な特徴付けとの具体的な対比
物質的集合論の教科書の中には、
\[
\begin{align}
0 &:= \varnothing \\
S(n) &:= n \cup \{n\} \\
\end{align}
\]
とした上で、自然数の足し算を以下の関係式によって再帰的に特徴付けられる記号 \(+\) として導入するものがある。
\[
\begin{align}
m + 0 &= m \\
m + S(n) &= S(m+n) \\
\end{align}
\]
実際、これをベースに考えれば、\(1+1\) という表記は、以下のような記号操作を経て直ちに \(2\) へと持っていかれる。
\[
\begin{align}
1 + 1 &= 1 + S(0) \\
&= S(1 + 0) \\
&= S(1) \\
&= 2 \\
\end{align}
\]
この事実だけみると、「こんなにも簡潔に説明できてしまうことを、どうしてわざわざややこしく考える必要があるのか」と疑問に思うかもしれない。
ポイントとなるのは、上の関係式は「写像 \((+)\) の満たす性質の1つ (帰結)」であって、「それ自体が写像 \((+)\) の構成方法を与えているというわけではない」ということである。
よりわかりやすく言い換えると、ETCS や ZFC といった公理的集合論の枠組みの上で「その再帰的な関係式を満足する写像の存在」を証明することはできるが、当然であるが「その関係式それ自体が、その写像の存在を示す証明になっている」というわけではなく、別途証明が必要になる。
ここでは敢えて「その関係式を満たす写像の存在を証明してから、自然数間の加法を定義する」という手順を踏まずに、「(その関係式が満たされることをまだ証明していない状況下で) 具体的に構成された射 \((+)\) を与え、そこに順序対 \(\langle 1,1 \rangle\) を合成したものが \(2\) になることを、圏の公理や普遍性だけを駆使して導く」という手順を踏んでいるので、このように煩雑な式変形になっている。
タグ一覧: