---
homepage_title: "Bedrock"
tagline: "𝑉 の形而上学のために基礎を築く"
title: "原点"
module: Origin
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/Origin.lagda.md
prerequisites: []
routes: []
translations: [https://bedrock.institute/en/index.md, https://bedrock.institute/zh/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 )
```