---
homepage_title: "Bedrock"
tagline: "为 𝑉 的形而上学奠基"
title: "原点"
module: Origin
lang: zh
site: "Bedrock"
description: "全书已经证明的最终成果，以及通往各项定理的阅读路线。"
stage: "开篇预览"
reading_order: 1
canonical: https://bedrock.institute/zh/index.html
html: index.html#milestones
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/Origin.lagda.md
prerequisites: []
routes: []
translations: [https://bedrock.institute/en/index.md, https://bedrock.institute/ja/index.md]
agent_guide: https://bedrock.institute/llms.txt
license: "CC-BY-NC-SA-4.0"
---


```agda
{-# OPTIONS --cubical --safe --guardedness #-}
module Origin where
```

# 原点

原点连接本书的开篇与收尾：先说明这段探索为何而来，再汇集各条证明路线最终抵达的成果。

## 前言

Bedrock 在 Cubical Agda 中形式化构建集合论，并以机器检验其证明，为关于集合宇宙的探问提供基础。首个已经完成的目标是：可构造宇宙满足 ZFC 与 GCH。全书逐步建立抵达这些成果所需的语言、模型与证明；下面的里程碑则让我们在出发前先看见终点。

这项工作的基本选择，是尽可能用宿主语言表达数学，只在公式本身成为研究对象时使用深嵌入的一阶语言。立方类型论还允许我们把累积层级构造为高阶归纳类型。这是一种数学基础的选择，并不声称元理论比所研究的理论更弱。

越过首个目标，还有关于力迫、内模型和 𝑉 的结构的问题。它们是项目的动力，而不是本书已经宣告的成果。我们的目的，是为这些探问提供经过验证的根基。

## 里程碑

**定理0** `SetChoice` 蕴含 `LEM`，而 `LEM` 蕴含 `ΩResizing`。

```agda
open import Base.Choice public using ( SetChoice→LEM )
open import Base.Classical public using ( LEM→ΩResizing )
```

**定理1** 假设 `ΩResizing`，HIT 累积层级 [V](V.Hierarchy.html#𝒮ᵥ) 是 [ZF](FOL.ZFModel.html#isZFModel) 的模型。

```agda
open import V.Model public using ( V⊨ZF )
```

**定理2** 假设 `SetChoice`，HIT 累积层级 [V](V.Hierarchy.html#𝒮ᵥ) 是 [ZFC](FOL.ZFModel.html#isZFCModel) 的模型。

```agda
open import V.Model public using ( V⊨ZFC )
```

**定理3** 假设 `LEM`，可构造宇宙 [L](L.Constructible.html#𝒮ʟ) 是 [ZFC](FOL.ZFModel.html#isZFCModel) 的模型。

```agda
open import L.Model public using ( L⊨ZFC )
```

**定理4** 假设 `LEM`，可构造宇宙 [L](L.Constructible.html#𝒮ʟ) 在内部满足[广义连续统假设](L.GCH.html#GCHStatement)。

```agda
open import L.GCH.Theorem public using ( L⊨GCH )
```