---
title: "结构"
module: FOL.ZFStructure
lang: zh
site: "Bedrock"
description: "结构"
stage: "一阶逻辑"
reading_order: 7
canonical: https://bedrock.institute/zh/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/ja/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` 上给出相等与成员关系。类型 `S` 称为结构的**载体**。我们把整个结构记作 `𝒮`，把载体中的元素记作 `x`、`y`；关系记号上的 `ˢ` 则表示该关系由 `𝒮` 提供。

为什么相等关系也要单独给出，而不直接采用 Agda 的路径相等 `x ≡ y`？因为对象语言中的相等记号可以有自己的解释，不必预先等同于路径相等。结构中的 `x ≈ˢ y` 给出一个真值，并不要求先有一条路径 `x ≡ y`。在这个定义中，`≈ˢ` 只是一个二元关系：我们既不要求它满足相等关系的定律，也不要求它与成员关系相容。

**定义** (`ZFStructure`) 给定载体的层级 `ℓ` 和真值类型 `Ω`，用 `record` 定义结构。其字段包括载体 `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` 只是一段语法。这个 `record` 只提供载体和关系，不规定词项怎样指代载体元素，也不要求两种关系满足集合论公理。

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

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

**定义** (`ZFStructureₕ`) 取 `hProp ℓ` 为真值类型 Ω，得到下文使用的命题值结构。下标 `ₕ` 表示这一选择，其中命题与载体处于同一层级 `ℓ`。这只是原定义的一个特例，不另设 `record`。

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

`ZFStructure` 这个名字表明它解释的是集合论语言，并不表示它已经是 ZF 模型。例如，可以用自然数作载体，用通常的大小关系解释成员关系。即使提供了定义所要求的全部数据，也不能仅凭这些数据断言 ZF 公理成立。

## 命题值结构

在命题值结构 `ZFStructureₕ` 中，`x ∈ˢ y` 包含一个类型，以及该类型为命题的证明。若要把「`x` 属于 `y`」的证明作为函数实参，就需要取出底层类型 `⟨ 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` 又按结构中的成员关系属于 `x`，那么 `y` 是否也被选中？如果答案总是肯定的，就称 `M` 为**传递类**。这里要求的是对*元素*闭合，而不是对子集闭合。

传递性是对类的闭合性要求，不是结构的字段。它使用成员关系的证明类型，因此放在 `hPropView` 中，沿用子模块已固定的命题值结构。

**定义** (`Transitive`) 给定命题值结构 `𝒮` 与类 `M`。若对任意载体元素 `x`、`y`，都能由 `y ∈ᵗ x` 和 `x ∈ᶜ M` 的证明得到 `y ∈ᶜ M` 的证明，就称 `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` 表示元素 `x` 满足谓词 `M`，说的不是两个载体元素之间的关系。

| 记号 | 两侧的对象 | 得到的结果 |
| --- | --- | --- |
| `t ∈̇ u` | 两个词项 | 尚未赋予真值的公式 |
| `x ∈ˢ y` | 两个载体元素 | `hProp ℓ` 中的命题 |
| `x ∈ᵗ y` | 同样的两个元素 | `x ∈ˢ y` 的底层证明类型 |
| `x ∈ᶜ M` | 一个元素与一个类 | `M x` 的底层证明类型 |
: 四种成员关系记号各自的用途

## 子结构

若要让变元只在 `M` 选中的元素中取值，就需要更换载体。仅仅给出谓词 `M`，却仍以整个 `S` 为载体，并不能限制取值范围。因此，新载体的每个元素都由两部分组成：一个 `x : S`，以及 `x ∈ᶜ M` 的证明。把结构 `𝒮` 限制到类 `M` 所得的结构，记作 `𝒮 ↾ M`。

限制结构不要求类具有传递性，也不要求原结构的关系取命题值：真值类型 `Ω` 可以任意选择，只有筛选载体元素的谓词需要取命题值。下面在本模块中打开载体相关的字段投影，两个关系则留到使用时再针对具体结构打开。与 `hPropView` 内的打开方式不同，这里不固定结构，而是在使用各投影时传入结构，例如用 `S 𝒮` 取得 `𝒮` 的载体。其中，`𝒮` 的作用相当于数学记号中 `S` 的下标，指明这是哪个结构的载体；在 Agda 中，它仍是普通的函数实参。

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

**定义** (`_↾_`) 给定类 `M : S → hProp ℓ`，限制结构的载体为 `Σ[ x ∶ S ] (x ∈ᶜ M)`。这是一个依值对类型，并不是在原结构内部找到了一个代表类 `M` 的集合。原载体是 h-集合，而每个元素属于 `M` 的证明类型都是命题，因此可用前文引入的 `isSetClass` 证明新载体也是 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)
```

反方向更直接：将 `fst` 作用于路径 `a ≡ b`，就得到 `a .fst ≡ b .fst`，无需另设引理。

## 小结

结构给出了所讨论的对象，以及相等和成员关系的解释。无论结构选用什么真值，都可以用命题值谓词限制载体，并继承原来的两种关系；附带的成员关系证明不会区分第一分量相等的依值对。对于命题值结构，传递性是另一项独立条件，要求被选中对象的元素也留在选定范围内。下一章将在选定的结构中解释词项与公式。