---
title: "ZF 与 ZFC 的模型"
module: FOL.ZFModel
lang: zh
site: "Bedrock"
description: "ZF 与 ZFC 的模型"
stage: "一阶逻辑"
reading_order: 11
canonical: https://bedrock.institute/zh/FOL.ZFModel.html
html: FOL.ZFModel.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/FOL/ZFModel.lagda.md
prerequisites: [Base.Prelude, FOL.ZFStructure, FOL.Syntax, FOL.Semantics]
routes: [common-foundations]
translations: [https://bedrock.institute/en/FOL.ZFModel.md, https://bedrock.institute/ja/FOL.ZFModel.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# ZF 与 ZFC 的模型

一个裸结构通过为 ZF 公理提供见证而成为集合论模型。本章分几步走完这条路：先说明集合何时实现一个类，再由显式的外延性论证证明实现者的唯一性，引入一个从唯一存在读出集合的摹状词算子，然后把公理汇成一个 record。最后加入选择公理，把 ZF 模型扩展为 ZFC 模型。

裸结构中还没有任何东西配得上「集合论」之名。它的成员关系未必容纳空集，未必能配对两个元素，也未必能聚出子集。一个集合宇宙必须提供什么，正是 **ZF 公理**所陈述的内容，本章把它们一一写出。**ZF 模型**是其字段供给这些公理的结构，因此「`𝒮` 满足 ZF」恰是说：这样的见证在 `𝒮` 处存在。

设定在此一次确定：`𝒮` 的等词与成员关系取值于 `hProp ℓ`，所以每条这样的断言都是命题；整个模块在同一个宇宙层级 `ℓ` 上运行，而它的公理住在 `Type (ℓ-suc ℓ)` 中。

模块签名说明了要研究的对象类型：`𝒮` 是一个 `ZFStructure`，其真值为命题，即 `hProp ℓ` 上的结构。由此立刻得到两点。其一，结构的等词 `≈ˢ` 与成员 `∈ˢ` 返回带有底层类型的命题，因此本章的成员断言都是可以用证明占据的东西。其二，参数 `{ℓ}` 是宇宙层级，全程固定：载体 `S` 住在 `Type ℓ`，而量化 `S` 全部子集的陈述，即公理本身，则落在 `Type (ℓ-suc ℓ)`。

```agda
{-# OPTIONS --cubical --safe --guardedness #-}

open import Base.Prelude
open import FOL.ZFStructure using ( ZFStructure; module hPropStructure )

module FOL.ZFModel {ℓ} (𝒮 : ZFStructure ℓ) where
```

这些公理直接在 `hProp` 中断言事实。常元解释取语义章的典范情形：常元域就是载体自身，解释就是 `id`，于是公式里出现的常元就**是**它指名的那个集合。

这里汇集公理所需的工作词汇。语法章提供 `Formula`、成员符号 `∈̇` 与构造子 `var`、`con`；分离与替换将把公式作为真正的输入。语义章贡献模块 `At`，它固定一个常元解释，并给出该解释下公式的满足关系。宿主库则提供 `Σ≡Prop` (用于化归第二分量为命题的依值对的路径)、正则公理将要记录的良基类型 `WellFounded`、空类型 `Empty.⊥`，以及选择公理所用的命题截断 `∥_∥₁`。

```agda
open import FOL.Syntax using ( Formula; var; con; _∈̇_ )
open import FOL.Semantics 𝒮 using ( module At )
open import Cubical.Data.Sigma using ( Σ≡Prop )
open import Cubical.Induction.WellFounded using ( WellFounded )
import Cubical.Data.Empty as Empty
```

两个 open 把结构与满足关系的名字带入作用域；`hProp` 上的直接逻辑运算已由基础词汇提供。打开 `hPropStructure 𝒮` 得到结构的载体 `S`、其 h-集合性证据，以及两个真值关系 `≈ˢ` 与 `∈ˢ`，连同成员的 Type 值读法 `∈ᵗ`。最后，打开 `At S id` 在典范常元解释下实例化满足关系 `_⊨_`，其中常元指自身，于是公式中的自由变元槽就被读作对某个具体集合的隶属。

```agda
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∥_∥₁ )

open hPropStructure 𝒮

open At S id using ( _⊨_ )
```

## 把类实现为集合

接下来的公理几乎全是同一个形状：**存在一个集合，其成员恰好是如此这般者**。先把「如此这般」说清楚。**类**是载体上的命题值谓词 `S → hProp ℓ`：可以对它谈论隶属，却不保证有集合恰好收齐它的全部成员。(类在前面已经出现过：结构章的限制 `𝒮 ↾ M` 正是沿这样一个 `M` 进行的。) 本节定义集合何时实现一个类，指出实现本身是命题，并把两者打包在一起。

实现的定义刻意采取逐点形式。`IsSetOf Q b` 说：对载体的**每个**元素 `x`，命题 `x ∈ˢ b` 作为 `hProp ℓ` 的元素等于类的值 `Q x`。这里没有公式、没有语法、也没有化归：比较就是真值之间的直接相等。该类型住在 `Type (ℓ-suc ℓ)`，因为它量化了整个 `S`，与公理本身所在的位置一致。

```agda
IsSetOf : (S → hProp ℓ) → S → Type (ℓ-suc ℓ)
IsSetOf Q b = (x : S) → (x ∈ˢ b) ≡ Q x

isPropIsSetOf : (Q : S → hProp ℓ) (b : S) → isProp (IsSetOf Q b)
isPropIsSetOf Q b = isPropΠ (λ x → isSetHProp _ _)

SetOf : (S → hProp ℓ) → Type (ℓ-suc ℓ)
```

实现是命题而不是更重的数据，这一点现在检验。函数类型 `(x : S) → (x ∈ˢ b) ≡ Q x` 是命题，恰因每个纤维都是命题：`hProp ℓ` 即 `hProp ℓ`，`isSetHProp` 说明 `hProp` 中两个命题之间的路径类型是 h-集合，其恒等类型因此是命题；`isPropΠ` 把逐点事实提升到整个函数类型。于是 `SetOf Q`，即候选集合 `b` 与证据 `IsSetOf Q b` 组成的依值对，其第二分量仍是命题，这一事实后面会反复使用。

```agda
SetOf Q = Σ[ b ∈ S ] IsSetOf Q b
```

一个类能有几个实现者？在**外延公理** (成员相同的集合相等；它将是 record 的第一个字段) 之下，答案是至多一个，而且是结构意义上的强「至多一」：任何一个实现者都使实现者的整个类型可缩。这条引理把外延性作为显式输入，因为提供外延性的 record 此时还没有定义。

给定类 `Q` 的一个实现者 `(b , sp)`，收缩把任何其他实现者 `(b' , sp')` 映到通向它的路径。第一分量的路径是把外延性用于 `λ x → sp x ∙ sym (sp' x)`：在每个 `x` 处，两条规格分别给出 `x ∈ˢ b ≡ Q x` 与 `x ∈ˢ b' ≡ Q x`，把第一条与第二条的反向复合，得到 `x ∈ˢ b ≡ x ∈ˢ b'`，外延性正是把它变成 `b ≡ b'`。第二分量由 `Σ≡Prop` 处理；这是合法的，因为 `isPropIsSetOf` 说明任何两个实现者的规格相等。注意论证的形状：类 `Q` 与一个实现者是显式输入，所以结论字面上就是类型 `SetOf Q` 以该实现者为中心可缩。

```agda
setOf-unique : ({a b : S} → ((x : S) → (x ∈ˢ a) ≡ (x ∈ˢ b)) → a ≡ b)
             → (Q : S → hProp ℓ) → SetOf Q → isContr (SetOf Q)
setOf-unique ext Q (b , sp) = (b , sp) , λ { (b' , sp') →
  Σ≡Prop (isPropIsSetOf Q) (ext (λ x → sp x ∙ sym (sp' x))) }
```

## 摹状词算子

`isContr` 是宿主的**唯一存在**：它打包一个中心，连同把每个元素收缩到该中心的数据。因此 `isContr (SetOf Q)` 读作：**恰有一个由 `Q` 者组成的集合**，而中心直接给出一个典范见证。后面的存在性公理都采用这一形式，其好处立即可见：有了唯一存在，「那个满足条件的集合」就是一次投影。不需要另加经典的描述公理，因为收缩的中心本身就是数据。

算子 `℩` 接受 `SetOf Q` 的收缩证明，返回其中心的第一个分量，即 `S` 的一个元素：`isContr A` 打包为一个中心连同收缩，`c .fst` 是中心，再投影一次就到达集合本身。经典处理在这里会调用描述公理；此处从唯一存在到见证的过渡是纯粹的数据提取，这也是下面每条公理都以 `isContr` 而非截断存在陈述的原因。

```agda
℩ : {Q : S → hProp ℓ} → isContr (SetOf Q) → S
℩ c = c .fst .fst
```

若无法读回该集合的成员是什么，提取出的集合便毫无用处；而这个读法同样是投影：`℩-spec c` 就是中心所携带的规格，即收缩的第一分量的第二分量。两者合起来说：由 `Q` 者组成的唯一集合存在，而 `℩` 把这个集合连同证书 `x ∈ˢ (℩ c) ≡ Q x` 一并交给你。后文每个派生运算都由「把 `℩` 用于某个公理字段」与「引用 `℩-spec` 作为规格」组成。

```agda
℩-spec : {Q : S → hProp ℓ} (c : isContr (SetOf Q)) → IsSetOf Q (℩ c)
℩-spec c = c .fst .snd
```

## 子集

还需要一个派生关系来补全词汇：`a ⊆ˢ b` 谓 `a` 的每个成员都是 `b` 的成员。这正是外延公理所比较的关系，只不过作为真值而非定理前提来读。与将要返回集合的公理不同，它住在 `hProp ℓ` 中，并且用 `hProp` 上直接的全称量词而非宿主函数类型来陈述。幂集字段与选择公理的选择集形式都将用它表述。

定义使用 `hProp` 上直接的全称量词 `∀[ x ] P x`，把对所有载体元素 `x` 的蕴涵 `x ∈ˢ a ⇒ x ∈ˢ b` 合取起来。留在 `hProp ℓ` 内很重要：结果是一个真值，可以与其他联结词比较与组合，而元层的函数类型做不到这一点。Type 值的蕴涵也可用，因为 `hProp` 中每个 `(x ∈ˢ a) ⇒ (x ∈ˢ b)` 都有底层类型，但定义把一切都保持为真值。

```agda
_⊆ˢ_ : S → S → hProp ℓ
a ⊆ˢ b = ∀[ x ∶ S ] (x ∈ˢ a) ⇒ (x ∈ˢ b)
```

记号 `a ⊆ˢ b` 将用于幂集公理及后续论证。这里固定它的优先级，使同时含成员、等词与子集的式子有明确读法。

```agda
infix 20 _⊆ˢ_
```

## 公理，作为 record

这里是本章的核心。字段分三类。第一类是外延性与存在性公理：空集、配对、并、分离、替换、幂集，全部采取刚准备好的唯一存在形式，因此各自经 `℩` 得到相应的集合 (无穷稍后加入)。第二类是两条公式模式：分离与替换各收一条 `Formula S 1` 或 `Formula S 2`，并用语义章的满足关系解释它，于是一阶逻辑诸章造出的语言在此真正派上用场。这里的限制是明确的：这些字段量化编码后的一阶公式，而非任意宿主谓词 `S → hProp ℓ`。因此每个实例都带有对象语言语法，并由满足关系解释。第三类是正则公理：Type 值成员关系的良基性，以宿主库的 `WellFounded _∈ᵗ_` 记录。下一节解释为何这条公理陈述在元层面，而其余公理住在结构内部。

这个 record 是命题值结构加上公理所要求的保证；由于字段量化了整个 `S`，它自身住在 `Type (ℓ-suc ℓ)`。头两个字段不是唯一存在形态。外延性是从成员真值逐点相等得到路径 `a ≡ b` 的蕴涵，正是让 `setOf-unique` 得以成立的那个假设。正则性取 `WellFounded _∈ᵗ_`，即 Type 值成员关系的良基性：它为每个元素提供 `Acc` 数据，从而支持沿成员关系的递归与归纳。其余字段各自对某个类 `Q` 断言 `isContr (SetOf Q)`。

```agda
record isZFModel : Type (ℓ-suc ℓ) where
  field
    extensional    : {a b : S} → ((x : S) → (x ∈ˢ a) ≡ (x ∈ˢ b)) → a ≡ b
    regularity     : WellFounded _∈ᵗ_
    hasEmpty       : isContr (SetOf (λ _ → ⊥))
```

把每个类读回自然语言，教科书的陈述一一重现。没有谁实现 `⊥`，所以空集就是实现恒假类的唯一集合。`a` 与 `b` 的配对实现「与 `a` 结构相等或与 `b` 结构相等」的类，用 `hProp` 上直接的析取 `⊔` 连接。`a` 的并实现那些 `x`：存在 `a` 的成员 `y` 使 `x` 属于 `y`，用 `⊓` 合取、`∃[ x ] P x` 存在聚合。分离是第一个消费公式的字段，恰好留下 `a` 中满足 `φ` 的成员 `x`：该类是「属于 `a`」与「`φ` 在单元素环境 `x ∷ []` 下满足」的合取，这个环境的唯一一项填入 `Formula S 1` 唯一的自由变元槽。

```agda
    hasPair        : (a b : S) → isContr (SetOf (λ x → (x ≈ˢ a) ⊔ (x ≈ˢ b)))
    hasUnion       : (a : S) → isContr (SetOf (λ x → ∃[ y ∶ S ] (y ∈ˢ a) ⊓ (x ∈ˢ y)))
    hasSeparation  : (a : S) (φ : Formula S 1)
                   → isContr (SetOf (λ x → (x ∈ˢ a) ⊓ ((x ∷ []) ⊨ φ)))
    hasReplacement : (a : S) (φ : Formula S 2)
```

替换是最长的字段，并自带一个前提。它取 `Formula S 2`，其两个自由变元槽按环境 `y ∷ x ∷ []` 的次序读：先是输出值，再是输入。前提说 `φ` 在 `a` 上是**函数性**的：对 `a` 的每个成员 `x`，恰有一个 `y` 满足 `φ`，这个「恰一」就是由这些 `y` 组成的类型的 `isContr`。在该前提之下，字段断言像集的唯一存在，即与 `a` 的某个成员处于关系 `φ` 的那些 `y` 组成的集合。注意它不断言什么：没有函数性前提时，字段不作任何断言，这与经典处理中替换公理限于函数性公式的限制一致。最后，`a` 的幂集实现子集的类，用的是上一节的派生关系 `⊆ˢ`。

```agda
                   → ((x : S) → ⟨ x ∈ˢ a ⟩ → isContr (Σ[ y ∈ S ] ⟨ (y ∷ x ∷ []) ⊨ φ ⟩))
                   → isContr (SetOf (λ y → ∃[ x ∶ S ] (x ∈ˢ a) ⊓ ((y ∷ x ∷ []) ⊨ φ)))
    hasPower       : (a : S) → isContr (SetOf (λ x → x ⊆ˢ a))
```

把每个 `λ` 读回自然语言，熟悉的陈述一一归位。没有谁实现 `⊥`，所以 `hasEmpty` 就是空集。配对的成员是与 `a` 或 `b` 相等者；并的成员是成员的成员。分离留下 `a` 中满足 `φ` 的成员 (环境 `x ∷ []` 把唯一的自由变量填上)。替换先要求 `φ` 在 `a` 上是函数性的，即在 `isContr` 意义下一进一出，再收集输出。幂集的成员就是子集。

## 正则公理为何置于元层面

其余公理说的要么是对象语言，要么是单纯的成员关系；唯独正则公理要借助宿主的良基概念。经典理由是：**没有任何一阶句子能表达外部良基性**。由经典模型论的**紧致性定理**，一个恰好在良基结构中成立的句子，也会在带有无穷下降 ∈-链的结构中成立，因为扩充理论 (新常元链 $a_{n+1} \in a_n$) 的每个有限片段都有模型。本书讲述这个论证但不依赖它，紧致性也不在本书展开。实践理由直接写在类型 `WellFounded _∈ᵗ_` 里：良基性作为显式数据，支持沿成员关系的递归与归纳。付出的代价是这个条件不再被一阶公式看见；除了下文证明的内容之外，本章不对这损失有多大作任何断言。

## 派生运算

现在用 `℩` 把每个唯一存在实现为运算，并用 `℩-spec` 给出规格；下面每条规格都是一次投影。配对之并给出二元并，二元并又给出**后继** `a ⁺ = a ∪ {a}` (`a` 与自身的配对即单点集)：这是从一个集合到下一个集合的冯·诺伊曼后继步骤，也是无穷公理稍后所用的那一步。

在 record 内部，每个字段通过应用 `℩` 变成运算。空集就是 `℩ hasEmpty`，配对运算 `pair a b` 把 `℩` 用于特定 `a`、`b` 处的配对证书。每个应用都是合法的，因为字段提供 `isContr (SetOf _)`，恰是 `℩` 的输入类型。规格 `pair-spec` 完全不是新证明：它在同一字段上引用 `℩-spec`，其陈述恰是实现断言，即对每个 `x`，`x ∈ˢ pair a b` 等于析取 `(x ≈ˢ a) ⊔ (x ≈ˢ b)`。

```agda
  ∅ : S
  ∅ = ℩ hasEmpty

  pair : S → S → S
  pair a b = ℩ (hasPair a b)

  pair-spec : ∀ a b → IsSetOf (λ x → (x ≈ˢ a) ⊔ (x ≈ˢ b)) (pair a b)
```

并运算 `⋃ a` 提取 `a` 的并证书，而二元并由它定义：`a ∪ b` 是配对 `pair a b` 的并，恰是「成员为 `a` 的成员与 `b` 的成员之全体」的集合。二元并不另外花费公理，它是配对与并的复合。注意定义的方向：`∪` 是由 `⋃` 作用于配对而构造，而不是相反。

```agda
  pair-spec a b = ℩-spec (hasPair a b)

  ⋃ : S → S
  ⋃ a = ℩ (hasUnion a)

  _∪_ : S → S → S
  a ∪ b = ⋃ (pair a b)
```

分离成为以公式为参数的运算：`separate a φ` 把 `℩` 用于 `a` 与公式 `φ` 处的分离证书，因此所得集合依赖一段对象语言语法。其规格同样逐字引用 `℩-spec`，给出对每个 `x` 的 `x ∈ˢ separate a φ ≡ (x ∈ˢ a) ⊓ ((x ∷ []) ⊨ φ)`：成员关系由「属于 `a`」与「满足 `φ`」合成。幂集运算 `𝒫 a` 提取幂集证书；经由它实现的类读出，其成员恰是 `a` 的子集。

```agda
  separate : (a : S) → Formula S 1 → S
  separate a φ = ℩ (hasSeparation a φ)

  separate-spec : ∀ a φ → IsSetOf (λ x → (x ∈ˢ a) ⊓ ((x ∷ []) ⊨ φ)) (separate a φ)
  separate-spec a φ = ℩-spec (hasSeparation a φ)

  𝒫 : S → S
```

末尾的空行结束这一组运算；接下来的小节将在此基础上推进，首先不借助任何新公理地导出交。

```agda
  𝒫 a = ℩ (hasPower a)
```

## 由分离导出的交

二元交刻意**不设**为字段。两个符号的公式 `var zero ∈̇ con b` 表示「该变量是 `b` 的成员」；把它传给 `separate` 并作用于 `a`，分离公理就给出 `a ∩ b`。它的规格与分离的规格完全相同，因为按 `⊨` 的定义子句，该公式的满足直接计算为 `x ∈ˢ b`。这是一般模式的一次具体运用：凡能被公式指名的宿主谓词，分离都能把它变成集合。

定义是应用语法的一行：`a ∩ b` 沿着那条内容仅为原子成员断言 `var zero ∈̇ con b` 的公式分离 `a`。由于常元 `b` 在解释 `id` 下指自身，在环境 `x ∷ []` 下满足该公式，按满足关系的定义子句化归为真值 `x ∈ˢ b`。于是规格定理就是分离规格在该特定公式上的原样引用：交中的成员关系是合取 `x ∈ˢ a ⊓ x ∈ˢ b`。不需要新公理，也不需要新的存在性证明；一条双符号公式已经指名了分离能够实现的一个宿主谓词。

```agda
  _∩_ : S → S → S
  a ∩ b = separate a (var zero ∈̇ con b)

  ∩-spec : ∀ a b x → (x ∈ˢ (a ∩ b)) ≡ ((x ∈ˢ a) ⊓ (x ∈ˢ b))
  ∩-spec a b x = separate-spec a (var zero ∈̇ con b) x
```

## 无穷

只剩无穷公理，它要求一个真正无穷的集合存在。**数码**是冯·诺伊曼自然数：`∅`、`∅ ⁺`、`(∅ ⁺) ⁺`，如此继续。record 把数码链本身作为字段，并用两条以裸成员与裸等词表述的命题方程确定它：第零个数码没有成员，后继数码的成员恰是前一个数码及其成员。由外延公理，这两条方程分别给出 `numeral zero ≡ ∅` 与 `numeral (suc n) ≡ numeral n ⁺`，所以其强度与直接定义数码链相同。方程不提及派生的 `∅`，因此具体模型可以采用最便于载体计算的数码链定义，并在证明方程时避免展开摹状词算子。

数码链是函数 `numeral : ℕ → S`，用宿主自然数作索引是显式数据。零的情形是否定条件：`z ∈ˢ numeral zero` 这个 Type 值隶属的任何居民都导出矛盾，见证落在空宿主类型 `Empty.⊥` 中。注意读法：`∈ˢ` 返回 `hProp ℓ` 中的命题，`⟨_⟩` 取其底层类型，从该类型的居民出发，字段导出荒谬。这说明第零个数码没有成员，却完全未提及派生的空集。

```agda
  field
    numeral      : ℕ → S
    numeral-zero : (z : S) → ⟨ z ∈ˢ numeral zero ⟩ → Empty.⊥
    numeral-suc  : (n : ℕ) (z : S)
                 → (⟨ z ∈ˢ numeral (suc n) ⟩ → ⟨ (z ∈ˢ numeral n) ⊔ (z ≈ˢ numeral n) ⟩)
```

后继情形是一对蕴涵，都处于无截断的命题读法之内。第一条说 `numeral (suc n)` 的成员 `z` 属于 `numeral n` 或与之结构相等，析取直接使用 `hProp` 上的 `⊔`；第二条说前一个数码的每个这样的成员、以及与之相等者，都属于后继。两个方向合起来说：后继数码的成员恰是前一个数码连同其成员，这正是冯·诺伊曼步骤，仅用 `∈ˢ` 与 `≈ˢ` 陈述。

```agda
                 × (⟨ (z ∈ˢ numeral n) ⊔ (z ≈ˢ numeral n) ⟩ → ⟨ z ∈ˢ numeral (suc n) ⟩)
```

`isNumeral` 所定出的类由**与某个数码相等**的对象组成。量化取提升到工作层级的 `ℕ`，因为索引数据位于最底层宇宙。本章采用的**无穷公理**说这个确切的类是集合。因此 `ω` 得到双向刻画：每个数码都属于它，而它的每个成员都与某个数码相等。

类 `isNumeral` 是直接在 `hProp` 中写出的存在式：`∃[ x ] P x` 在一个载体类型上量化，析取命题族 `x ≈ˢ numeral (lower n)`。载体必须具有类型 `Type ℓ` 才能应用 `∃[ x ] P x`，而 `ℕ` 住在 `Type ℓ-zero`；`Lift {ℓ-zero} {ℓ} ℕ` 把它提升到工作层级，`lower` 取回普通索引交给 `numeral`。这是层级的调整，不是数学内容的改变：被提升的类型恰有同样的元素。字段 `hasInfinity` 随即以熟悉的形式断言：实现该类的集合唯一存在。

```agda
  isNumeral : S → hProp ℓ
  isNumeral x = ∃[ n ∶ Lift {ℓ-zero} {ℓ} ℕ ] x ≈ˢ numeral (lower n)

  field
    hasInfinity : isContr (SetOf isNumeral)

  ω : S
```

与其他唯一存在一样，`ω` 是 `℩` 从 `hasInfinity` 取出的中心。由于被实现的类就是 `isNumeral` 本身，规格 `℩-spec` 说 `ω` 的每个成员都与某个数码相等；正是这一点使这个强形式可以直接当作自然数集来用，而不只是数码能嵌入其中的一个集合。

```agda
  ω = ℩ hasInfinity
```

## 最初的定理

外延公理把整套存在机制一次性升级：由 `setOf-unique`，凡是有实现者的类，该实现者就是唯一实现者，且实现者类型以它为中心可缩。因此本章的每个派生集合都带有唯一性。

## ZFC：作为扩展的选择公理

这里采用选择集形式的**选择公理**：给定集合 `a`，若其成员非空且两两不交，则存在一个集合，与 `a` 的每个成员恰交于一点。该形式只用成员关系和派生的交即可陈述；它与其他形式的等价性属于模型内部的数学，留待需要时证明。命题截断 `∥_∥₁` 分别包住非空性、公共点证据与选择集的存在。因此公理断言存在，却不在全局选定见证。把它保持为独立的扩展而非基础 record 的字段，正好保留了 ZF 所证与选择公理所增之间的区别。

ZFC record 采取扩展而非重复：它的第一个字段是一整个 ZF 模型，随后 `open ... public` 一行把其全部字段再导出，于是对 ZF 模型证明的一切都逐字适用于 ZFC 模型。record 只在这之后才声明自己的新字段，使新增公理与基础理论干净地分开。

```agda
record isZFCModel : Type (ℓ-suc ℓ) where
  field
    zf : isZFModel
  open isZFModel zf public
  field
```

`hasChoice` 的两条前提说 `a` 是由非空、两两不交的集合组成的族，各自按此处可用的读法理解。非空性是截断的：对 `a` 的每个成员 `x`，**仅仅**存在其中的 `y`，即 `∥ Σ[ y ∈ S ] ⟨ y ∈ˢ x ⟩ ∥₁`，没有被选定的见证。两两不交同样截断：若 `a` 的两个成员 `x` 与 `y` **仅仅**共享一点 `z`，则 `x ≡ y` 无截断地成立。注意不交前提的形状：其结论是宿主中的路径，正是共享点证据的截断在为无截断的相等供料。

```agda
    hasChoice :
      (a : S)
      → ((x : S) → ⟨ x ∈ˢ a ⟩ → ∥ Σ[ y ∈ S ] ⟨ y ∈ˢ x ⟩ ∥₁)
      → ((x y : S) → ⟨ x ∈ˢ a ⟩ → ⟨ y ∈ˢ a ⟩
           → ∥ Σ[ z ∈ S ] (⟨ z ∈ˢ x ⟩ × ⟨ z ∈ˢ y ⟩) ∥₁ → x ≡ y)
```

结论同样是截断的存在：**仅仅**存在一个选择集 `c`，使得对 `a` 的每个成员 `x`，交 `c ∩ x` 恰有一个元素，即其元素类型的 `isContr`。内层 `isContr` 不是截断：对每个 `x`，它给出 `c ∩ x` 的一个元素，并证明其他此类元素都与之相等。外层截断作用于合适的 `c` 的存在性，因此公理不指定某个选择集。

```agda
      → ∥ Σ[ c ∈ S ] ((x : S) → ⟨ x ∈ˢ a ⟩
           → isContr (Σ[ z ∈ S ] ⟨ z ∈ˢ (c ∩ x) ⟩)) ∥₁
```

## 小结

ZF 模型是一个含三类字段的 record：外延性，它使实现者唯一；空集、配对、并、分离、替换、幂集的唯一存在字段，其中分离与替换限于本书自己的公式；以及正则性，作为宿主对成员关系的良基性陈述在元层面，从而沿成员关系的递归与归纳可用。`℩` 把字段转为运算，其规格都是投影；二元并与后继是复合，交则由分离加一条满足关系直接计算的双符号公式得到。无穷以数码链进入，即由裸成员方程确定的函数 `ℕ → S`；强形式使 `ω` 成为成员全为数码的集合。`isZFCModel` 在此之上添加选择公理，其中非空性与公共点证据截断，结论也截断，而每个所选交集的 `isContr` 不截断。