---
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: https://bedrock.institute/llms.txt
license: "CC-BY-NC-SA-4.0"
---


```agda
{-# OPTIONS --cubical --safe --guardedness #-}
module FOL.ZFStructure where
```

# 構造

```agda
open import Base.Prelude
```

前章では集合についてどのような主張を書けるかを定めたが、その主張がいつ成り立つかはまだ決めていない。書かれた主張の意味を定めるには、そこで指す対象の範囲と、二つの基本的な関係、すなわち対象どうしの等しさと所属をどう判定するかを選ぶ必要がある。その選択を与えるのが**構造**である。

本章ではまず構造に必要なデータを定め、続いて、ある性質を満たす対象だけに制限した構造を作る。ここでは集合論の公理を仮定しない。

## 台と関係

対象言語の `t ≐ u` と `t ∈̇ u` は論理式であり、まだ証明できる命題ではない。その意味を定めるには、対象の型 `S` と、その上の二つの関係を選ぶ。得られる構造を `𝒮`、その**台** `S` の元を `x`、`y` と書く。上付きの `ˢ` は、関係が構造 `𝒮` から与えられることを示す。

等号の関係まで別に与え、Agda のパス等式 `x ≡ y` をそのまま使わないのはなぜか。対象言語の等号には独自の解釈が必要だからである。パス `x ≡ y` が与えられていなくても、フィールド `x ≈ˢ y` は真理値を与えられる。この段階では単なる二項関係であり、等号の法則も、所属との整合性もまだ要求しない。

**定義** (`ZFStructure`) 台がレベル `ℓ` にあるとき、このレコードは真理値の型 `Ω` を引数に取る。フィールドは台 `S : Type ℓ`、`S` が h-集合である証明、および等号と所属を解釈する二つの `S → S → Ω` 型の関係である。`Ω` のレベルは `ℓ` と一致しなくてもよい。基礎となる定義をこのように一般的に保ち、具体的な真理値は別に選ぶ。この時点で二つの関係には法則を課さない。

```agda
record ZFStructure (ℓ : Level) {ℓΩ : Level} (Ω : Type ℓΩ)
  : Type (ℓ-max (ℓ-suc ℓ) ℓΩ) where
  field
    S         : Type ℓ
    isSetS    : isSet S
```

残る二つのフィールドは、台の元の組ごとに真理値を与える。`x ∈ˢ y` の値は `Ω` に属するが、前章の `t ∈̇ u` はまだ構文にすぎない。このレコードは、項が台の元をどう指すかも、二つの関係が集合論の公理を満たすかどうかも定めない。

```agda
    _≈ˢ_ _∈ˢ_ : S → S → Ω

  infix 20 _≈ˢ_ _∈ˢ_
```

**定義** (`ZFStructureₕ`) 以下で使う命題値の構造では、真理値の型 Ω に `hProp ℓ` を選ぶ。添字 `ₕ` は台のレベルでこの選択を表し、別のレコードを導入しない。

```agda
ZFStructureₕ : (ℓ : Level) → Type (ℓ-suc ℓ)
ZFStructureₕ ℓ = ZFStructure ℓ (hProp ℓ)
```

`ZFStructure` という名前は解釈する記号が集合論の言語に属することを示すのであって、すでに ZF のモデルであるという意味ではない。たとえば自然数を台とし、通常の大小関係を所属のフィールドに入れても、ここで必要なデータはそろう。しかしそれだけで ZF の公理が証明されるわけではない。

## 命題値の構造

`ZFStructureₕ` では、フィールド `x ∈ˢ y` は `hProp`、すなわち命題とその証明無関係性を返す。その命題の証明を関数の引数として使うには、基礎となる型 `⟨ x ∈ˢ y ⟩` を取り出す。部分モジュール `hPropView` は構造 `𝒮` を固定し、この型を `x ∈ᵗ y` と書けるようにする。

<details open class="submodule-fold">
<summary class="submodule-fold-heading">

```agda
module hPropView {ℓ} (𝒮 : ZFStructureₕ ℓ) where
```

</summary>
<div class="submodule-fold-content">

まず `public` を付けて `ZFStructure 𝒮` を開き、`hPropView` が `𝒮` における `ZFStructure` の全フィールドを「継承」するようにする。これらのフィールドは部分モジュール内で使えるだけでなく、このビューを開くモジュールにも公開される。新しい構造を作るわけではない。

```agda
  open ZFStructure 𝒮 public
```

`y ∈ᵗ x` の元は、この構造で `y` が `x` に属することの証明である。`∈ˢ` と同じく左側が所属する元であり、二つの記法の結び付きの強さも同じにする。

**定義** (`_∈ᵗ_`) 台の元 `x`、`y` に対し、`x ∈ᵗ y` を `x ∈ˢ y` の基礎型と定める。

```agda
  infix 20 _∈ᵗ_
  _∈ᵗ_ : S → S → Type ℓ
  x ∈ᵗ y = ⟨ x ∈ˢ y ⟩
```

### 推移的クラス

クラス `M` が台の元をいくつか選ぶとする。選ばれた `x` に、構造の所属関係によって `y` が属するなら、`y` も選ばれるだろうか。常にそうなるクラスを**推移的クラス**という。これは*要素*についての閉性であり、部分集合についての閉性ではない。

推移性はクラスに課す閉性の条件であり、構造のフィールドではない。所属の証明の型を使うため、命題値の構造を固定した `hPropView` の中に置く。

**定義** (`Transitive`) 命題値の構造 `𝒮` とクラス `M` に対し、推移性とは、任意の台の元 `x`、`y` について、`y ∈ᵗ x` と `x ∈ᶜ M` の証明から `y ∈ᶜ M` の証明を与えることである。コードでは `x`、`y` を暗黙に量化する。

