ZF 与 ZFC 的模型

可以直接阅读本章，也可以通过阅读指南和依赖地图选择其他路线。

阅读指南 · 依赖地图

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

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

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

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

{-# 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.⊥，以及选择公理所用的命题截断 ∥_∥₁。

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 在典范常元解释下实例化满足关系 _⊨_，其中常元指自身，于是公式中的自由变元槽就被读作对某个具体集合的隶属。

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，与公理本身所在的位置一致。

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 组成的依值对，其第二分量仍是命题，这一事实后面会反复使用。

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 以该实现者为中心可缩。

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 而非截断存在陈述的原因。

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

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

℩-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) 都有底层类型，但定义把一切都保持为真值。

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

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

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)。

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 唯一的自由变元槽。

    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 的幂集实现子集的类，用的是上一节的派生关系 ⊆ˢ。

                   → ((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)。

  ∅ : 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 的成员之全体」的集合。二元并不另外花费公理，它是配对与并的复合。注意定义的方向：∪ 是由 ⋃ 作用于配对而构造，而不是相反。

  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 的子集。

  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

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

  𝒫 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。不需要新公理，也不需要新的存在性证明；一条双符号公式已经指名了分离能够实现的一个宿主谓词。

  _∩_ : 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 ℓ 中的命题，⟨_⟩ 取其底层类型，从该类型的居民出发，字段导出荒谬。这说明第零个数码没有成员，却完全未提及派生的空集。

  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 上的 ⊔；第二条说前一个数码的每个这样的成员、以及与之相等者，都属于后继。两个方向合起来说：后继数码的成员恰是前一个数码连同其成员，这正是冯·诺伊曼步骤，仅用 ∈ˢ 与 ≈ˢ 陈述。

                 × (⟨ (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 随即以熟悉的形式断言：实现该类的集合唯一存在。

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

  field
    hasInfinity : isContr (SetOf isNumeral)

  ω : S

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

  ω = ℩ hasInfinity

最初的定理

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

ZFC：作为扩展的选择公理

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

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

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 无截断地成立。注意不交前提的形状：其结论是宿主中的路径，正是共享点证据的截断在为无截断的相等供料。

    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 的存在性，因此公理不指定某个选择集。

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

小结

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