--- title: "構造" module: FOL.ZFStructure lang: ja site: "Bedrock" description: "構造" stage: "一階論理" reading_order: 7 canonical: https://bedrock.institute/ja/FOL.ZFStructure.html html: FOL.ZFStructure.html agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/FOL/ZFStructure.lagda.md prerequisites: [Base.Prelude] routes: [common-foundations] translations: [https://bedrock.institute/en/FOL.ZFStructure.md, https://bedrock.institute/zh/FOL.ZFStructure.md] agent_guide: /llms.txt license: CC-BY-NC-SA-4.0 --- # 構造 集合についての一階言語には、等号と所属という二つの原始述語があります。これを解釈するには、変数が何を渡り歩くかを定め、その二つの述語がそこで何を意味するかを指定しなければなりません。`ZFStructure` はまさにこのデータをまとめます。すなわち「集合」からなる台と、等号と所属の命題値の解釈です。レコードが要求するのは台が h-集合であることだけで、ZF の公理は組み込まれていません。 二つの関係はどちらも `hProp` に値を取るので、各原子文には証明を要素とする基礎型があります。台の上のクラスは、それによってより小さな構造を切り出すのに使えます。`Transitive` はクラスの要素の要素が再びそのクラスに属することを表し、制限 `𝒮 ↾ M` はクラスを依存対からなる新しい構造の台に変えます。所属の各ファイバーが命題であるため、この対の台は再び h-集合であり、第一射影の等しさだけで対全体の等しさが定まります。 全章を通して三つの所属の記法を区別しなければなりません。ホストレベルのクラス所属 `∈ᶜ` は、台の要素が述語 `M` を満たすかを調べます。構造の所属 `∈ˢ` は命題に値を持つフィールドです。そして「対象言語」の章の構文にある対象言語の所属記号 `∈̇` は、構造が解釈を与えて初めて意味を持ちます。 所属は三つの異なる層に現れ、記法がそれらを区別します。ホストレベルでは、クラスは `hProp` 値の述語 `M` であり、`x ∈ᶜ M` は基底の命題 `⟨ M x ⟩`、つまり `x` が述語を満たすことを証拠立てる型です。これは台の要素と述語の間の関係であって、二つの集合の間の関係ではありません。構造レベルでは、`x ∈ˢ y` が二つの台の要素についての命題です。対象レベルは「対象言語」の章の構文に属し、そこの `∈̇` は解釈を待つ単なる記号です。 ```agda {-# OPTIONS --cubical --safe --guardedness #-} module FOL.ZFStructure where open import Base.Prelude ``` 構造の関係は命題なので、その基礎型を証明によって満たせます。クラスを満たす台の要素を集めると、依存対の型が得られます。台 `S` が h-集合でも、そのような対の型が h-集合になるとは限りません。これを保証するのは、各ファイバー、すなわち固定した要素での所属の証拠が命題であることで、異なる二組の証拠が本来等しいはずの対を引き裂くことはありません。 ```agda open import Cubical.Foundations.HLevels using ( isSetΣSndProp ) ``` したがって、構造をクラスへ制限することは、依存対に関する一般的な原理に依拠します。対は第一射影と、その型が第一射影に依存する第二成分からなります。第二成分が命題値であれば、等しさに関して対が第一射影を超える情報を持つことはありません。つまり `fst a ≡ fst b` なら、すでに `a ≡ b` です。本章は最後に補題 `↾-reflects` で、制限された台についてのこの向きを記録します。 ```agda open import Cubical.Data.Sigma using ( Σ≡Prop ) ``` ## 構造の record 集合の等号は、ホストのパス等式をそのまま使わず、なぜフィールドとして与えるのでしょうか。集合論の言語は `=` と `∈` を原始記号として扱い、構造とはそれらの意味の選択にほかなりません。二つの台の要素は、ホスト型の要素としては異なっていても、構造には等しいとされることがあります。`≈ˢ` と `∈ˢ` を命題値のフィールドにすることで、構造が実際に与えるデータを正確に表します。このレコードは二つの関係の間にいかなる整合性の法則も課しません。 約束は本書全体で共通です。筆記体の `𝒮` は構造を、`S` はその台を、`x`、`y`、`z` は台の要素、すなわちこの言語が語る「集合」を表します。上付きの `ˢ` は、その記号が**当該構造のフィールド**であることの印で、紙面上の所属記号の族はすでに一字一層に分かれています。ライブラリの `∈` がホストを、`∈ˢ` が構造を、対象言語の `∈̇` が構文を表します。 このレコードは、あえて素のモデル論的データだけを記録します。台が h-集合であることを要求し、二つの真理値関係を与えますが、外延性や正則性、その他の ZF 公理は一切主張しません。それらは後のモデル諸章に属し、そこでモデルのさらなるフィールドとして現れます。 台 `S` はレベル `ℓ` の通常の型で、フィールド `isSetS` はそれが h-集合であること、つまり等式の型がすべて命題であることを要求します。これが、この言語の「集合」となりうるものに対する唯一の制約です。二つの関係フィールドは `hProp ℓ` に値を取ります。`S : Type ℓ` と `hProp ℓ` はどちらも一つ上の宇宙に住むため、レコード全体の型は `Type (ℓ-suc ℓ)` です。 ```agda record ZFStructure (ℓ : Level) : Type (ℓ-suc ℓ) where field S : Type ℓ isSetS : isSet S ``` 二つの関係フィールドは構造の等号 `≈ˢ` と所属 `∈ˢ` を与え、いずれも `S → S → hProp ℓ` 型の関数です。したがって `x ∈ˢ y` は二つの台の要素についての命題です。レコードはここで終わり、台と二つの関係がデータ、h-集合性が制約であり、集合論の公理は課されません。 ```agda _≈ˢ_ _∈ˢ_ : S → S → hProp ℓ infix 20 _≈ˢ_ _∈ˢ_ ``` 構造の等号 `≈ˢ` は、ホスト言語のパス等式ではなくフィールドです。したがって、任意の構造は等号と所属についてそれぞれ真理値を返す解釈を与えますが、レコードは整合性の法則を課しません。 ## 命題として読む 構造の所属を表す各命題には基礎型があります。記法 `x ∈ᵗ y` は、ちょうど `⟨ x ∈ˢ y ⟩` を表します。この Type 値の読み方により、後続の定義は所属の証明を使い、クラスの要素を依存対に集められます。モジュール `hPropStructure` は構造のフィールドの上にこの記法を追加します。 `x ∈ᵗ y` は基礎型 `⟨ x ∈ˢ y ⟩` と定義され、`Type ℓ` に属します。これは新しい関係ではなく、既存の所属命題を Type として読むものです。引数の向きはこれまでの記法と一致し、`x ∈ᵗ y` は「x は y の要素である」と読みます。 ```agda module hPropStructure {ℓ} (𝒮 : ZFStructure ℓ) where open ZFStructure 𝒮 public _∈ᵗ_ : S → S → Type ℓ x ∈ᵗ y = ⟨ x ∈ˢ y ⟩ ``` つまり `y ∈ᵗ x` は、命題値の構造において y が x の要素であることを述べます。この型の要素は、所属の真理値が成り立つことの証拠です。 ```agda infix 20 _∈ᵗ_ ``` ## 推移的クラス 所属が Type 値の命題として使えるようになると、台の上のクラスは要素を一つずつ論じられる対象になります。クラス `M` は、`M` の要素のすべての要素が再び `M` に属するとき、**推移的**であるといいます。これは集合論の推移性の概念を、利用できる二つの所属関係で述べたものです。含意の左には構造の `∈ᵗ` を、クラスそのものへの所属にはホストレベルの `∈ᶜ` を用います。 `Transitive` は命題値の構造 `𝒮` とクラス `M : S → hProp ℓ` を受け取り、含意 `y ∈ᵗ x → x ∈ᶜ M → y ∈ᶜ M` を述べます。構造において y が x の要素であり、x がクラス `M` に属するなら、y も `M` に属する、というものです。向きとしては要素の要素についての閉性であって、部分集合についての閉性ではありません。定義は台の要素 `x`、`y` を暗黙に量化し、この含意以外は何も主張しません。 ```agda Transitive : ∀ {ℓ} (𝒮 : ZFStructure ℓ) → (ZFStructure.S 𝒮 → hProp ℓ) → Type ℓ Transitive 𝒮 M = ∀ {x y} → y ∈ᵗ x → x ∈ᶜ M → y ∈ᶜ M where open hPropStructure 𝒮 ``` ## 部分構造 命題値のクラス `M` が与えられれば、台のうち `M` を満たす部分へ構造を切り詰められます。制限 `𝒮 ↾ M` は再び `ZFStructure` であり、その台は依存対 `(x , proof)` の型です。ここで `x : S` かつ `proof : x ∈ᶜ M` です。制限された要素に対する等号と所属は `𝒮` から受け継がれます。どちらの関係も第一射影だけを見て、そこに元の関係を適用します。変わるのは構造の要素の範囲であって、`M` を表す集合を構成するのでも、構文や定数域をそれ自体で固定するのでもありません。 新しい台は Σ 型 `Σ[ x ∈ S ] (x ∈ᶜ M)` です。その要素は「元となる台の要素と `M` への所属の証拠」の対であり、したがって制限は `M` を集合に集めるのではなく、どの対を要素とみなすかを変えるだけです。レコードの `isSetS` フィールドは依然として埋める必要があり、ここで章の冒頭のファイバーごとの事実が働きます。各 `M x` は第二成分によって命題なので、`isSetS` に `isSetΣSndProp` を適用すれば、この対の型が再び h-集合であることが示されます。 ```agda _↾_ : ∀ {ℓ} (𝒮 : ZFStructure ℓ) → (ZFStructure.S 𝒮 → hProp ℓ) → ZFStructure ℓ _↾_ {ℓ} 𝒮 M = record { S = Σ[ x ∈ S ] (x ∈ᶜ M) ; isSetS = isSetΣSndProp isSetS (λ x → (M x) .snd) ``` どちらの関係フィールドも、元の関係を第一射影に沿って引き戻します。制限された要素 `a`、`b` に対して、構造は `fst a ≈ˢ fst b` と `fst a ∈ˢ fst b` を評価します。したがって、制限された要素の間の所属も等号も、もっぱら基底の台の要素の上で評価され、対が第二成分に持つ証拠はこの二つの関係に何の役割も果たしません。 ```agda ; _≈ˢ_ = λ a b → fst a ≈ˢ fst b ; _∈ˢ_ = λ a b → fst a ∈ˢ fst b } where open ZFStructure 𝒮 infixl 21 _↾_ ``` `𝒮 ↾ M` の関係は第二成分を無視します。そこで、制限された台は第一射影を超えて対を区別できるのか、と問えるでしょう。できません。各所属の型 `M x` が命題であるため、第一射影の間のパスが依存対全体の間のパスを定めます。次の補題はこの向きを記録します。 `↾-reflects` の型は `fst a ≡ fst b → a ≡ b` です。族 `λ x → (M x) .snd` とともに `Σ≡Prop` を適用します。この族は各点で、`x` での所属の証拠が命題値であることを示すものであり、対の間のパスは第一射影の間のパスだけから組み立てられます。補題が述べるのはこの一方向だけです。基底の要素の等しさが制限された要素の等しさとして反映されることであり、逆については何も主張しません。 ```agda ↾-reflects : ∀ {ℓ} {𝒮 : ZFStructure ℓ} {M : ZFStructure.S 𝒮 → hProp ℓ} {a b : ZFStructure.S (𝒮 ↾ M)} → fst a ≡ fst b → a ≡ b ↾-reflects {M = M} = Σ≡Prop (λ x → (M x) .snd) ``` ## まとめ `ZFStructure` は、台、その h-集合性の証明、等号と所属の真理値による解釈という四つのフィールドを記録し、ZF の公理は含みません。命題値の構造では、`∈ᵗ` が所属の基礎型を与え、`Transitive` が要素の要素についての閉性を述べ、`𝒮 ↾ M` が台を依存対からなるクラスへ制限します。`↾-reflects` は、第一射影の等しさを制限された台の等しさへ持ち上げます。次の段階は、このような構造の中で対象言語の論理式そのものを解釈することです。