import FormalLab.LogicAndComputation.ToposesAndCategoricalLogic /-! # 第81章：トポスの内部論理——部分対象・量化・局所的真理を読む 部分対象分類子は各対象上の述語を真理値への射として表します。しかし、これだけでは論理結合子、量化、高階述語が 圏のどの構造から生じるか、層の局所的な真理を外部からどう読めばよいかはまだ分かりません。 本章では**内部論理**（internal logic）を、圏の対象と射によって解釈される論理として扱います。まず冪対象が 述語族を分類することをLeanで確かめ、部分対象のHeyting構造と再添字付けの左右随伴としての量化へ進みます。 さらにKripke–Joyal意味論と、幾何学的射が保存する論理を調べます。外部のメタ理論が古典的であることと、対象トポスの内部論理がBooleanである ことを厳格に区別します。 ## 冪対象は部分対象を族として分類する 初等トポスで対象 `A` を固定すると、指数対象 $$ P(A):=\Omega^A. $$ を冪対象（power object）と呼びます。カリー化と部分対象分類を続けると $$ \operatorname{Hom}(X,\Omega^A) \cong\operatorname{Hom}(A\times X,\Omega) \cong\operatorname{Sub}(A\times X). $$ を得ます。従って射 `X→P(A)` は、`X` によって添字付けられた `A` の部分対象族を分類します。 -/ namespace FormalLab.LogicAndComputation.ToposInternalLogic open _root_.CategoryTheory open _root_.CategoryTheory.Limits open _root_.CategoryTheory.MonoidalCategory open _root_.CategoryTheory.MonoidalClosed open scoped MonoidalCategory universe uE vE noncomputable section variable {E : Type uE} [Category.{vE} E] variable (𝒞 : Subobject.Classifier E) section PowerObjects variable [CartesianMonoidalCategory E] [MonoidalClosed E] def powerObject (A : E) : E := (ihom A).obj 𝒞.Ω example {A X : E} : (A ⊗ X ⟶ 𝒞.Ω) ≃ (X ⟶ powerObject 𝒞 A) := (ihom.adjunction A).homEquiv X 𝒞.Ω def membershipCharacteristic (A : E) : A ⊗ powerObject 𝒞 A ⟶ 𝒞.Ω := (ihom.ev A).app 𝒞.Ω end PowerObjects /-! `membershipCharacteristic` の真の引戻しが、内部の所属関係 `∈_A↪A×P(A)` です。集合論の冪集合を要素の集まりとして 先に作るのではなく、全ての部分対象族を自然に分類する対象として特徴づけています。 `P(A)` をLeanの型 `Set A = A→Prop` と同一視できるのは `Type` の具体例です。一般のトポスでは冪対象も圏内の 対象であり、その外部の大域要素だけで全ての内部部分対象族を観測できるとは限りません。 -/ /-! ## 部分対象は内部のHeyting論理をなす 対象 `Γ` を文脈と読むと、その部分対象 `P↪Γ` は自由変数 `Γ` を持つ述語です。有限極限により、部分対象の共通部分 が連言、最大部分対象が真になります。部分対象分類子とデカルト閉性を用いると、含意と否定を含むHeyting代数構造が 得られます。 $$ P\land Q=\text{引戻しによる共通部分}, \quad P\Rightarrow Q=\max\{R\mid R\land P\le Q\}, \quad\neg P=P\Rightarrow\bot. $$ Heyting代数では `P∨¬P=⊤` は一般には成立しません。全ての部分対象について排中律が成り立つトポスをBooleanトポスと 呼びます。Boolean性は初等トポスの公理ではなく追加条件です。外部のLeanで古典論理を使って証明を行っても、対象と しているトポスの内部論理が自動的にBooleanになるわけではありません。 ## 量化は再添字付けの随伴である 射 `f:Δ→Γ` に沿う述語の代入は、部分対象の引戻し $$ f^*:\operatorname{Sub}(\Gamma)\longrightarrow\operatorname{Sub}(\Delta) $$ です。適切な像と依存積を使うと、左随伴と右随伴 $$ \exists_f\dashv f^*\dashv\forall_f. $$ を得ます。射影 `π:Γ×A→Γ` の場合、これらが変数 `a:A` に関する存在量化と全称量化です。第73章の型族における `Σ_f⊣f⁎⊣Π_f` と同じ随伴形が、ここでは部分対象上の論理演算として現れます。 等式述語は対角射 `A→A×A` が表す部分対象です。項の代入は射の合成、述語の代入は引戻し、量化はその左右の随伴に なります。圏論的論理では、推論規則を対象と射の普遍性として読み替えます。 ## 高階性は冪対象と指数対象から生じる `P(A)=Ω^A` があるため、述語そのものを変数として量化できます。関数対象 `B^A` も圏内にあるので、高階関数と 高階述語を内部言語で扱えます。このため初等トポスは直観主義高階論理のモデルになります。 ただし「集合論の全公理が自動的に成り立つ」という意味ではありません。自然数対象がなければ内部自然数論を標準的な 形で解釈できず、選択公理や排中律も一般には成立しません。サイズを越えて「全ての対象の対象」を作る操作も トポス公理にはありません。どの内部理論を解釈するかに応じて追加構造を明示します。 -/ /-! ## Kripke–Joyal意味論は局所的な真理を読む 層トポスの内部式を外部から読む方法がKripke–Joyal意味論です。対象 `U` を段階または局所的文脈とし、 `U ⊩ φ` を「`U` 上で `φ` が成り立つ」と読みます。射 `V→U` に沿って真理は制限されます。 連言は同じ段階で両方が成り立つこと、含意は全ての制限段階で前件から後件が従うこととして読まれます。層の Grothendieck位相では、選言や存在量化が被覆上で局所的に証明されれば全体で強制される場合があります。従って `U⊩∃x,φ(x)` から、外部で一つの大域要素 `x` を選べるとは限りません。局所証人と大域証人を区別します。 この意味論は内部言語の定義そのものではなく、内部判断をサイト上の外部条件へ翻訳するforcing意味論です。同じ トポスに異なるサイト表示があり得るので、内部真理を特定のサイトの構文へ同一視しません。 ## 幾何学的射は論理の保存範囲を示す トポス `E,F` の間の幾何学的射 `f:E→F` は、関手の随伴 $$ f^*:\mathcal F\rightleftarrows\mathcal E:f_*. $$ で、逆像関手 `f⁎` が有限極限を保存するものです。空間の連続写像が層の逆像・直像を誘導する向きに合わせ、 幾何学的射の向きは右随伴 `f₊` の向きで記します。 有限連言、任意選言、存在量化から作る幾何学的論理は、逆像関手によって保存されます。全称量化や含意は一般の 幾何学的射で同じようには保存されません。この保存範囲は、どの公理がモデルの逆像に安定かを判定する基準になります。 トポスの点は `Type` または集合のトポスからそのトポスへの幾何学的射です。空間の点に対応する例がありますが、 全てのトポスが真理を判定するのに十分な点を持つとは限りません。点で全てを検査できるという集合論的直観を 無条件に持ち込みません。 ## 現行mathlibが形式化する境界 mathlibの `Subobject.Classifier E` は分類子のデータ、`HasSubobjectClassifier E` はその存在を表します。 `Classifier.representableBy` は部分対象前層の表現可能性を与えます。`Presheaf.classifier C` は篩前層を分類子として 構成し、`Sheaf.classifier J` は `J`-閉篩の層を分類子として構成します。 本章で述べた論理の全体系を、これら数個の宣言だけで形式化したわけではありません。そこにはHeyting代数、 量化随伴、内部言語、Kripke–Joyal意味論、幾何学的射が含まれます。現行APIでは初等トポスの構成要素を 複数の型クラスとして扱います。Leanで 分類正方形が検査されたことと、特定の内部理論の健全性・完全性が全て証明されたことを区別します。 ## 要点 * 冪対象 `Ω^A` は `A` の部分対象族を分類し、内部の高階述語を表す。 * 初等トポスの部分対象はHeyting論理をなし、排中律が成り立つBoolean性は追加条件である。 * 述語の代入は引戻し、存在量化と全称量化はその左随伴と右随伴として解釈される。 * Kripke–Joyal意味論では層トポスの内部判断を段階と被覆に関する外部条件へ翻訳する。 * 幾何学的射の逆像が保存する論理と、一般には保存しない含意・全称量化を区別する。 ## 研究史と文献案内 Lawvere [LAW70] は量化を随伴として扱い、層と論理の関係を明示した初等トポス形成期の一次資料です。講演は1970年、 会議録の刊行は1971年なので両年を区別します。Tierney [TIE72] は初等トポスと層意味論を集合論の独立性へ応用した 一次資料です。Kripke–Joyal意味論とLawvere–Tierney位相には [MM92] を参照してください。同書は初等トポスと Grothendieckトポスも比較しています。現行Lean APIには [MATHLIB] を参照してください。 ## 問題 ### 冪対象の所属関係から部分対象族を回収する 射 `p:X→Ω^A` を逆カリー化して `A×X→Ω` を作り、`truth` の引戻しとして部分対象 `R↪A×X` を構成してください。 逆に任意の `R↪A×X` の特性射をカリー化して `X→Ω^A` を得ます。二構成が互いに逆であることをβη則と分類子の 一意性へ分解し、`Hom(X,Ω^A)≃Sub(A×X)` の自然性まで示せば完了です。 ### 排中律が失敗する局所的な真理値を調べる 位相空間の開集合の層トポスを一つ選び、真理値を開集合として読む具体例を構成してください。開集合 `U` のHeyting否定が `int(X∖U)` になることを確認し、`U∪int(X∖U)` が全空間にならない例を与えます。外部の集合論では各点が `U` に 入るか否かを判定できても、内部の排中律が従わない理由を局所性と開性から説明できれば完了です。 ### 二種類のトポスと保存される論理を比較する 有限集合の圏が有限極限、指数対象、部分対象分類子を持つことを示し、無限余積を持たないためGrothendieckトポスでは ないことを証明してください。次に一つの前層トポスが任意の小極限・小余極限を対象ごとに持つことを確認します。 最後に幾何学的射の逆像が有限連言・任意選言・存在量化を保存する理由を、有限極限保存と左随伴性へ対応させれば 完了です。 -/ end end FormalLab.LogicAndComputation.ToposInternalLogic