量化子の随伴
概要
量化子の随伴（quantifiers as adjoints）とは、部分対象の引き戻し $f^*$ の左随伴と右随伴として、存在量化 $\exists_f$ と全称量化 $\forall_f$ を表すことである。集合では写像のファイバーにおける存在・全称条件になり、前層ではすべての制限先も量化条件に含まれる。
定義
述語 $S(z)$ を集合 $Z$ の部分集合とみなし、写像 $f\colon Z\to Y$ によって変数を $Y$ 側へ移す。$Y$ の部分集合を $Z$ へ引き戻す操作 $f^*$ に対し、「ある $z$ が満たす」と「すべての $z$ が満たす」を返す操作はそれぞれ左随伴と右随伴になる。これが 量化子の随伴 という見方である。MM92 I §9。
引き戻しをもつ圏 $\mathcal E$ の射 $f\colon Z\to Y$ を考える。対象 $Y$ について $\operatorname{Sub}(Y)$ は、$Y$ への単射（モノ射）の同型類を、$m\le m'$ を「$m$ が $m'$ を経由して分解する」で並べた順序集合である。単射の引き戻しは単射なので、部分対象の引き戻し
$$
f^*\colon\operatorname{Sub}(Y)\longrightarrow\operatorname{Sub}(Z)
$$
が定まる。これに左随伴 $\exists_f$ と右随伴 $\forall_f$ があるとは、任意の $S\in\operatorname{Sub}(Z)$、$T\in\operatorname{Sub}(Y)$ について
$$
\exists_f S\leq T\quad\Longleftrightarrow\quad S\leq f^*T,
\qquad
f^*T\leq S\quad\Longleftrightarrow\quad T\leq\forall_f S
$$
が成り立つことをいう。順序は部分対象の包含を表す。したがって $\exists_f\dashv f^*\dashv\forall_f$ であり、両量化子は存在すれば一意である。MM92 I §9。
述語 $S(x,y)$ に対して射 $p\colon X\times Y\to Y$ を投影とすれば、$\exists_p S$ は「ある $x$ に対して $S(x,y)$」、$\forall_p S$ は「すべての $x$ に対して $S(x,y)$」を表す。一般の $f$ では、量化する範囲は各 $y$ のファイバー $f^{-1}(y)$ になる。
直感
$f^*$ は述語を変数変換で読み替える。$\exists_f$ は $f^*$ で読み替えると $S$ を含むような、最小の $Y$ 側の述語、$\forall_f$ は読み替えると元の述語の内側に収まる最大の $Y$ 側の述語である。この大小関係が随伴式になり、集合の要素を直接使えない圏でも量化の意味を指定できる。
例と反例
$\mathbf{Set}$ で $f\colon Z\to Y$ と $S\subset Z$ に対し
$$
\exists_f S=\{y\in Y\mid \text{ある }z\in f^{-1}(y)\text{ が }S\text{ に属する}\}=f(S),
$$
$$
\forall_f S=\{y\in Y\mid f^{-1}(y)\subset S\}
$$
と定める。$f^{-1}(y)=\emptyset$ なら、$y$ は $\exists_f S$ に入らず、$\forall_f S$ には入る。空の範囲に対する存在文は偽、全称文は真という通常の規則と一致する。MM92 I §9。
$X=\{0,1\}$、$Y=\{a,b\}$、$S=\{(0,a),(1,a),(0,b)\}\subset X\times Y$ とする。投影 $p\colon X\times Y\to Y$ について $\exists_p S=\{a,b\}$ だが $\forall_p S=\{a\}$ である。$a$ のファイバーは両方とも $S$ に入り、$b$ のファイバーは片方だけ入るためである。
上の投影では $p(S)=\{a,b\}$ は存在量化を与えるが、全称量化は $\{a\}$ である。したがって「像をとれば全称量化にもなる」は誤りである。随伴の向きも異なり、像は $p^*$ の左随伴、全称量化は右随伴である。
性質
集合の圏での随伴
任意の写像 $f\colon Z\to Y$ に対し、上の $\exists_f$ と $\forall_f$ は $f^*T=f^{-1}(T)$ の左随伴と右随伴である。MM92 I §9 Theorem 2（p. 58）。
左随伴の同値は、$\exists_fS=f(S)$ として 像(写像) の命題「像と逆像の随伴関係」を適用したものである。次に $f^{-1}(T)\subset S$ は、$y\in T$ のすべての逆像 $z\in f^{-1}(y)$ が $S$ に入るという条件と同値であり、$T\subset\forall_f S$ と同値である。空ファイバーもこの同値に含まれる。$\square$
引き戻しと量化子の交換
集合の引き戻し正方形
$$
\begin{array}{ccc}
Z'&\xrightarrow{g'}&Z\\
\big\downarrow f'&&\big\downarrow f\\
Y'&\xrightarrow{g}&Y
\end{array}
$$
において、$S\subset Z$ に対し
$$
g^*(\exists_f S)=\exists_{f'}((g')^*S),\qquad
g^*(\forall_f S)=\forall_{f'}((g')^*S)
$$
である。これは量化する変数とは別の変数を代入しても結果が一致することを表す。MM92 IV §9 Proposition 1（p. 205）と右随伴に関する式 (13)（p. 209）。初等トポス一般で成り立ち、$\mathbf{Set}$ はその特別な場合である。
$Z'$ を $\{(z,y')\mid f(z)=g(y')\}$ と表す。$y'\in Y'$ が左辺の存在量化に入る条件は、$f(z)=g(y')$ かつ $z\in S$ である $z$ が存在すること。右辺では $(z,y')\in Z'$ が $(g')^*S$ に入り、$f'(z,y')=y'$ となる条件なので同じである。全称量化についても、左辺の条件は $f(z)=g(y')$ であるすべての $z$ が $S$ に入ること。これは $f'^{-1}(y')$ のすべての $(z,y')$ が $(g')^*S$ に入るという右辺の条件と同じである。よって両等式が従う。$\square$
前層での全称量化
部分前層 $S\subset Z$ とは、各対象 $U$ で $S(U)\subset Z(U)$ が制限で閉じる（任意の $u\colon V\to U$ で $Z(u)(S(U))\subset S(V)$）ものをいう。前層の射の引き戻しは点ごとに計算されるので、$\operatorname{Sub}(Z)$ は部分前層の包含順序と同一視でき、部分前層 $T\subset Y$ の引き戻しは $(f^*T)(U)=f_U^{-1}(T(U))$ で与えられる。
集合上の全称量化を点ごとに適用するだけでは、前層の制限写像で閉じないことがある。例えば $\mathcal C$ を $0\to1$ の二元鎖、$Y=1$（各対象で一元集合）、$Z(1)=\emptyset$、$Z(0)=\{*\}$、$S=\emptyset$ とすると、集合の全称量化を点ごとに適用した値は、$U=1$ ではファイバー $Z(1)=\emptyset$ が空だから $\{*\}$、$U=0$ では $\emptyset$ となり、制限 $Y(1)\to Y(0)$ で閉じない（破れる条件：制限への閉性。実際は後述の式により $(\forall_fS)(1)=\emptyset$ になる）。そこで後続のすべての射も条件に入れる。
$\mathcal C$ を小圏、$f\colon Z\to Y$ を集合値前層の射とする。部分前層 $S\subset Z$ に対し、$\exists_f S$ は $f$ の点ごとの像であり、$\forall_f S$ は
$$
(\forall_f S)(U)=\{y\in Y(U)\mid\text{すべての }u\colon V\to U\text{ と }z\in Z(V)\text{ について、}f_V(z)=Y(u)y\Rightarrow z\in S(V)\}
$$
で定まる。このとき $\exists_f\dashv f^*\dashv\forall_f$ である。MM92 第 I 章の演習 10（p. 63）。
$f_U(S(U))$ は $U$ に関する制限に閉じる。実際、$f_U(s)$ を $u\colon V\to U$ で制限すると $f_V(Z(u)s)$ になり、$S$ が部分前層だから $Z(u)s\in S(V)$。ゆえに点ごとの像は部分前層である。$\exists_f S\subset T$ と $S\subset f^*T$ は各 $U$ の集合での同値を並べたものなので左随伴が従う。
右辺を $Q(U)$ とおく。$y\in Q(U)$ を $u\colon U'\to U$ で制限し、さらに $v\colon V\to U'$ と $z\in Z(V)$ をとる。$f_V(z)=Y(v)Y(u)y=Y(u\circ v)y$ なら、$y\in Q(U)$ の条件から $z\in S(V)$。したがって $Q$ は部分前層である。$f^*T\subset S$ なら $y\in T(U)$ のすべての制限 $Y(u)y$ は $T(V)$ にあるので、その逆像の $z$ は $S(V)$ に入り、$T\subset Q$。逆に $T\subset Q$ なら $z\in(f^*T)(U)$ に対し $f_U(z)\in T(U)\subset Q(U)$ として $u=\operatorname{id}_U$ を適用すれば $z\in S(U)$。ゆえに $f^*T\subset S$。これが右随伴の条件である。$\square$
この式の $u$ を省くと、今いる対象でのファイバーだけを調べることになる。前層の論理では、その後のすべての制限先でも述語が真であることを確かめて初めて全称量化となる。Heyting代数の部分前層の含意も同じ形の「すべての制限先」を使う。
合成した写像の量化
量化の範囲を二段階に分けても、一度に合成写像のファイバーを調べても同じ結果になる。ここでは射の合成と、論理式の中で量化する順序の関係を明示する。
写像 $f\colon X\to Y$ と $g\colon Y\to Z$ に対し、部分集合の間の写像として
$$
\exists_{g\circ f}=\exists_g\circ\exists_f,
\qquad \forall_{g\circ f}=\forall_g\circ\forall_f
$$
である。同じ等式は、部分対象の引き戻しに両随伴が存在する圏でも成り立つ。
集合上の存在量化は像を取る操作なので、その合成等式は 像(写像) の命題「合成による像」による。
全称量化について $z\in\forall_g(\forall_f S)$ とは、$g(y)=z$ となるすべての $y$ に対し、$f(x)=y$ となるすべての $x$ が $S$ に入ることである。これは $g(f(x))=z$ となるすべての $x$ が $S$ に入る条件である。$y$ のファイバーが空の場合、その $y$ に関する条件は自動的に真となるので同値を妨げない。
一般の圏では、引き戻しは $(g\circ f)^*=f^*g^*$ を満たす。随伴の同値を二回使うと
$$
\exists_g\exists_f S\le T
\Longleftrightarrow\exists_f S\le g^*T
\Longleftrightarrow S\le f^*g^*T
$$
となる。右随伴についても
$$
f^*g^*T\le S
\Longleftrightarrow g^*T\le\forall_f S
\Longleftrightarrow T\le\forall_g\forall_f S.
$$
したがって各合成は合成射の引き戻しの左右随伴であり、順序集合の随伴の一意性から結論が従う。$\square$
恒等写像のファイバーは一点集合なので、$\exists_{\operatorname{id}}S=\forall_{\operatorname{id}}S=S$ である。また、全単射のファイバーも一点集合だから、存在量化と全称量化は同じ集合を与える。しかし単射だけではこの結論は出ない。像に入らない点では、存在量化は偽、全称量化は真だからである。全射だけの場合も、ファイバーに二点以上あると、その一部だけが述語を満たす可能性が残る。
全称量化と交わり
集合上の存在量化は像であり、その合併との関係は 像 で扱う。右随伴である全称量化には、交わりを保つという対応する性質がある。空の族を含めた形にすると、空ファイバーの扱いとも整合する。
写像 $f\colon X\to Y$ と部分集合の族 $(S_i)_{i\in I}$ に対し
$$
\forall_f\left(\bigcap_{i\in I}S_i\right)
=\bigcap_{i\in I}\forall_f S_i
$$
である。$I=\emptyset$ のとき、左側の交わりは $X$、右側の交わりは $Y$ と解釈する。
$y$ が左辺に入る条件は、$f^{-1}(y)$ のすべての元がすべての $S_i$ に入ることである。二つの全称条件の順序を交換すると、すべての $i$ に対して $f^{-1}(y)\subseteq S_i$ となり、右辺への所属条件になる。$I=\emptyset$ のときも条件は常に真であり、$\forall_fX=Y$ となる。$\square$
$X=\{0,1\}$、$Y=\{*\}$ とし、$f$ を唯一の写像とする。$S_0=\{0\}$、$S_1=\{1\}$ とすれば、$\forall_fS_0=\forall_fS_1=\emptyset$ だが $\forall_f(S_0\cup S_1)=Y$ である。各点がどちらかの述語を満たすことから、ファイバー全体が同じ一方の述語を満たすとはいえない。
補集合で全称を表せる範囲
集合では、ファイバーのすべての元が $S$ に入ることは、$S$ の外に入る元が一つもないことと同値である。したがって
$$
\forall_fS=Y\setminus\exists_f(X\setminus S)
$$
となる。$S$ の補集合は $X$ 内、存在量化した後の補集合は $Y$ 内で取るので、二つの終域を混同してはならない。ファイバーが空の点でも、右辺の存在条件は偽になり、その否定は真になる。
この公式は部分集合のBoolean代数を使っている。部分前層では点ごとの補集合が部分前層にならないことがあり、Heyting代数の否定を代わりに使っても同じ公式は一般に成り立たない。既存の「集合の全称量化を点ごとに適用するだけでは閉じない」反例は、補集合による点ごとの計算にもそのまま当てはまる。
一般式の失敗は恒等写像ですでに確かめられる。$0\to1$ の二元鎖上の終対象前層 $1$ と、その部分前層 $A(0)=\{*\}$、$A(1)=\emptyset$ を取る。$f=\operatorname{id}_1$、$S=A$ なら、$\forall_f A=A$ だが、$\neg\exists_f\neg A=\neg\neg A=1$ である。$A$ は対象 $1$ では偽だが、その後の制限先で否定を維持できないため二重否定が真となる。全称量化そのものと、Heyting否定を二回用いた式は区別が必要である。部分前層の含意・否定の計算の基礎は Heyting代数 と MM92 I §8 Proposition 5（p. 56）を参照。
| 条件・操作 | 集合上での結果 | 境界となる例 |
|---|---|---|
| 空ファイバー | 存在は偽、全称は真 | 像に入らない終域の点 |
| 射の合成 | 同種の量化子を順に合成 | 量化範囲を二段階に分解 |
| 任意の交わり | 全称量化と交換する | 空族でも $\forall_fX=Y$ |
| 合併 | 全称量化とは一般に交換しない | 二点ファイバーを二つの述語で分割 |
| 補集合による全称の計算 | Boolean代数で成立 | 前層では二重否定が元に戻らない |
固定した条件を量化の外へ出す
集合上で $S\subseteq X$、$T\subseteq Y$ とすると、存在量化には
$$
\exists_f(S\cap f^*T)=(\exists_fS)\cap T
$$
という等式がある（MM92 IV §9 の式 (2)、p. 204）。これは、量化する変数によらず真偽が決まる条件を外に出せるという規則である。この等式は $\exists_fS=f(S)$、$f^*T=f^{-1}(T)$ として 像(写像) の命題「像と逆像の射影公式」による。空のファイバーを含む任意写像に適用できる。
全称量化では、$T$ に含まれる点に限れば
$$
(\forall_f(S\cap f^*T))\cap T=(\forall_fS)\cap T
$$
となる。$y\in T$ ならファイバー全体が自動的に $f^*T$ に含まれるので、残る条件はファイバー全体が $S$ に含まれることだけだからである。しかし、両辺の末尾の $\cap T$ を左側だけから除いて等式を主張することはできない。$y\notin T$ に空のファイバーがあると、その点も左側の全称量化には入ってしまう。たとえば $X=\emptyset$、$Y=\{*\}$、$T=\emptyset$ の場合、$\forall_f\emptyset=Y$ であり、右側は空集合である。
この違いから、随伴の存在だけと、量化と他の論理演算の交換を混同してはならない。等式を使う際には、射、述語の属する対象、ファイバーの空性をそれぞれ指定する必要がある。集合の具体的な計算から一般の圏へ進む場合は、同じ等式を保証する追加条件を別に確認する。
反例で確かめる条件
| 外す条件 | 反例 | 成り立たなくなること |
|---|---|---|
| 各ファイバーが一点であること（空ファイバーがないことは保つ） | $p\colon\{0,1\}\times\{a,b\}\to\{a,b\}$、$S=\{(0,a),(1,a),(0,b)\}$（ex-quantifiers-as-adjoints-image） | 像を全称量化に使うこと。$\exists_pS=\{a,b\}$ だが $\forall_pS=\{a\}$ |
| 写像の単射性（二つの集合の合併の保存を求める場合） | $f\colon\{0,1\}\to\{*\}$、$S_0=\{0\}$、$S_1=\{1\}$（ex-quantifiers-as-adjoints-union） | $\forall_f(S_0\cup S_1)=\forall_fS_0\cup\forall_fS_1$。左辺は $\{*\}$、右辺は空集合 |
関連項目
参考文献
Mathpediaは寄付と、参考文献の書籍リンク（Amazonアソシエイト）の紹介料で運営されています。 支援について ／ 寄付する
