文献あり

順像と存在量化∃

129

概要

本稿では、射の順像と論理式の存在量化の関係について解説する。
有限積の射影で順像を取ることが、射影の前後で消える対象に対応する自由変数で存在量化を取ることと対応する。
存在量化が積の射影の順像で表示できることは、圏論的な二項関係の合成の定義につながる。

1 図形の射影と順像

立体図形$V$と平面$S$が与えられたとする。このとき、$S$と垂直な方向から$V$全体に光を照射して、$V$の影が$S$に落ちたとする。$V$の落とした影が$S$上に作る平面図形を、$V$の$S$に対する射影と呼ぶことにする。
スクリーンに落ちる影

座標空間で考える。座標空間中の図形は時として論理式による内包表記によって表示される。例えば、原点を中心とした半径$1$の球およびその内部$V$は、次のように表示される。

$$ V \overset{\mathrm{def}}{=} \{ (x,y,z) \in \mathbb R^3 \mid x^2 + y^2 + z^2 \leq 1 \} $$

$x,y,z$座標軸のうちふたつを選ぶと、それらは平面を張る。ここでは$xz$平面に対する$V$の射影を考えてみる。
球とその射影

$xz$平面に対して垂直な方向から、$V$全体に光を照射したとき、$V$の各点$(x,y,z)$の影は$xz$平面上の点$(x,0,z)$に写る。これは写像$\theta \colon \mathbb R^3 \to \mathbb R^3,\ (x,y,z) \mapsto (x,0,z)$を作用させることと同じである。$V$の射影を、$xz$平面上で捉え直そう。全単射$\mathbb R \times \{0\} \times \mathbb R \leftrightarrow \mathbb R \times \mathbb R,\ (x,0,z) \leftrightarrow (x,z)$に基づいて、射影の図形を$\mathbb R^2$の部分集合として扱う。この同一視の下で、射影を表す写像は$\mathbb R^3 \to \mathbb R^2,\ (x,y,z) \mapsto (x,z)$になるが、これは直積の射影$\langle \pi_x,\pi_z \rangle$に他ならない。図形$V$の$xz$平面への射影は、$\langle \pi_x,\pi_z \rangle$による順像で与えられる。順像の様子を像分解の図式で表したものは以下の通り。
積の射影の順像

$$ S \overset{\mathrm{def}}{=} \{ (x,z) \in \mathbb R^2 \mid \exists (a,b,c) \in V\ .\ (x,z) = \langle \pi_x,\pi_z \rangle(a,b,c) \} $$

このように、立体$V$の$xz$平面への射影は、$xz$平面への積の射影に関する順像として表示される。

2 図形の射影と存在量化

2.1 論理式の存在量化

一階述語論理では、論理式$\varphi$が与えられたとき、新たな論理式$\exists x . \varphi$を作り出すことができる。$\exists x . \varphi$を、変数$x$に関する$\varphi$の存在量化という。$\varphi$が自由変数$x$を有しているとき、$\exists x . \varphi$中の変数$x$は束縛変数となり、もはや自由変数ではなくなる。

2.2 図形を表す論理式の存在量化

ここでまた、座標空間中の立体図形の射影について考える。前節では、原点を中心とする半径$1$の球及びその内部を例として考えた。

$$ V = \{ (x,y,z) \in \mathbb R^3 \mid x^2 + y^2 + z^2 \leq 1 \} $$

この図形$V \subseteq \mathbb R^3$は、$\varphi \overset{\mathrm{def}}{\equiv} (x,y,z) \in \mathbb R^3 \land x^2 + y^2 + z^2 \leq 1$という論理式によって表示される$\mathbb R^3$の部分集合である。

さて、図形$V$を表示する論理式$\varphi$に対して存在量化、例えば変数$y$に関する存在量化を施したとき、$\exists y . \varphi$は一体どんな部分集合を表示するだろうか？

$$ \exists y . \varphi \equiv \exists y . (x,y,z) \in \mathbb R^3 \land x^2 + y^2 + z^2 \leq 1 $$

$y$は束縛変数となり、自由変数は$x,z$のみである。そこで$x,z$がそれぞれ$\mathbb R$上を走り回る場合、次の集合が得られる。