```agda
  Transitive : (S → hProp ℓ) → Type ℓ
  Transitive M = ∀ {x y} → y ∈ᵗ x → x ∈ᶜ M → y ∈ᶜ M
```

</div>
</details>

よく似た所属の記法にも、それぞれ異なる役割がある。特にクラスは述語 `M : S → hProp ℓ` である。したがって `x ∈ᶜ M` は元がその述語を満たすかを問い、台の二つの元を比較するものではない。

| 記法 | 関係するもの | 得られるもの |
| --- | --- | --- |
| `t ∈̇ u` | 二つの項 | まだ真理値を与えていない論理式 |
| `x ∈ˢ y` | 二つの台の元 | `hProp ℓ` の命題 |
| `x ∈ᵗ y` | 同じ二つの元 | `x ∈ˢ y` の基礎となる証明の型 |
| `x ∈ᶜ M` | 元とクラス | `M x` の基礎となる証明の型 |
: 四つの所属記法とそれぞれの役割

## 部分構造

変数が `M` に選ばれた元だけを動くようにするには、台を作り直す必要がある。元の型 `S` を残して横に `M` を添えるだけでは、`S` 型の変数は選ばれなかった元も指せてしまう。そこで新しい台の各元を、`x : S` と `x ∈ᶜ M` の証拠の組にする。`𝒮 ↾ M` は、構造 `𝒮` をこのクラスへ制限したものを表す。

構造の制限には、クラスの推移性も、関係が命題に値を取るという条件も要らない。真理値の型 `Ω` は任意であり、台の元を選ぶ述語だけが命題値であればよい。以下では台に関するフィールドの射影をモジュールのスコープで開き、二つの関係は使う場所で構造を固定して開く。`hPropView` の内部とは異なり、構造は固定せず、`S 𝒮` のように各射影へ構造を引数として渡す。ここで `𝒮` は、数学の記法で `S` に付ける添字に相当し、どの構造の台かを指定する。ただし Agda では通常の関数の引数である。

```agda
open ZFStructure using ( S; isSetS )
```

**定義** (`_↾_`) 任意のクラス `M : S → hProp ℓ` に対し、制限された構造の台を `Σ[ x ∶ S ] (x ∈ᶜ M)` とする。これは依存対の型であり、構造の内部でそのクラスを表す集合ではない。先に導入した `isSetClass` を `isSetS` と各点で所属の型が命題であることに適用し、新しい台の h-集合性を得る。

```agda
infixl 21 _↾_
_↾_ : ∀ {ℓ ℓΩ} {Ω : Type ℓΩ} (𝒮 : ZFStructure ℓ Ω)
    → (S 𝒮 → hProp ℓ) → ZFStructure ℓ Ω
_↾_ {ℓ} 𝒮 M = record
  { S      = Σ[ x ∶ S 𝒮 ] (x ∈ᶜ M)
  ; isSetS = isSetClass (isSetS 𝒮) (λ x → ⟨ M x ⟩isProp)
```

新しい台の上で二つの関係をどう定めるか。制限された元 `a`、`b` の第一射影に `𝒮` の関係を適用し、`a .fst ≈ˢ b .fst` と `a .fst ∈ˢ b .fst` を得る。以下の定義では、元の構造のこの二つの関係だけを局所的に開く。第二成分の証拠は元が `M` に属することを保証するだけで、等号や所属の真理値を変えない。つまり二つの関係を `fst` に沿って `𝒮` から引き戻す。

```agda
  ; _≈ˢ_   = λ a b → a .fst ≈ˢ b .fst
  ; _∈ˢ_   = λ a b → a .fst ∈ˢ b .fst }
  where open ZFStructure 𝒮 using ( _≈ˢ_; _∈ˢ_ )
```

二つの関係は第一成分だけを使う。それでは、依存対そのものの等しさは第二成分の証拠に左右されるだろうか。ここで扱うのは Agda のパス等式であり、自由に与えた構造の関係 `≈ˢ` ではない。

**補題** (`↾-reflects`) 制限された台の `a`、`b` について、パス `a .fst ≡ b .fst` からパス `a ≡ b` が定まる。

**証明** 第一成分の間に与えられたパスに沿って、一方の証拠を移す。移した後の二つの証拠は同じ命題に属するので等しく、依存対の間のパスが得られる。この構成はライブラリの補題 `Σ≡Prop` が行う。その前提である各ファイバーの命題性は `⟨ M x ⟩isProp` が与える。

```agda
↾-reflects : ∀ {ℓ ℓΩ} {Ω : Type ℓΩ} {𝒮 : ZFStructure ℓ Ω}
             {M : S 𝒮 → hProp ℓ} {a b : S (𝒮 ↾ M)}
           → a .fst ≡ b .fst → a ≡ b
↾-reflects {M = M} = Σ≡Prop (λ x → ⟨ M x ⟩isProp)
```

逆向きに特別な補題は要らない。パス `a ≡ b` に `fst` を作用させれば `a .fst ≡ b .fst` が得られる。

## まとめ

構造は、考察する対象の台と、等号・所属の解釈を与える。真理値の型によらず、二つの関係を受け継ぎながら、命題値の述語で台を制限できる。添えられた所属の証拠は、第一成分が等しい依存対を区別しない。命題値の構造では、推移性はこれとは独立の条件であり、選ばれた対象に属する要素も選ばれた範囲に残ることを要求する。次章では、選んだ構造の中で項と論理式に意味を与える。