---
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: /llms.txt
license: CC-BY-NC-SA-4.0
---
# 结构

关于集合的一阶语言有两个初始谓词：等词与隶属。要解释它，就必须选定变量的取值范围，以及这两个谓词在那里分别指什么。`ZFStructure` 正是打包这些数据：一个由「集合」组成的载体，加上等词与隶属的命题值解释。这个 record 只要求载体是 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

为什么集合的等词应当是字段，而不是直接采用宿主中的路径相等？因为集合论语言把 `=` 与 `∈` 当作初始符号，而结构正是对它们意义的一次选定。两个载体元素即使作为宿主类型的元素并不相同，也可能被结构判为相等。把 `≈ˢ` 与 `∈ˢ` 做成取命题值的字段，准确写出了结构所提供的数据；这个 record 不对两种关系施加任何相容性定律。

约定全书通用：花体 `𝒮` 代表结构，`S` 代表其载体，`x`、`y`、`z` 代表载体元素，即这门语言所谈的「集合」。上标 `ˢ` 标示一个符号是**当前结构的字段**，纸面上的隶属记号一族已一字一层：库的 `∈` 表示宿主，`∈ˢ` 表示结构，对象语言中的 `∈̇` 表示语法。

这个 record 刻意只记录裸的模型论数据：要求载体是 h-集合，并给出两个命题值关系；不主张外延性、良基性或任何其他 ZF 公理。那些属于后文的模型诸章，在那里成为模型的进一步字段。

载体 `S` 是层级 `ℓ` 上的普通类型，字段 `isSetS` 要求它是 h-集合：其相等类型都是命题。这是对语言中「集合」可以是什么的唯一约束。两个关系字段取值于 `hProp ℓ`。由于 `S : Type ℓ` 与 `hProp ℓ` 都位于高一层宇宙，整个 record 的类型是 `Type (ℓ-suc ℓ)`。

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

两个关系字段给出结构的等词 `≈ˢ` 与隶属 `∈ˢ`，都是 `S → S → hProp ℓ` 型的函数。因此，`x ∈ˢ y` 是关于两个载体元素的命题。record 到此为止：载体与两个关系是数据，h-集合性是约束，并未施加集合论公理。

```agda
    _≈ˢ_ _∈ˢ_ : S → S → hProp ℓ

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

结构等词 `≈ˢ` 是字段，而不是宿主的路径相等，因此任意结构都分别提供自己的真值等词解释与成员解释，record 不施加任何相容性定律。

## 命题侧

每个结构隶属命题都有底层类型。记号 `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` 收集成一个集合，只是改变哪些对算作元素。record 的 `isSetS` 字段仍须填写，这里正是章首那条逐纤维的事实起作用：由于每个 `M x` 凭第二分量是命题，把 `isSetΣSndProp` 作用于 `isSetS` 便证明这个对类型仍是 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`。它把 `Σ≡Prop` 用于族 `λ x → (M x) .snd`，该族逐点证明 `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` 把第一投影的相等提升为限制载体中的相等。下一步是在这样的结构中解释对象语言的公式本身。