$$ S' \overset{\mathrm{def}}{=} \{ (x,z) \in \mathbb R^2 \mid \exists y \in \mathbb R . (x,y,z) \in \mathbb R^3 \land x^2 + y^2 + z^2 \leq 1 \} $$

2.3 射影写像の順像と、図形を表す論理式の存在量化

さて、前節で、$xyz$座標空間中の立体図形$V$を$xz$平面に射影して得られる平面図形$S$は、積の射影写像$\langle \pi_x,\pi_z \rangle\colon \mathbb R^3 \to \mathbb R^2$の順像と同一視できることを確認した。$V$が原点を中心とした半径$1$の球及びその内部の場合、$S$は次のようになる。

$$ S = \{(x,z) \in \mathbb R^2 \mid \exists (a,b,c) \in V\ .\ (x,z) = \langle \pi_x , \pi_z \rangle(a,b,c) \} $$

内包表記によって$S$を表示する論理式に注目してみよう。これは次のように式変形できる。

$$ \begin{aligned} \exists (a,b,c) \in V\ .\ (x,z) = \langle \pi_x, \pi_z \rangle(a,b,c) &\equiv \exists (a,b,c) \in V\ .\ (x,z) = (a,c)\\ &\equiv \exists a,b,c \in \mathbb R\ .\ (x = a) \land (z = c)\land a^2 + b^2 + c^2 \leq 1\\ &\equiv \exists b \in \mathbb R\ .\ x\in \mathbb R \land z \in \mathbb R \land x^2 + b^2 + z^2 \leq 1\\ &\equiv \exists y\ .\ y \in \mathbb R \land x\in \mathbb R \land z \in \mathbb R \land x^2 + b^2 + z^2 \leq 1\\ &\equiv \exists y\ .\ (x,y,z) \in \mathbb R^3 \land x^2 + y^2 + z^2 \leq 1 \end{aligned} $$

つまり、$S = \{(x,z) \in \mathbb R^2 \mid \exists y\ .\ (x,y,z)\in \mathbb R^3 \land x^2+y^2+z^2 \leq 1\}$であるから、$S = S'$が従う。射影写像$\langle \pi_x,\pi_z \rangle$による$V$の順像は、$V$を表示する論理式$\varphi$の存在量化$\exists y . \varphi$によって表示されるということである。

3 順像と存在量化

ここまでの2つの節で、座標空間中の立体に対して、積の射影の順像と、内包表記の論理式の存在量化とが、同一の平面図形を表示することを見た。この関係が偶然の一致ではないことを確かめていこう。

集合の有限族$A_1,A_2,\cdots,A_n$が与えられたとする。部分集合$R \subseteq \prod_{i=1}^n A_i$を取る。$(a_i)_{i=1}^n \in R$を、$Ra_1a_2\cdots a_n$と書くことにする。$k \in \mathbb N$を取り、$1 \leq k \leq n$を満たすとする。また有限集合$J$を、$J = \{ 1,2,\cdots,n\}\setminus \{k\}$で定義する。このとき、射影写像$\langle \pi_j \rangle_{j \in J}\colon \prod_{i=1}^n A_i \to \prod_{j \in J} A_j$に関する$R$の順像は、集合$\{ (a_j)_{j \in J} \in \prod_{j \in J}A_j \mid \exists a_k \in A_k\ .\ Ra_1a_2\cdots a_n \} \subseteq \prod_{j \in J}A_j$と一致する。

$\langle \pi_j \rangle_{j \in J}$による$R$の順像は、$\{ (b_j)_{j \in J} \in \prod_{j\in J}A_j \mid \exists (a_i)_{i=1}^n \in R\ .\ (b_j)_{j\in J} = \langle \pi_j \rangle_{j \in J}(a_i)_{i=1}^n \}$である。これを表示する論理式は、次のように式変形できる。

