内部論理
概要
内部論理（internal logic）とは、トポスの対象を型とし、論理式を部分対象として、論理結合子を部分対象の Heyting 代数の演算で、量化子を引き戻しの左随伴と右随伴で解釈することにより、トポスの中で論理式が成り立つことを定める仕組みである。部分対象分類子 $\Omega$ が真理値の対象になり、直観主義論理で証明できる式はどのトポスでも成り立つが、排中律は一般には成り立たない。前層のトポスでは、論理式が成り立つかどうかを各対象ごとに、含意・否定・全称についてはその後のすべての射まで見て判定する Kripke–Joyal 意味論で計算でき、とくに前層のトポスが Boolean になるのは土台の圏が亜群のときに限る。
集合 $X$ の部分集合 $\{x\in X\mid\varphi(x)\}$ は、条件 $\varphi$ を満たす元を集めて作る。トポスでは対象が元をもつとは限らないが、部分対象分類子 $\Omega$ を使えば、部分対象を「$\Omega$ に値をとる述語」とみなせる。そこで論理式を部分対象として解釈し、「トポスの中で成り立つ」ことを定義できる。これがトポスの内部論理である。
部分対象の全体は Heyting代数 をなし、量化子は引き戻しの随伴として得られる（量化子の随伴）。このため内部論理は一般に直観主義論理になり、排中律が成り立つとは限らない。前層のトポスでは、論理式が成り立つかどうかを「各段階 $c$ で、その後のすべての段階を見て判定する」という Kripke 型の規則で計算できる（Kripke–Joyal 意味論、thm-ilogic-kripke-joyal）。この記事ではその規則を証明し、それを使って、前層のトポスで排中律が成り立つのは土台の圏が亜群のときに限ることを示す（thm-ilogic-boolean）。
定義
以下、$\mathcal E$ を初等トポス（トポス の定義「初等トポス」）とする。対象 $X$ の部分対象の全体 $\operatorname{Sub}(X)$ は包含で半順序集合になり、部分対象分類子 の命題「特性射と部分対象の対応」により $\operatorname{Sub}(X)\cong\operatorname{Hom}(X,\Omega)$ である。次の 2 つの事実を使う。
- $\operatorname{Sub}(X)$ は Heyting 代数であり、射 $f\colon X\to Y$ による引き戻し $f^{-1}\colon\operatorname{Sub}(Y)\to\operatorname{Sub}(X)$ は Heyting 代数の準同型である（MM92 IV.8 Theorem 1）。
- $f^{-1}$ は左随伴 $\exists_f$ と右随伴 $\forall_f$ をもつ（MM92 IV.6 Proposition 3、IV.9 Proposition 3）。$\exists_f S$ は $S\rightarrowtail X\to Y$ の像である。
前層のトポスについては、1 は Heyting代数 の定理「部分前層の含意」、2 は 量化子の随伴 の定理「部分前層の量化子」で具体的に示されている。
$\mathcal E$ の対象を型とする。型 $X_1,\dots,X_n$ の変数の列 $\Gamma=(x_1{:}X_1,\dots,x_n{:}X_n)$ を文脈といい、$[\![\Gamma]\!]:=X_1\times\dots\times X_n$ とおく（$n=0$ なら終対象 $1$）。文脈 $\Gamma$ の型 $Y$ の項とは、射 $t\colon[\![\Gamma]\!]\to Y$ のことである（変数 $x_i$ は射影である）。
文脈 $\Gamma$ の論理式を次で帰納的に定める。
- 項 $t,s\colon[\![\Gamma]\!]\to Y$ に対し $t=s$。部分対象 $R\rightarrowtail Y$ と項 $t$ に対し $R(t)$。および $\top$、$\bot$。
- 論理式 $\varphi,\psi$ に対し $\varphi\land\psi$、$\varphi\lor\psi$、$\varphi\Rightarrow\psi$、$\lnot\varphi:=(\varphi\Rightarrow\bot)$。
- 文脈 $(\Gamma,y{:}Y)$ の論理式 $\varphi$ に対し、文脈 $\Gamma$ の論理式 $\exists y{:}Y\,\varphi$ と $\forall y{:}Y\,\varphi$。
文脈 $\Gamma$ の論理式 $\varphi$ の解釈 $[\![\varphi]\!]\in\operatorname{Sub}([\![\Gamma]\!])$ を次で定める。
- $[\![t=s]\!]$ は $t,s$ の等化子、$[\![R(t)]\!]:=t^{-1}(R)$、$[\![\top]\!]:=[\![\Gamma]\!]$、$[\![\bot]\!]:=0$（最小の部分対象）。
- $[\![\varphi\land\psi]\!]$、$[\![\varphi\lor\psi]\!]$、$[\![\varphi\Rightarrow\psi]\!]$ は、$\operatorname{Sub}([\![\Gamma]\!])$ の Heyting 代数としての交わり・結び・含意で定める。
- $\pi\colon[\![\Gamma]\!]\times Y\to[\![\Gamma]\!]$ を射影として、$[\![\exists y\,\varphi]\!]:=\exists_\pi[\![\varphi]\!]$、$[\![\forall y\,\varphi]\!]:=\forall_\pi[\![\varphi]\!]$。
$[\![\varphi]\!]$ が最大の部分対象 $[\![\Gamma]\!]$ に等しいとき、$\varphi$ は $\mathcal E$ で妥当である、または $\mathcal E$ の内部で成り立つという。
$[\![\varphi]\!]$ を $\{x\mid\varphi(x)\}$ とも書く。その特性射 $[\![\Gamma]\!]\to\Omega$ を $\varphi$ の値と考えれば、$\Omega$ が真理値の対象、$\mathrm{true}$ が「真」にあたる。この定義は、項として冪対象 $\Omega^X$ や所属関係 $\in$、$\lambda$ 抽象も許す Mitchell–Bénabou 言語（MM92 VI.5）の一部分である。
すべての対象 $X$ とすべての $S\in\operatorname{Sub}(X)$ で $S\lor\lnot S=X$ が成り立つとき、$\mathcal E$ は Boolean であるという。すなわち、論理式 $R(x)\lor\lnot R(x)$ がすべての部分対象 $R$ について妥当であることである。
Heyting 代数では $S\land S'=0$ なら $S'\le\lnot S$ なので、$S$ が補元 $S'$（$S\land S'=0$、$S\lor S'=X$）をもつことと $S\lor\lnot S=X$ は同値である。したがってこの定義は、すべての部分対象が補部分対象をもつという定義（Cohenトポス の定義「Boolean トポスと選択公理」）と一致する。
直感
集合の世界では、条件 $\varphi(x)$ は各元 $x$ について真か偽かに決まる。前層のトポスでは、真偽は「段階」$c$ ごとに決まり、ある段階で真になったものは後の段階でも真のままである（prop-ilogic-monotone）。$\varphi\Rightarrow\psi$ や $\lnot\varphi$ は、今の段階だけでなく「これから先のどの段階でも」という条件になる。たとえば $\lnot\varphi$ は「この先どの段階でも $\varphi$ は真にならない」ことである。すると「$\varphi$ はまだ真でないが、いつか真になりうる」段階では、$\varphi$ も $\lnot\varphi$ も成り立たない。これが排中律の破れ方であり、直観主義論理 の Kripke モデルと同じ形をしている。
前層のトポスの Kripke–Joyal 意味論
ここでは $\mathcal C$ を小さい圏とし、$\mathcal E=\widehat{\mathcal C}$ を前層のトポスとする。前層 $X$ の部分対象は部分前層と 1 対 1 に対応する（部分対象分類子 の「前層の圏における構成」）。前層 $X$、対象 $c$、$a\in X(c)$、射 $f\colon d\to c$ について、$a\cdot f:=X(f)(a)\in X(d)$ と書く。文脈 $\Gamma$ について $[\![\Gamma]\!](c)$ の元は組 $a=(a_1,\dots,a_n)$ である（極限は対象ごとに計算される）。
文脈 $\Gamma$ の論理式 $\varphi$、$\mathcal C$ の対象 $c$、$a\in[\![\Gamma]\!](c)$ について、$a\in[\![\varphi]\!](c)$ であることを
$$
c\Vdash\varphi(a)
$$
と書き、「$c$ は $\varphi(a)$ を強制する」という。
$c\Vdash\varphi(a)$ で $f\colon d\to c$ なら $d\Vdash\varphi(a\cdot f)$ である。
$[\![\varphi]\!]$ は部分前層なので、制限で閉じている。$\square$
$\mathcal E=\widehat{\mathcal C}$ とし、$\varphi,\psi$ を文脈 $\Gamma$ の論理式、$c$ を $\mathcal C$ の対象、$a\in[\![\Gamma]\!](c)$ とする。このとき次が成り立つ。
- $c\Vdash(t=s)(a)\iff t_c(a)=s_c(a)$。$c\Vdash R(t)(a)\iff t_c(a)\in R(c)$。$c\Vdash\top$ はつねに成り立ち、$c\Vdash\bot$ は決して成り立たない。
- $c\Vdash(\varphi\land\psi)(a)\iff c\Vdash\varphi(a)$ かつ $c\Vdash\psi(a)$。
- $c\Vdash(\varphi\lor\psi)(a)\iff c\Vdash\varphi(a)$ または $c\Vdash\psi(a)$。
- $c\Vdash(\varphi\Rightarrow\psi)(a)\iff$ すべての射 $f\colon d\to c$ について、$d\Vdash\varphi(a\cdot f)$ ならば $d\Vdash\psi(a\cdot f)$。
- $c\Vdash\lnot\varphi(a)\iff$ $d\Vdash\varphi(a\cdot f)$ となる射 $f\colon d\to c$ は存在しない。
さらに $\varphi$ を文脈 $(\Gamma,y{:}Y)$ の論理式とすると、次が成り立つ。 - $c\Vdash(\exists y\,\varphi)(a)\iff$ ある $b\in Y(c)$ について $c\Vdash\varphi(a,b)$。
- $c\Vdash(\forall y\,\varphi)(a)\iff$ すべての射 $f\colon d\to c$ とすべての $b\in Y(d)$ について $d\Vdash\varphi(a\cdot f,b)$。
とくに $\varphi$ が妥当であることは、すべての $c$ とすべての $a\in[\![\Gamma]\!](c)$ で $c\Vdash\varphi(a)$ となることと同値である。
$P:=[\![\Gamma]\!]$ とおく。各項目は、$\operatorname{Sub}(P)$ の演算と量化子を部分前層で具体的に書いたものを、強制の記号で読み替えたものである。
1：極限は対象ごとに計算されるので、等化子 $[\![t=s]\!]$ の $c$ での値は $\{a\in P(c)\mid t_c(a)=s_c(a)\}$、引き戻し $t^{-1}(R)$ の値は $\{a\mid t_c(a)\in R(c)\}$ である。$\top$ は $P$ 自身、$\bot$ は空な部分前層である。
2・3：部分前層 $S,T\subset P$ について、対象ごとの共通部分 $c\mapsto S(c)\cap T(c)$ と和集合 $c\mapsto S(c)\cup T(c)$ はどちらも制限で閉じているので部分前層であり、包含の順序で $S,T$ の下限と上限になる。よって $\operatorname{Sub}(P)$ の交わりと結びは対象ごとの共通部分と和集合である。
4：Heyting代数 の定理「部分前層の含意」により、
$$
[\![\varphi\Rightarrow\psi]\!](c)=\{a\in P(c)\mid\text{すべての }f\colon d\to c\text{ について、}a\cdot f\in[\![\varphi]\!](d)\Rightarrow a\cdot f\in[\![\psi]\!](d)\}
$$
である。これは 4 の右辺そのものである。
5：4 で $\psi=\bot$ とし、1 により $d\Vdash\bot$ が決して成り立たないことを使う。
6：量化子の随伴 の定理「部分前層の量化子」により、$\exists_\pi$ は対象ごとの像をとる操作である。$\pi_c(a,b)=a$ なので、$a\in(\exists_\pi[\![\varphi]\!])(c)$ は「ある $b\in Y(c)$ で $(a,b)\in[\![\varphi]\!](c)$」と同値である。
7：同じ定理により、$a\in(\forall_\pi[\![\varphi]\!])(c)$ は「すべての $f\colon d\to c$ と、$\pi_d(z)=a\cdot f$ を満たすすべての $z\in(P\times Y)(d)$ について $z\in[\![\varphi]\!](d)$」と同値である。$\pi_d(z)=a\cdot f$ を満たす $z$ はちょうど $(a\cdot f,b)$（$b\in Y(d)$）の形の元なので、7 の右辺になる。
最後の主張は、$[\![\varphi]\!]=P$ がすべての $c$ で $[\![\varphi]\!](c)=P(c)$ であることと同じだからである。$\square$
3 と 6 は、前層のトポスでは選言と存在が「その段階で実際にどちらか・どれかが分かる」という BHK 解釈どおりの形をとることを示している。一方 4・5・7 には「その後のすべての段階」が入る。$\mathcal C$ が半順序集合 $W$ のとき、$W^{\mathrm{op}}$ を情報の増える向きと読めば、これは 直観主義論理 の注意「完全性定理の出典と Kripke モデル」の Kripke モデルの規則と同じである（MM92 VI.7）。
$\mathcal E$ を任意の初等トポス、$\Gamma$ を文脈、$\varphi_1,\dots,\varphi_m$ を $\Gamma$ の論理式とする。命題変数 $p_1,\dots,p_m$ の論理式 $\theta$ が直観主義論理で証明可能なら、$\theta$ の $p_i$ に $\varphi_i$ を代入した論理式は $\mathcal E$ で妥当である。
$\operatorname{Sub}([\![\Gamma]\!])$ は Heyting 代数であり、$\land,\lor,\Rightarrow,\bot$ はその演算で解釈される。代入した論理式の解釈は、付値 $p_i\mapsto[\![\varphi_i]\!]$ による $\theta$ の Heyting 代数での値（直観主義論理 の定義「Heyting 代数での値」）に等しい。同じ記事の定理「Heyting 代数に関する健全性」により、その値は最大元 $[\![\Gamma]\!]$ である。$\square$
量化子を含む直観主義述語論理の推論規則も、すべてのトポスで妥当な論理式を妥当な論理式に移す（MM92 VI.5。この記事では証明しない）。トポスの中では、排中律と選択公理を使わない「構成的な」議論であれば、変数を元のように扱って普通に推論してよい。逆に、排中律を使う議論は一般のトポスでは通らない。この意味で、トポスは構成的数学のモデルになる。
層のトポスと一般のトポス
位相が自明でない景の上の層のトポス $\operatorname{Sh}(\mathcal C,J)$ でも強制関係は同じく $a\in[\![\varphi]\!](c)$ で定まるが、3 と 6 は被覆を使った形に変わる。たとえば $c\Vdash(\varphi\lor\psi)(a)$ は「$c$ の被覆 $\{f_i\colon c_i\to c\}$ があって、各 $i$ で $c_i\Vdash\varphi(a\cdot f_i)$ または $c_i\Vdash\psi(a\cdot f_i)$」と同値である（MM92 VI.7 Theorem 1。この記事では証明しない）。選言は全体では決まらなくても、局所的には決まればよい。一般の初等トポスでは、元 $a\in X(c)$ の代わりに任意の射 $a\colon U\to X$（一般化された元）を使い、「$a$ が $[\![\varphi]\!]$ を経由する」ことを $U\Vdash\varphi(a)$ とする。このとき 3・6 では $U$ へのエピ射による被覆が現れる（MM92 VI.6 Theorem 1）。
排中律と亜群
小さい圏 $\mathcal C$ について、次は同値である。
- 前層のトポス $\widehat{\mathcal C}$ は Boolean である。
- $\mathcal C$ は亜群である。すなわち $\mathcal C$ のすべての射は同型射である。
外の集合論は通常の（古典論理の）集合論とする。
2 ⇒ 1。前層 $X$、部分前層 $S\subset X$、$a\in X(c)$ をとる。$a\in S(c)$ なら $a\in(S\lor\lnot S)(c)$ である。$a\notin S(c)$ とする。もし射 $f\colon d\to c$ で $a\cdot f\in S(d)$ となるものがあれば、$f$ は同型なので $a=(a\cdot f)\cdot f^{-1}\in S(c)$ となり矛盾する（$S$ は制限で閉じている）。よって thm-ilogic-kripke-joyal の 5 により $a\in(\lnot S)(c)$ である。いずれにせよ $(S\lor\lnot S)(c)=X(c)$ である。
1 ⇒ 2。射 $f\colon d\to c$ をとる。表現可能前層 $h_c=\operatorname{Hom}_{\mathcal C}(-,c)$ の部分前層
$$
S(e):=\{g\colon e\to c\mid g=f\circ k\text{ となる }k\colon e\to d\text{ がある}\}
$$
を考える（$f$ が生成する篩(圏論)）。仮定から $\mathrm{id}_c\in(S\lor\lnot S)(c)$ であり、thm-ilogic-kripke-joyal の 3 により $\mathrm{id}_c\in S(c)$ または $\mathrm{id}_c\in(\lnot S)(c)$ である。$h_c$ の制限は合成なので $\mathrm{id}_c\cdot f=f\in S(d)$ であり、同じ定理の 5 により $\mathrm{id}_c\notin(\lnot S)(c)$ である。よって $\mathrm{id}_c\in S(c)$、すなわち $f\circ k=\mathrm{id}_c$ となる $k\colon c\to d$ がある。
こうして $\mathcal C$ のすべての射は右逆射をもつ。$k$ にもこれを当てはめて $k\circ l=\mathrm{id}_d$ となる $l$ をとると、$l=(f\circ k)\circ l=f\circ(k\circ l)=f$ なので $k\circ f=\mathrm{id}_d$ である。したがって $f$ は同型射である。$\square$
この定理は MM92 第 VI 章の演習 2 にも挙げられている。群 $G$ を 1 対象の圏 $BG$ とみれば、トポス の例「$G$ 集合の圏」の $G$ 集合のトポスは Boolean である。とくに $\mathbf{Set}$（1 点の圏の上の前層）の内部論理は古典論理である。
例と反例
$\mathcal C$ を、対象 $0,1$ と恒等射以外にただ 1 つの射 $u\colon0\to1$ をもつ圏とする。前層 $X$ は集合 $X(1)$、$X(0)$ と写像 $X(u)\colon X(1)\to X(0)$ の組である。表現可能前層 $h_1$ は $h_1(1)=\{\mathrm{id}_1\}$、$h_1(0)=\{u\}$ であり、その部分前層は
$$
\emptyset,\qquad S\ (S(1)=\emptyset,\ S(0)=\{u\}),\qquad h_1
$$
の 3 つである（$T(1)=\{\mathrm{id}_1\}$ とすると、制限で閉じるために $T(0)=\{u\}$ が必要になる）。$\operatorname{Sub}(h_1)$ は 3 元の鎖 $\emptyset< S< h_1$ である。
thm-ilogic-kripke-joyal の 5 で $\lnot S$ を計算する。$\mathrm{id}_1\cdot u=u\in S(0)$ なので $\mathrm{id}_1\notin(\lnot S)(1)$、$u\in S(0)$ なので $u\notin(\lnot S)(0)$ であり、$\lnot S=\emptyset$ である。よって $(S\lor\lnot S)(1)=\emptyset\ne h_1(1)$ で、論理式 $S(x)\lor\lnot S(x)$（$x{:}h_1$）は妥当でない。また $\lnot\lnot S=\lnot\emptyset=h_1\ne S$ なので、$\lnot\lnot S(x)\Rightarrow S(x)$ も妥当でない。
段階 $1$ では「$x\in S$」はまだ真でないが、後の段階 $0$ で真になる。だから $\lnot$ も成り立たない。$\operatorname{Sub}(h_1)$ は 直観主義論理 の例「反例：3 元の鎖と排中律」の Heyting 代数そのものである。この圏 $\mathcal C$ は亜群でないので、thm-ilogic-boolean とも合っている。
位相空間 $X$ 上の層のトポス $\operatorname{Sh}(X)$ では、終対象 $1$ の部分対象は $X$ の開集合と 1 対 1 に対応し、順序は包含である（トポス の命題「位相空間の層のトポスの部分対象分類子」）。したがって空の文脈の論理式の値は開集合であり、$\lnot U$ は $X\setminus U$ の内部、$U\Rightarrow V$ は $(X\setminus U)\cup V$ の内部である（Heyting代数 の例「開集合の束」）。$X=\mathbb{R}$、$U=(0,\infty)$ なら $U\lor\lnot U=\mathbb{R}\setminus\{0\}$ であり、点 $0$ が「どちらとも決まらない」場所になる。
反例の表
| 外す条件 | 反例 | 成り立たなくなること |
|---|---|---|
| $\mathcal C$ が亜群であること（thm-ilogic-boolean） | 2 点の鎖 $0\to1$（ex-ilogic-sierpinski） | 排中律 $S(x)\lor\lnot S(x)$ の妥当性 |
| 位相が自明であること（前層のトポス） | 2 点の離散空間 $\{p,q\}$ 上の層のトポスで、開集合 $\{p\},\{q\}$ に対応する $1$ の部分対象 $U_p,U_q$ | thm-ilogic-kripke-joyal の 3 の形。$U_p\lor U_q$ は開集合 $\{p,q\}$ なので全体 $\{p,q\}$ で強制されるが、$U_p$ も $U_q$ も全体では強制されない |
| 7 で後のすべての射 $f$ を動かすこと | 2 点の鎖の上で、$Z(1)=\emptyset$、$Z(0)=\{*\}$ の前層 $Z$ と空な部分前層（量化子の随伴 の「前層での全称量化」の例） | 対象ごとに全称をとったものが部分前層になること。段階 $1$ ではファイバーが空なので真、段階 $0$ では偽となり、制限で閉じない |
2 行目では $\lnot U_p$ は $\{q\}$ の内部、すなわち $U_q$ なので、$U_p\lor\lnot U_p$ は全体である。排中律のこの例が成り立っていても、前層の形の選言の規則は使えない。
関連項目
参考文献
Mathpediaは寄付と、参考文献の書籍リンク（Amazonアソシエイト）の紹介料で運営されています。 支援について ／ 寄付する
