---
title: "マイルストーン"
module: Milestones
lang: ja
site: "Bedrock"
description: "本書で証明された到達点と、各定理へ至る読書ルート。"
stage: "最終定理の展望"
reading_order: 1
canonical: https://bedrock.institute/ja/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/zh/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 )
```