$$ \begin{aligned} &\exists (a_i)_{i=1}^n \in R\ .\ (b_j)_{j \in J} = \langle \pi_j \rangle_{j \in J}(a_i)_{i=1}^n\\ &\equiv \exists a_1 \in A_1\ .\ \exists a_2 \in A_2\ .\ \cdots\ . \exists a_n \in A_n\ .\ Ra_1a_2\dots a_n \land \bigwedge_{j \in J} (b_j = a_j)\\ &\equiv \exists a_k \in A_k\ .\ Rb_1b_2\cdots b_{k-1}a_kb_{k+1}\cdots b_n\\ &\equiv \exists b_k \in A_k\ .\ Rb_1b_2\cdots b_n \end{aligned} $$

よって主張成立。

よって、積の射影で順像を取ることは、射影の前後で消滅する集合の上を走る自由変数で存在量化を取ることと対応する、と言える。一般に、圏論では対象の元を取ることは必ずしも出来ないが、しかし有限積と像を持つ圏ならば、積の射影で順像を取ることはできる。よって、これを以て圏論的な存在量化の表示と定義してしまえるのである。
積の射影による順像が存在量化

3.1 射の像と存在量化

※射のグラフや、coverと像の関係に関しては、こちらを参照してもらいたい。

射のグラフに関する記事

coverと像の関係に関する記事

有限積と像を持つ圏では、任意の射の像を存在量化として表示できる。任意の圏の任意の射$f \colon A \to B$に対し、$f$のグラフという$A,B$上の標準的な二項関係が定義され、標準的な2-table$(A;1_A,f)$を代表元として持つのであった。すると有限積と像を持つ圏では、$f \colon A \to B$に基づいて次の図式が成立する。
射の像とは射のグラフの存在量化

ただし$(\exists \pi_B A;m)$は、$\pi_B$による$(A;\langle 1_A,f \rangle)$の順像の表示である。$f = m \circ \overline{\pi_B \circ \langle 1_A,f \rangle}$が成り立ち、右辺はcoverとmonicの分解であるから、$[(\exists \pi_B A;m)]$は$f$の像である。このように、像と有限積を持つ圏では、任意の射の像を射のグラフに基づいて存在量化で表示できる。このことは、写像の像がグラフの第一成分に関する存在量化で定義されることの一般化と言える。写像$f \colon A \to B$のグラフを$G_f$と書くとき、$(a,b) \in G_f$は$b = f(a)$と同値であるから、

$$ fA = \{ b \in B \mid \exists a \in A\ .\ b = f(a) \} = \{ b \in B \mid \exists a . G_fab \} $$

ただし$G_fab$は$(a,b) \in G_f$の別表記。

このことから、射$f \colon A \to B$の像を$\exists f A$と書く流儀も存在する。

4 圏論的二項関係の合成

集合論的な二項関係には、次のような合成の定義がある。

二項関係の合成

集合$A,B,C$が与えられ、部分集合$R \subseteq A \times B,S \subseteq B \times C$が与えられたとする。$R,S$を二項関係のグラフと見做したとき、二項関係の合成のグラフが次で定義される。

$$ S \circ R \overset{\mathrm{def}}{=} \{ (a,c) \in A \times C \mid \exists b \in B\ . Rab \land Sbc \} $$

ただし$Rab,Sbc$はそれぞれ$(a,b) \in R,(b,c) \in S$の別表記。

集合論的な二項関係の合成の定義は、集合の元に関する論理式で表示されている。圏論では必ずしも対象の元を取れるとは限らないから、この定義をそっくりそのまま拝借するわけにはいかない。どうすれば圏論的な二項関係の合成を定義できるだろうか？その手がかりは、ここまでに既に見てきている。

directimage-existenceより、$S \circ R$は三項関係$T \overset{\mathrm{def}}{=} \{ (a,b,c) \in A \times B \times C \mid Rab \land Sbc \}$を射影写像$\langle \pi_A,\pi_C \rangle$によって順像を取ったものと一致する。そこで圏論でも、二項関係のグラフを表す2-table$R,S$から、三項関係のグラフ$T$に相当する3-tableを何とかして構成できれば、あとは積の射影$\langle \pi_A,\pi_C \rangle$で順像を取ることで、合成された二項関係を表示できるのである。この内容は次回の記事で扱う。