---
title: "里程碑"
module: Milestones
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/Milestones.lagda.md
prerequisites: []
routes: []
translations: [https://bedrock.institute/en/index.md, https://bedrock.institute/ja/index.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# 里程碑

本页汇集全书已经证明的最终成果，也为通往这些成果的阅读路线提供简明入口。每一项先用传统数学书的语言陈述定理，再直接导入证明它的 Agda 声明。

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

module Milestones where
```

**定理1** 在排中律假设下，宿主层 `V` 是 ZF 的模型。

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

**定理2** 在宿主层选择公理的假设下，宿主层 `V` 是 ZFC 的模型。

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

**定理3** 在排中律假设下，可构造宇宙 `L` 是 ZFC 的模型。

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

**定理4** 在排中律假设下，可构造宇宙 `L` 在内部满足广义连续统假设。

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