---
title: "可构造宇宙是 ZFC 的模型"
module: L.Model
lang: zh
site: "Bedrock"
description: "可构造宇宙是 ZFC 的模型"
stage: "典范良序与选择公理"
reading_order: 85
canonical: https://bedrock.institute/zh/L.Model.html
html: L.Model.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/Model.lagda.md
prerequisites: [Base.Prelude, Base.Classical, FOL.ZFStructure, FOL.ZFModel, L.Constructible, L.Axioms.Basic, L.Axioms.Numerals, L.Axioms.Infinity, L.Axioms.Full, L.Axioms.Power, L.Choice.Transversal]
routes: [choice-completion]
translations: [https://bedrock.institute/en/L.Model.md, https://bedrock.institute/ja/L.Model.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# 可构造宇宙是 ZFC 的模型

可构造结构 `𝒮ʟ` 满足 ZF 的全部公理，而它的典范良序进一步给出选择公理。所得陈述分别记作 `L⊨ZF` 与 `L⊨ZFC`。两者都在立方 Agda 中证明，只采用一项明确声明的排中律实例，其层级与模型的命题宇宙相同。

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

open import Base.Prelude
open import Base.Classical using ( LEM )

module L.Model {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where

open import FOL.ZFStructure using ( module hPropStructure )
```

这是一项语义形式的相对一致性结果。宿主元理论构造外围层级及其可构造子结构，并在后者中逐项验证公理。因此，本章并不声称无条件的一致性；它相对于承载形式化的元理论给出一个 ZFC 模型。

```agda
import FOL.ZFModel
open import L.Constructible {ℓ} using ( 𝒮ʟ )
open import L.Axioms.Basic {ℓ}
  using ( extensionalL; regularityL; hasEmptyL; hasPairL; hasUnionL )
open import L.Axioms.Numerals {ℓ}
```

基本集合运算与数词以构造方式得到。无穷、分离、替换、幂集以及可构造选择定理的证明则使用所选的排中律实例。这一区分准确标出了经典推理进入模型的位置。

```agda
  using ( numeralL; numeralL-zero; numeralL-suc )
open import L.Axioms.Infinity {ℓ} lem using ( hasInfinityL )
open import L.Axioms.Full {ℓ} lem using ( hasSeparationL; hasReplacementL )
open import L.Axioms.Power {ℓ} lem using ( hasPowerL )
open import L.Choice.Transversal {ℓ} lem using ( hasChoiceL )
```

## ZF 模型

模型结构汇集十二项已经验证的条款。外延、公理基础、空集、配对与并集是 `L` 的构造性性质；分离与替换给出两个公式模式；幂集章与无穷章给出相应的集合；三个数词条款则确定模型内部的自然数序列。

```agda
open hPropStructure 𝒮ʟ

module ModelL = FOL.ZFModel 𝒮ʟ
open ModelL using ( isZFModel; isZFCModel )
L⊨ZF : isZFModel
L⊨ZF = record
```

记录的前五个字段陈述基本的结构性质与集合构造原理。每个字段都填入此前对同一成员结构证明的定理，因而它们对集合、成员关系与公式采用同一种解释。

```agda
  { extensional    = extensionalL
  ; regularity     = regularityL
  ; hasEmpty       = hasEmptyL
  ; hasPair        = hasPairL
  ; hasUnion       = hasUnionL
```

接下来的字段加入分离、替换、幂集以及数词的零条款。两个公理模式量化在同一结构中解释的公式，而幂集字段确定模型自身的幂集运算。

```agda
  ; hasSeparation  = hasSeparationL
  ; hasReplacement = hasReplacementL
  ; hasPower       = hasPowerL
  ; numeral        = numeralL
  ; numeral-zero   = numeralL-zero
```

数词的后继方程与无穷集合的存在补全最后两个字段。记录至此闭合，`L⊨ZF` 已经证明可构造结构满足完整的 ZF。

```agda
  ; numeral-suc    = numeralL-suc
  ; hasInfinity    = hasInfinityL }
```

## 加入选择公理

`isZFCModel` 由一个 ZF 模型和在该模型中解释的选择陈述组成。可构造良序定理为 `L⊨ZF` 给出选择公理；特别地，该陈述中的交集正是由这一 ZF 结构导出的交集。加入这份证明便得到 `L⊨ZFC`。因此，在已经声明的排中律假设下，ZFC 的每条公理都作为定理成立。

```agda
L⊨ZFC : isZFCModel
L⊨ZFC = record { zf = L⊨ZF ; hasChoice = hasChoiceL L⊨ZF }
```