雑記帳
置換公理型を認めない初等トポスの一般論の中で、集合 {x∈X|P(x)} はどのようにして構成されるのか
目次
従来の集合論とトポス理論の比較
一口に「集合論」といっても
- 従来の ZFC 集合論 (選択公理を含めるツェルメロ＝フレンケル集合論)
- トポス理論ベースの ETCS 集合論 (ウィリアム・ローヴェアによる集合の圏の初等理論)
は、それぞれ趣が大きく異なる。
最も大きな違いの一つに、
- ZFC においては「(集合の要素に関する) 論理式の組み立て手続き」というのは「一階述語論理」が担っている
というのに対して
- ETCS (より一般にトポス理論) においては「(抽象集合の要素に関する) 論理式の組み立て手続き」というのは「トポスの公理それ自体」が担っている
という点である。
具体的に ZFC の場合、Set-builder notation (集合の内包的記法) による部分集合 \(\{ x\in X \:|\: P(x) \}\) の構成を考える際に必要になる述語 \(P(x)\) というのは理論の根源要素にあたる「具体集合」として構成されているわけではなく、公理型 (axiom schema) の持つパワーを借りることで「一階の言語で書かれた任意の述語」を集合の理論の中に直接持ち込んでいる。即ち、論理式の組み立ての部分に「集合」が関与してこない。
例えば、
\[
\{ x\in X \:|\: x \in X_1 \wedge x \in X_2 \}
\]
という式の右部の「\(\in\)」や「\(\wedge\)」といった記号が、予め「写像」として構成されているものであったかどうかを考えてみれば、要旨が見えてくるのではないだろうか。
一方 ETCS の場合、ZFC のように論理式の組み立て機構を一階述語論理から無理やり引っ張ってくるのではなく、与えられた公理の中だけで具体的に実装するというアプローチをとる。
というのも、トポスの一般論では「置換公理型 (axiom schema of replacement)」或いは「分出公理型 (axiom schema of specification)」が公理として含まれていない。
即ち、もし論理式を集合構成の中で取り扱いたいのであれば、まずその組み立てたい論理式の中で用いる「論理演算子」たちを全て先行して定義しておくことが前提条件として求められる。
わかりやすく言い換えると、先ほどの「\(\in\)」や「\(\wedge\)」のような記号が持つ意味・振舞いが適切に反映されたモノを理論の構成要素の一つとして組み立てておいてあげる必要が生じてくる。
余談
トポスは一般に部分対象分類子を要素として持つ対象である「真理値対象 \(\Omega\)」を持つが、その真理値対象 \(\Omega\) が余積対象 \(2:=1+1\) と同形であることはトポスの公理からは証明されない。
一方、ETCS 公理系からは「\(\Omega\cong 2\)」を定理として証明可能ではあるが、かといって初めから \(2\) を真理値対象として扱うことは避ける方針をとる。
その具体的な理由としては、「同形射 \(i:\Omega\rightarrow 2\) の選択に絶対的なものがない」、わかりやすく言い換えると「\({\rm inj}_1\) と \({\rm inj}_2\) のどちらに \({\rm true}\) を対応させるのかという選択に自然なものがない」というためである。
もう一つは、例えば考えてみてほしいのだが、ETCS 集合論における定理として \({\mathbb{R}}\times {\mathbb{R}} \cong {\mathbb{R}}\) が証明されるからといって、適当な同形射 \(i:{\mathbb{R}}\times {\mathbb{R}} \rightarrow {\mathbb{R}}\) を選択した上で、\({\mathbb{R}}\times {\mathbb{R}}\) の代わりに \({\mathbb{R}}\) という集合を使用し、射影を \({\rm prj}_1':{\mathbb{R}} \rightarrow {\mathbb{R}}\times {\mathbb{R}}\) \(({\rm prj}_1' = i^{-1} {\sf \, ⨟ \,} {\rm prj}_1 {\sf \, ⨟ \,} i)\) などと書いている場面に遭遇したらどう思うだろうか。少なからずそれに対してあまり嬉しくないと感じる人はいるだろう。
トポスの一般論の中で論理式を取り扱うシステムを組み立てる
論理式のピースとなる論理演算子 +α の構成
ZFC のような「集合」が主役となる集合論の観点からは、「そんなこと現実問題として可能なのか」と疑問に思うかもしれない。
トポスの公理が強力なのは、実際にそういった論理演算子を全てトポスの持つ射として構成出来てしまうところにある。
では実際に構成していく。
まず式の意味をわかりやすくするために以下の表記を導入しておく。
\[
\begin{align}
{\rm const}(x) :=& ! {\sf \, ⨟ \,} x \\
{\rm arrToEl}(f) :=& \lambda[{\rm prj}_2 {\sf \, ⨟ \,} f] \\
\end{align}
\]
注意してほしいのは、これらはあくまでも糖衣構文 (syntactic sugar) のようなものであるという点である。
つまり通常の射のように \({\rm arrToEl}\) を \(f\) から切り離して考えることは基本的にできないが、かといってこの表記が技術的に欠かせない状況が存在するわけでも全くない。
つまり通常の射のように \({\rm arrToEl}\) を \(f\) から切り離して考えることは基本的にできないが、かといってこの表記が技術的に欠かせない状況が存在するわけでも全くない。
相等関係 (equality)
\(A\) を抽象集合としたとき、\(A\) の2つの要素 \(a_1,a_2:1\rightarrow A\) が同じであるのかを判定する演算子 \((==):A\times A\rightarrow \Omega\) は次のように構成できる。
\[
\begin{align}
\langle A,A \rangle {\sf \, ⨟ \,} {\rm prj}_1 &= A \\
\langle A,A \rangle {\sf \, ⨟ \,} {\rm prj}_2 &= A \\
\end{align}
\]
より、射影をレトラクションとして持つため分裂モニックであることが従う。
分裂モニック射はモニック射であり、さらに部分対象分類子の公理より、任意のモニック射はその分類射をその圏に持つため、次の射
\[
\chi[\langle A,A \rangle]:A\times A\rightarrow \Omega
\]
が得られる。
この射が、構成したかった射となる。
まとめると、相等関係 \((==):A \times A \rightarrow \Omega\) は次のように構成される。
\[
(==):=\chi[\Delta]
\]
局所要素関係 (local membership relation)
\(A\) を抽象集合としたとき、\(A\) の要素 \(a:1\rightarrow A\) が、\(A\) の冪集合の要素として与えられる \(A\) の部分集合 \(S:1\rightarrow \Omega^A\) に属しているのかを判定する演算子 \((\in):A\times \Omega^A \rightarrow \Omega\) は次のように構成できる。
とはいっても非常に単純で、この判定は指数対象公理により存在が保証される評価射 \({\rm ev}:\Omega^A \times A\rightarrow \Omega\) によって実現し、そこに「見やすさ向上のための入力の対を反転させる射」を合成してあげたものがそれに該当する。
まとめると、局所要素関係 \((\in): A \times \Omega^{A} \rightarrow \Omega\) は次のように構成される。
\[
(\in):=\langle {\rm prj}_2, {\rm prj}_1 \rangle {\sf \, ⨟ \,}{\rm ev}
\]
余談
注意点として、この \((\in)\) は「局所的 (local)」な要素関係であり、よく目にする「大域的 (global)」な要素関係とはモノが異なる。
また入力のツイストは必ずしも必要であるわけではない。
論理積 (conjunction)
2つの真理値 \(t_1,t_2:1\rightarrow \Omega\) が与えられたとき、それらの論理積をとる演算子 \((\wedge):\Omega\times \Omega\rightarrow \Omega\) は次のように構成できる。
まず部分対象分類子の存在はトポスの公理により認められているので、射 \({\rm true}:1 \rightarrow \Omega\) が得られる。
ここで、終対象の定義より、終射 \(!:\Omega \rightarrow 1\) の存在が従い、さらに合成射 \({\rm true}{\sf \, ⨟ \,} !\) は、終対象をコドメインにとる平行な射は同じであるという終対象の定義より恒等射 \(1:1\rightarrow 1\) になる。つまり、\({\rm true}\) はレトラクション \(!\) を持つことから (分裂) モニックになる。
続いて積の定義より、\(\Omega:\Omega\rightarrow \Omega\) 同士が引き起こす射として入力のコピーの役割を果たす対角射 \(\Delta:\Omega \rightarrow \Omega \times \Omega\) の存在が従う。この射も積の定義より、合成射 \(\Delta {\sf \, ⨟ \,} {\rm prj}_1\) と \(\Delta {\sf \, ⨟ \,} {\rm prj}_2\) が共に恒等射 \(\Omega:\Omega\rightarrow \Omega\) になる。つまり \(\Delta\) は射影をレトラクションに持つため、(分裂) モニックになる。
ここで一般的抽象的ナンセンスより、モニック射同士の合成射はモニック射になるため、\({\rm true} {\sf \, ⨟ \,} \Delta\) はモニックになる。
部分対象分類子の定義より任意のモニック射はその分類射を一意に持つため、そのモニック射の分類射 \(\chi[{\rm true} {\sf \, ⨟ \,} \Delta]:\Omega \times \Omega \rightarrow \Omega\) の存在が従う。
この射が論理積の役割を果たす射となる。
まとめると、論理積 \((\wedge):\Omega \times \Omega \rightarrow \Omega\) は次のように構成される。
\[
(\wedge):=\chi[{\rm true} {\sf \, ⨟ \,} \Delta]
\]
含意 (implication)
2つの真理値 \(x,y:1\rightarrow \Omega\) が与えられたとき、それらの含意をとる演算子 \((\Rightarrow):\Omega\times \Omega\rightarrow \Omega\) は次のように構成できる。
まず含意が満たすべき関係式は
\[
x \Rightarrow y :\Leftrightarrow (x == x \wedge y)
\]
である。この関係式を元に射 \((\Rightarrow)\) のあるべき形を以下のように抽出することができる。
\[
\begin{align}
x \Rightarrow y &\Leftrightarrow (x == x \wedge y) \\
\langle x,y \rangle {\sf \, ⨟ \,} (\Rightarrow) &\Leftrightarrow \langle x, x \wedge y \rangle {\sf \, ⨟ \,} (==) \\
\langle x,y \rangle {\sf \, ⨟ \,} (\Rightarrow) &\Leftrightarrow \langle x, \langle x,y \rangle {\sf \, ⨟ \,} (\wedge) \rangle {\sf \, ⨟ \,} (==) \\
\langle x,y \rangle {\sf \, ⨟ \,} (\Rightarrow) &\Leftrightarrow \langle x,y \rangle {\sf \, ⨟ \,} (\langle {\rm prj}_1, (\wedge) \rangle {\sf \, ⨟ \,} (==)) \\
\langle x,y \rangle {\sf \, ⨟ \,} (\Rightarrow) &\Leftrightarrow \langle x,y \rangle {\sf \, ⨟ \,} (\Delta {\sf \, ⨟ \,} ({\rm prj}_1 \times (\wedge)) {\sf \, ⨟ \,} (==)) \\
\end{align}
\]
まとめると、含意 \((\Rightarrow):\Omega \times \Omega \rightarrow \Omega\) は次のように構成される。
\[
(\Rightarrow):= \Delta {\sf \, ⨟ \,} ({\rm prj}_1 \times (\wedge)) {\sf \, ⨟ \,} (==)
\]
全称量化子 (universal quantifier)
\(A\) を抽象集合としたとき、\(A\) の各要素に対して真理値が定められた \(\Omega^A\) の要素が「全ての \(A\) の要素に対して \({\rm true}\) を定めるものであるのか」を判定する演算子 \((\forall_A):\Omega^A \rightarrow \Omega\) は次のように構成できる。
まず、「全ての \(A\) の要素に対して \({\rm true}\) を定める \(\Omega^A\) の要素」というのは
\[
{\rm arrToEl}({{\rm const}}({\rm true}))
\]
として得られる。(大域) 要素である以上、終射をレトラクションとして持つためこの射もモニックということになる。
つまり再び部分対象分類子の公理より、そのモニック射の分類射の存在が従うが、その射が構成したかった射に相当する。
まとめると、全称量化子 \((\forall_A):\Omega^A \rightarrow \Omega\) は次のように構成される。
\[
(\forall_A):=\chi[{\rm arrToEl}({\rm const}({\rm true}))]
\]
偽 (false)
偽 \({\rm false}:1 \rightarrow \Omega\) は次のように構成できる。
まず \({\rm false}\) が満たすべき推論規則は、
- \({\rm false}\) であるならば、任意の結論が正しくなる
これを型理論っぽく書くと
\[
{\rm false} \vdash \phi
\]
である。
ここで、\(\forall x:\Omega[x]\) という仮定、つまり「全ての真理値が真である」という仮定の下では、上のような「任意の結論が正しい」という状況を作れるという点に注意してほしい。
つまり「偽であるべきルール」を満たしている \(\forall x:\Omega[x]\) を \({\rm false}\) の定義として採用してしまえばよい。因みにその記号は以下のような射の合成として実現することになる。
\[
\begin{align}
{\rm false} &\Leftrightarrow \forall x:\Omega[x] \\
{\rm false} &\Leftrightarrow \forall x:\Omega[\langle {\rm arrToEl}(\Omega), x \rangle {\sf \, ⨟ \,} {\rm ev}] \\
{\rm false} &\Leftrightarrow {\rm arrToEl}(\Omega) {\sf \, ⨟ \,} \lambda[{\rm ev}] {\sf \, ⨟ \,} (\forall_{\Omega}) \\
{\rm false} &\Leftrightarrow {\rm arrToEl}(\Omega) {\sf \, ⨟ \,} (\forall_{\Omega}) \\
\end{align}
\]
まとめると、偽 \({\rm false}:1 \rightarrow \Omega\) は次のように構成される。
\[
{\rm false}:={\rm arrToEl}(\Omega) {\sf \, ⨟ \,} (\forall_{\Omega})
\]
否定 (negation)
真理値 \(x:1\rightarrow \Omega\) が与えられたとき、その否定をとる演算子 \((\neg):\Omega\rightarrow \Omega\) は次のように構成できる。
まず否定が満たすべき関係式は
\[
\neg x :\Leftrightarrow x \Rightarrow {\rm false}
\]
である。この関係式を元に射 \((\neg)\) のあるべき形を以下のように抽出することができる。
\[
\begin{align}
\neg x &\Leftrightarrow x \Rightarrow {\rm false} \\
x {\sf \, ⨟ \,} (\neg) &\Leftrightarrow \langle x, {\rm false} \rangle {\sf \, ⨟ \,} (\Rightarrow) \\
x {\sf \, ⨟ \,} (\neg) &\Leftrightarrow x {\sf \, ⨟ \,} \langle \Omega, {\rm const}({\rm false}) \rangle {\sf \, ⨟ \,} (\Rightarrow) \\
\end{align}
\]
まとめると、否定 \((\neg):\Omega \rightarrow \Omega\) は次のように構成される。
\[
(\neg):=\langle \Omega, {\rm const}({\rm false}) \rangle {\sf \, ⨟ \,} (\Rightarrow)
\]
論理和 (disjunction)
2つの真理値 \(x,y:1\rightarrow \Omega\) が与えられたとき、それらの論理和をとる演算子 \((\vee):\Omega\times \Omega\rightarrow \Omega\) は次のように構成できる。
まず論理和が満たすべき関係式は
\[
x \vee y :\Leftrightarrow \forall w:\Omega[((x\Rightarrow w)\wedge(y\Rightarrow w))\Rightarrow w]
\]
である。この関係式を元に射 \((\vee)\) のあるべき形を以下のように抽出することができる。
\[
\begin{align}
x \vee y \Leftrightarrow & \forall w:\Omega[((x\Rightarrow w)\wedge(y\Rightarrow w))\Rightarrow w] \\
\langle x,y \rangle {\sf \, ⨟ \,} (\vee) \Leftrightarrow & \forall w:\Omega[((\langle x,w \rangle {\sf \, ⨟ \,} (\Rightarrow))\wedge(\langle y,w \rangle {\sf \, ⨟ \,} (\Rightarrow)))\Rightarrow w] \\
\langle x,y \rangle {\sf \, ⨟ \,} (\vee) \Leftrightarrow & \forall w:\Omega[(\langle \langle x,w \rangle {\sf \, ⨟ \,} (\Rightarrow), \langle y,w \rangle {\sf \, ⨟ \,} (\Rightarrow) \rangle {\sf \, ⨟ \,} (\wedge) )\Rightarrow w] \\
\langle x,y \rangle {\sf \, ⨟ \,} (\vee) \Leftrightarrow & \forall w:\Omega[\langle (\langle \langle x,w \rangle {\sf \, ⨟ \,} (\Rightarrow), \langle y,w \rangle {\sf \, ⨟ \,} (\Rightarrow) \rangle {\sf \, ⨟ \,} (\wedge)), w \rangle {\sf \, ⨟ \,} (\Rightarrow)] \\
\langle x,y \rangle {\sf \, ⨟ \,} (\vee) \Leftrightarrow & \forall w:\Omega[\langle \langle x,y \rangle, w \rangle {\sf \, ⨟ \,} \Delta {\sf \, ⨟ \,} ( (\Delta {\sf \, ⨟ \,} ( ((({\rm prj}_1 {\sf \, ⨟ \,} {\rm prj}_1) \times {\rm prj}_2 ) {\sf \, ⨟ \,} (\Rightarrow))\times ((({\rm prj}_1 {\sf \, ⨟ \,} {\rm prj}_2) \times {\rm prj}_2 ) {\sf \, ⨟ \,} (\Rightarrow)) ) {\sf \, ⨟ \,} (\wedge)) \times {\rm prj}_2 ) {\sf \, ⨟ \,} (\Rightarrow)] \\
\langle x,y \rangle {\sf \, ⨟ \,} (\vee) \Leftrightarrow & \langle x,y \rangle {\sf \, ⨟ \,} \lambda[\Delta {\sf \, ⨟ \,} ( (\Delta {\sf \, ⨟ \,} ( ((({\rm prj}_1 {\sf \, ⨟ \,} {\rm prj}_1) \times {\rm prj}_2 ) {\sf \, ⨟ \,} (\Rightarrow))\times ((({\rm prj}_1 {\sf \, ⨟ \,} {\rm prj}_2) \times {\rm prj}_2 ) {\sf \, ⨟ \,} (\Rightarrow)) ) {\sf \, ⨟ \,} (\wedge)) \times {\rm prj}_2 ) {\sf \, ⨟ \,} (\Rightarrow)] {\sf \, ⨟ \,} (\forall_{\Omega}) \\
\end{align}
\]
まとめると、論理和 \((\vee):\Omega \times \Omega \rightarrow \Omega\) は次のように構成される。
\[
(\vee):=\lambda[\Delta {\sf \, ⨟ \,} ( (\Delta {\sf \, ⨟ \,} ( ((({\rm prj}_1 {\sf \, ⨟ \,} {\rm prj}_1) \times {\rm prj}_2 ) {\sf \, ⨟ \,} (\Rightarrow))\times ((({\rm prj}_1 {\sf \, ⨟ \,} {\rm prj}_2) \times {\rm prj}_2 ) {\sf \, ⨟ \,} (\Rightarrow)) ) {\sf \, ⨟ \,} (\wedge)) \times {\rm prj}_2 ) {\sf \, ⨟ \,} (\Rightarrow)] {\sf \, ⨟ \,} (\forall_{\Omega})
\]
存在量化子 (existential quantifier)
\(A\) を抽象集合としたとき、\(A\) の各要素に対して真理値が定められた \(\Omega^A\) の要素が「ある \(A\) の要素について \({\rm true}\) を定めるものが存在するのか」を判定する演算子 \((\exists_A):\Omega^A \rightarrow \Omega\) は次のように構成できる。
まず存在量化子が満たすべき関係式は、\(a:1\rightarrow A\) を \(A\) の要素、\(\varphi:A\rightarrow \Omega\) を真理値を定める射とすると
\[
\exists a:A [\varphi(a)] :\Leftrightarrow \forall w:\Omega[\forall a:A [\varphi(a) \Rightarrow w] \Rightarrow w]
\]
である。この関係式を元に射 \((\Rightarrow)\) のあるべき形を以下のように抽出することができる。
\[
\begin{align}
\exists a:A [\varphi(a)] \Leftrightarrow & \forall w:\Omega[\forall a:A [\varphi(a) \Rightarrow w] \Rightarrow w] \\
\exists a:A [\langle {\rm arrToEl}(\varphi),a \rangle {\sf \, ⨟ \,}{\rm ev}] \Leftrightarrow & \forall w:\Omega[\langle \forall a:A [\varphi(a) \Rightarrow w], w \rangle {\sf \, ⨟ \,} (\Rightarrow)] \\
{\rm arrToEl}(\varphi) {\sf \, ⨟ \,} \lambda[{\rm ev}] {\sf \, ⨟ \,} (\exists_A) \Leftrightarrow & \forall w:\Omega[\langle \forall a:A [\langle \langle {\rm arrToEl}(\varphi),a \rangle {\sf \, ⨟ \,}{\rm ev}, w \rangle {\sf \, ⨟ \,} (\Rightarrow)], w \rangle {\sf \, ⨟ \,} (\Rightarrow)] \\
{\rm arrToEl}(\varphi) {\sf \, ⨟ \,} \Omega^A {\sf \, ⨟ \,} (\exists_A) \Leftrightarrow & \forall w:\Omega[\langle \forall a:A [\langle \langle {\rm arrToEl}(\varphi), w \rangle , a \rangle {\sf \, ⨟ \,} \Delta {\sf \, ⨟ \,} ( (\langle {\rm prj}_1 {\sf \, ⨟ \,} {\rm prj}_1, {\rm prj}_2 \rangle {\sf \, ⨟ \,}{\rm ev}) \times ({\rm prj}_1 {\sf \, ⨟ \,} {\rm prj}_2) ) {\sf \, ⨟ \,} (\Rightarrow)], w \rangle {\sf \, ⨟ \,} (\Rightarrow)] \\
{\rm arrToEl}(\varphi) {\sf \, ⨟ \,} (\exists_A) \Leftrightarrow & \forall w:\Omega[\langle \langle {\rm arrToEl}(\varphi), w \rangle {\sf \, ⨟ \,} \lambda[\Delta {\sf \, ⨟ \,} ( (\langle {\rm prj}_1 {\sf \, ⨟ \,} {\rm prj}_1, {\rm prj}_2 \rangle {\sf \, ⨟ \,}{\rm ev}) \times ({\rm prj}_1 {\sf \, ⨟ \,} {\rm prj}_2) ) {\sf \, ⨟ \,} (\Rightarrow)] {\sf \, ⨟ \,} (\forall_A), w \rangle {\sf \, ⨟ \,} (\Rightarrow)] \\
{\rm arrToEl}(\varphi) {\sf \, ⨟ \,} (\exists_A) \Leftrightarrow & \forall w:\Omega[\langle {\rm arrToEl}(\varphi), w \rangle {\sf \, ⨟ \,} \Delta {\sf \, ⨟ \,} ( (\lambda[\Delta {\sf \, ⨟ \,} ( (\langle {\rm prj}_1 {\sf \, ⨟ \,} {\rm prj}_1, {\rm prj}_2 \rangle {\sf \, ⨟ \,}{\rm ev}) \times ({\rm prj}_1 {\sf \, ⨟ \,} {\rm prj}_2) ) {\sf \, ⨟ \,} (\Rightarrow)] {\sf \, ⨟ \,} (\forall_A)) \times {\rm prj}_2 ) {\sf \, ⨟ \,} (\Rightarrow)] \\
{\rm arrToEl}(\varphi) {\sf \, ⨟ \,} (\exists_A) \Leftrightarrow & {\rm arrToEl}(\varphi) {\sf \, ⨟ \,} \lambda[\Delta {\sf \, ⨟ \,} ( (\lambda[\Delta {\sf \, ⨟ \,} ( (\langle {\rm prj}_1 {\sf \, ⨟ \,} {\rm prj}_1, {\rm prj}_2 \rangle {\sf \, ⨟ \,}{\rm ev}) \times ({\rm prj}_1 {\sf \, ⨟ \,} {\rm prj}_2) ) {\sf \, ⨟ \,} (\Rightarrow)] {\sf \, ⨟ \,} (\forall_A)) \times {\rm prj}_2 ) {\sf \, ⨟ \,} (\Rightarrow)] {\sf \, ⨟ \,} (\forall_{\Omega}) \\
\end{align}
\]
まとめると、存在量化子 \((\exists_A):\Omega^A \rightarrow \Omega\) は次のように構成される。
\[
(\exists_A) := \lambda[\Delta {\sf \, ⨟ \,} ( (\lambda[\Delta {\sf \, ⨟ \,} ( (\langle {\rm prj}_1 {\sf \, ⨟ \,} {\rm prj}_1, {\rm prj}_2 \rangle {\sf \, ⨟ \,}{\rm ev}) \times ({\rm prj}_1 {\sf \, ⨟ \,} {\rm prj}_2) ) {\sf \, ⨟ \,} (\Rightarrow)] {\sf \, ⨟ \,} (\forall_A)) \times {\rm prj}_2 ) {\sf \, ⨟ \,} (\Rightarrow)] {\sf \, ⨟ \,} (\forall_{\Omega})
\]
余談
論理和や存在量化子が一見複雑なのは、トポスの定義に通常「全ての有限余極限が存在すること」を含めていないことが原因の一つとしてあるだろう。
ホモトピー型理論などで採用されるような「述語を型で表す」という方法においては「圏論的和が論理和」「圏論的積が論理積」というように圏論的に自然な操作が論理演算に直接的に用いられる。
一方トポス理論においては、極限の存在は公理的に認める一方で、始対象や圏論的和といった余極限の存在は「公理」として認めず、トポスの公理から得られる一つの「帰結」という扱いになる。
ホモトピー型理論などで採用されるような「述語を型で表す」という方法においては「圏論的和が論理和」「圏論的積が論理積」というように圏論的に自然な操作が論理演算に直接的に用いられる。
一方トポス理論においては、極限の存在は公理的に認める一方で、始対象や圏論的和といった余極限の存在は「公理」として認めず、トポスの公理から得られる一つの「帰結」という扱いになる。
ピースを組み合わせて論理式を組み立てる例
前節で、論理式のピースとなる論理演算子の構成が済んだため、それらを使って実際にどのようにして論理式が構成されるのかを具体的に紹介していく。
Dedekind 切断の判定
例の一つとして、Dedekind 切断であることを判定する述語 \({\rm isDedekindCut}:\Omega^{\mathbb{Q}} \times \Omega^{\mathbb{Q}} \rightarrow \Omega\) を明示的に構成していく。
便利のため幾つかのリンクは以下に貼っておくが、Dedekind 切断に関する解説については他サイトや教科書等を参照してほしい。
- Dedekind cut (nLab 記事)
- デデキント切断 (Wikipedia 記事)
まず、\(\langle L,U \rangle:1\rightarrow \Omega^{\mathbb{Q}} \times \Omega^{\mathbb{Q}}\) としたとき、その対が Dedekind 切断であるとは、以下の条件式を満たすことと同値である。
\[
\begin{align}
& \exists x:{\mathbb{Q}} [x\in L] \\
& \exists x:{\mathbb{Q}} [x\in U] \\
& \\
& \forall \langle a,b \rangle:{\mathbb{Q}} \times {\mathbb{Q}}[(a < b \wedge b\in L) \Rightarrow a\in L] \\
& \forall \langle a,b \rangle:{\mathbb{Q}} \times {\mathbb{Q}}[(a < b \wedge a\in U) \Rightarrow b\in U] \\
& \\
& \forall a:{\mathbb{Q}}[a\in L \Rightarrow \exists b:{\mathbb{Q}} [a < b \wedge b \in L]] \\
& \forall b:{\mathbb{Q}}[b\in U \Rightarrow \exists a:{\mathbb{Q}} [a < b \wedge a \in U]] \\
& \\
& \forall \langle a,b \rangle:{\mathbb{Q}} \times {\mathbb{Q}}[a < b \Rightarrow (a\in L \vee b\in U)] \\
& \forall \langle a,b \rangle:{\mathbb{Q}} \times {\mathbb{Q}}[(a\in L \wedge b\in U) \Rightarrow a < b] \\
& \end{align}
\]
余談
構成的数学 (constructive mathematics) を意識して、上の定義を採用している
これらの式は以下のように変形することができる。(// 不完全)
\[
\begin{align}
\langle L,U \rangle {\sf \, ⨟ \,} & ({\rm prj}_1 {\sf \, ⨟ \,} \lambda[\langle {\rm prj}_2, {\rm prj}_1 \rangle {\sf \, ⨟ \,} (\in)] {\sf \, ⨟ \,} (\exists_{{\mathbb{Q}}})) \\
\langle L,U \rangle {\sf \, ⨟ \,} & ({\rm prj}_2 {\sf \, ⨟ \,} \lambda[\langle {\rm prj}_2, {\rm prj}_1 \rangle {\sf \, ⨟ \,} (\in)] {\sf \, ⨟ \,} (\exists_{{\mathbb{Q}}})) \\
& \\
\langle L,U \rangle {\sf \, ⨟ \,} & ({\rm prj}_1 {\sf \, ⨟ \,} \lambda[\Delta {\sf \, ⨟ \,} ((\Delta {\sf \, ⨟ \,} (({\rm prj}_2 {\sf \, ⨟ \,} (<))\times(\Delta {\sf \, ⨟ \,} (({\rm prj}_2 {\sf \, ⨟ \,} {\rm prj}_2)\times {\rm prj}_1) {\sf \, ⨟ \,} (\in))) {\sf \, ⨟ \,} (\wedge))\times(\Delta {\sf \, ⨟ \,} (({\rm prj}_2 {\sf \, ⨟ \,} {\rm prj}_1)\times {\rm prj}_1) {\sf \, ⨟ \,} (\in))) {\sf \, ⨟ \,} (\Rightarrow)] {\sf \, ⨟ \,} (\forall_{{\mathbb{Q}} \times {\mathbb{Q}}})) \\
\langle L,U \rangle {\sf \, ⨟ \,} & ({\rm prj}_2 {\sf \, ⨟ \,} \lambda[\Delta {\sf \, ⨟ \,} ((\Delta {\sf \, ⨟ \,} (({\rm prj}_2 {\sf \, ⨟ \,} (<))\times(\Delta {\sf \, ⨟ \,} (({\rm prj}_2 {\sf \, ⨟ \,} {\rm prj}_1)\times {\rm prj}_1) {\sf \, ⨟ \,} (\in))) {\sf \, ⨟ \,} (\wedge))\times(\Delta {\sf \, ⨟ \,} (({\rm prj}_2 {\sf \, ⨟ \,} {\rm prj}_2)\times {\rm prj}_1) {\sf \, ⨟ \,} (\in))) {\sf \, ⨟ \,} (\Rightarrow)] {\sf \, ⨟ \,} (\forall_{{\mathbb{Q}} \times {\mathbb{Q}}})) \\
& \\
\langle L,U \rangle {\sf \, ⨟ \,} & ({\rm prj}_1 {\sf \, ⨟ \,} \lambda[\Delta {\sf \, ⨟ \,} ((\Delta {\sf \, ⨟ \,} ({\rm prj}_2 \times {\rm prj}_1))\times(\lambda[\Delta {\sf \, ⨟ \,} ((\Delta {\sf \, ⨟ \,} (({\rm prj}_1 {\sf \, ⨟ \,} {\rm prj}_2) \times {\rm prj}_2) {\sf \, ⨟ \,} (<))\times(\Delta {\sf \, ⨟ \,} ({\rm prj}_2 \times ({\rm prj}_1 {\sf \, ⨟ \,} {\rm prj}_1)) {\sf \, ⨟ \,} (\in))) {\sf \, ⨟ \,} (\wedge)] {\sf \, ⨟ \,} (\exists_{{\mathbb{Q}}}))) {\sf \, ⨟ \,} (\Rightarrow)] {\sf \, ⨟ \,} (\forall_{{\mathbb{Q}}})) \\
\langle L,U \rangle {\sf \, ⨟ \,} & ({\rm prj}_2 {\sf \, ⨟ \,} \lambda[\Delta {\sf \, ⨟ \,} ((\Delta {\sf \, ⨟ \,} ({\rm prj}_2 \times {\rm prj}_1))\times(\lambda[\Delta {\sf \, ⨟ \,} ((\Delta {\sf \, ⨟ \,} ({\rm prj}_2 \times ({\rm prj}_1 {\sf \, ⨟ \,} {\rm prj}_2)) {\sf \, ⨟ \,} (<))\times(\Delta {\sf \, ⨟ \,} ({\rm prj}_2 \times ({\rm prj}_1 {\sf \, ⨟ \,} {\rm prj}_1)) {\sf \, ⨟ \,} (\in))) {\sf \, ⨟ \,} (\wedge)] {\sf \, ⨟ \,} (\exists_{{\mathbb{Q}}}))) {\sf \, ⨟ \,} (\Rightarrow)] {\sf \, ⨟ \,} (\forall_{{\mathbb{Q}}})) \\
\end{align}
\]
よって Dedekind 切断か否かを判定する論理式 \(\Omega^{\mathbb{Q}} \times \Omega^{\mathbb{Q}} \rightarrow \Omega\) はトポス理論的には次のようにして構成できることになる。
\[
{\rm isDedekindCut} := \Delta {\sf \, ⨟ \,} ({\rm prj}_1 {\sf \, ⨟ \,} \lambda[\langle {\rm prj}_2, {\rm prj}_1 \rangle {\sf \, ⨟ \,} (\in)] {\sf \, ⨟ \,} (\exists_{{\mathbb{Q}}}))\times(\Delta {\sf \, ⨟ \,} ({\rm prj}_2 {\sf \, ⨟ \,} \lambda[\langle {\rm prj}_2, {\rm prj}_1 \rangle {\sf \, ⨟ \,} (\in)] {\sf \, ⨟ \,} (\exists_{{\mathbb{Q}}}))\times(\Delta {\sf \, ⨟ \,} ({\rm prj}_1 {\sf \, ⨟ \,} \lambda[\Delta {\sf \, ⨟ \,} ((\Delta {\sf \, ⨟ \,} (({\rm prj}_2 {\sf \, ⨟ \,} (<))\times(\Delta {\sf \, ⨟ \,} (({\rm prj}_2 {\sf \, ⨟ \,} {\rm prj}_2)\times {\rm prj}_1) {\sf \, ⨟ \,} (\in))) {\sf \, ⨟ \,} (\wedge))\times(\Delta {\sf \, ⨟ \,} (({\rm prj}_2 {\sf \, ⨟ \,} {\rm prj}_1)\times {\rm prj}_1) {\sf \, ⨟ \,} (\in))) {\sf \, ⨟ \,} (\Rightarrow)] {\sf \, ⨟ \,} (\forall_{{\mathbb{Q}} \times {\mathbb{Q}}}))\times(\Delta {\sf \, ⨟ \,} ({\rm prj}_2 {\sf \, ⨟ \,} \lambda[\Delta {\sf \, ⨟ \,} ((\Delta {\sf \, ⨟ \,} (({\rm prj}_2 {\sf \, ⨟ \,} (<))\times(\Delta {\sf \, ⨟ \,} (({\rm prj}_2 {\sf \, ⨟ \,} {\rm prj}_1)\times {\rm prj}_1) {\sf \, ⨟ \,} (\in))) {\sf \, ⨟ \,} (\wedge))\times(\Delta {\sf \, ⨟ \,} (({\rm prj}_2 {\sf \, ⨟ \,} {\rm prj}_2)\times {\rm prj}_1) {\sf \, ⨟ \,} (\in))) {\sf \, ⨟ \,} (\Rightarrow)] {\sf \, ⨟ \,} (\forall_{{\mathbb{Q}} \times {\mathbb{Q}}}))\times(\Delta {\sf \, ⨟ \,} ({\rm prj}_1 {\sf \, ⨟ \,} \lambda[\Delta {\sf \, ⨟ \,} ((\Delta {\sf \, ⨟ \,} ({\rm prj}_2 \times {\rm prj}_1))\times(\lambda[\Delta {\sf \, ⨟ \,} ((\Delta {\sf \, ⨟ \,} (({\rm prj}_1 {\sf \, ⨟ \,} {\rm prj}_2) \times {\rm prj}_2) {\sf \, ⨟ \,} (<))\times(\Delta {\sf \, ⨟ \,} ({\rm prj}_2 \times ({\rm prj}_1 {\sf \, ⨟ \,} {\rm prj}_1)) {\sf \, ⨟ \,} (\in))) {\sf \, ⨟ \,} (\wedge)] {\sf \, ⨟ \,} (\exists_{{\mathbb{Q}}}))) {\sf \, ⨟ \,} (\Rightarrow)] {\sf \, ⨟ \,} (\forall_{{\mathbb{Q}}}))\times({\rm prj}_2 {\sf \, ⨟ \,} \lambda[\Delta {\sf \, ⨟ \,} ((\Delta {\sf \, ⨟ \,} ({\rm prj}_2 \times {\rm prj}_1))\times(\lambda[\Delta {\sf \, ⨟ \,} ((\Delta {\sf \, ⨟ \,} ({\rm prj}_2 \times ({\rm prj}_1 {\sf \, ⨟ \,} {\rm prj}_2)) {\sf \, ⨟ \,} (<))\times(\Delta {\sf \, ⨟ \,} ({\rm prj}_2 \times ({\rm prj}_1 {\sf \, ⨟ \,} {\rm prj}_1)) {\sf \, ⨟ \,} (\in))) {\sf \, ⨟ \,} (\wedge)] {\sf \, ⨟ \,} (\exists_{{\mathbb{Q}}}))) {\sf \, ⨟ \,} (\Rightarrow)] {\sf \, ⨟ \,} (\forall_{{\mathbb{Q}}})) {\sf \, ⨟ \,} (\wedge)) {\sf \, ⨟ \,} (\wedge)) {\sf \, ⨟ \,} (\wedge)) {\sf \, ⨟ \,} (\wedge)) {\sf \, ⨟ \,} (\wedge)
\]
{x∈X|P(x)} を構成する例
実数対象の土台となる部分対象を構成する
\(X\) の部分対象
\[
\{ x:\Omega^{\mathbb{Q}} \times \Omega^{\mathbb{Q}} \:|\: {\rm isDedekindCut}(x) \}
\]
の構造は、部分対象分類子 \({\rm true}\) の \({\rm isDedekindCut}\) に沿った引き戻しから得ることができる。
この部分集合 \(\langle {\mathbb{R}}, {\rm isDedekindCut}^{-1}({\rm true}) \rangle\) が構成できれば、その部分集合が持つ \(\Omega^{\mathbb{Q}} \times \Omega^{\mathbb{Q}}\) へのモニック射 \({\rm isDedekindCut}^{-1}({\rm true})\) を上手く使って実数の演算構造や順序構造を厳密に組み立てることができ、それらから実数対象 (real numbers object) を得ることができる。
また実数対象の厳密な定義については以下を参照。
- real numbers object (nLab 記事)
信憑性を疑う場合...
ここで説明している内容と似たような説明 (特に、論理式に相当する射に沿った部分対象分類子の引き戻しとして、Set-builder notation で書かれるような部分集合が構成されるという部分) は nLab の Kripke-Joyal の意味論 (Kripke-Joyal semantics) の記事にも掲載されているので、興味があればそのページも参考にしてほしい。
- Kripke-Joyal semantics (nLab 記事)
また、推論規則については、nLab のシークエント計算の記事が参考になるかもしれない。
- sequent calculus (nLab 記事)
タグ一覧: