---
title: "L における無限公理"
module: L.Axioms.Infinity
lang: ja
site: "Bedrock"
description: "L における無限公理"
stage: "構成可能段階と公理"
reading_order: 39
canonical: https://bedrock.institute/ja/L.Axioms.Infinity.html
html: L.Axioms.Infinity.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/Axioms/Infinity.lagda.md
prerequisites: [Base.Prelude, Base.Classical, FOL.ZFStructure, FOL.ZFModel, L.Constructible, L.Ordinal, L.Ordinal.Stages, L.Axioms.Basic, L.Axioms.Numerals]
routes: [constructible-axioms]
translations: [https://bedrock.institute/en/L.Axioms.Infinity.md, https://bedrock.institute/zh/L.Axioms.Infinity.md]
agent_guide: https://bedrock.institute/llms.txt
license: "CC-BY-NC-SA-4.0"
---


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

# L における無限公理

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

このモジュールが取る仮定は `lem : LEM (ℓ-suc ℓ)` の一つだけである。これは作業レベル ℓ の一つ上のレベルの命題に対する判定である。本章で必要なものは、構成的であるか、この一つのパラメータから導かれるかのどちらかなので、以降の証明は、どの段階が古典的かという正確な勘定をもって読める。

```agda
module L.Axioms.Infinity {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where
```

```agda
open import FOL.ZFStructure using ( module hPropView )
import FOL.ZFModel
open import L.Constructible {ℓ} using ( 𝒮ʟ; isL )
open import L.Ordinal {ℓ} using ( suc-ord; ω-ord )
open import L.Ordinal.Stages {ℓ} lem using ( ord∈Lset-suc )
open import L.Axioms.Basic {ℓ} using ( uniqueL )
open import L.Axioms.Numerals {ℓ} using ( numeralL; numeralL-fst )
```

`L` の内部で構成的に定義された数項列 `numeralL` は、各自然数に一つの内部数項を与える。しかし、互いに別々の集合からなる数項列は、まだ無限集合ではない。無限公理が求めるのは、要素が数項ちょうどである一つの構成可能集合である。この章ではその集合を示し、あわせて候補の集合を構成可能階層へ置くために用いる古典的依存関係を明らかにする。ω のような順序数が構成可能階層のどの段階に現れるかを知ることは順序数の比較であり、インポートされた段階定理はその比較を用いるため、モジュールパラメータ `lem` を受け取る。

周囲の集合階層は `ω` と後者 `sucV` を与え、`numeralL-fst` は各内部数項を `ω` の対応する要素に結びつける。`lem` で具体化した段階定理 `ord∈Lset-suc` は、順序数をその後者段階に置く。以下の証明が排中律をパラメータとする結果を用いるのはこの箇所である。

命題的切り詰めは単なる存在を表し、`∣_∣₁` は与えられた証人をその切り詰めに入れる。`⇔toPath` は真理値間の二つの含意を真理値間のパスに変換し、集合の仕様が要求する形を与える。

ここでの真理値は `hProp` の組であり、その添字付き選言 `∃[ x ] P x` は、ある台にわたる単なる存在を表す。構成可能構造 `𝒮ʟ` では、`∈ˢ` は所属を、`≈ˢ` は構造の等しさを表し、その基礎にある等式は周囲の集合の等式である。

```agda
open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( module InfinitySet )
open InfinitySet using ( sucV; ω )

open hPropView 𝒮ʟ
```

最後に、`SetOf` はクラスの実現者の型を指す。すなわち、構成可能集合と、すべての要素についてその所属の真理値がクラスの値に等しいことの証明を組にしたものである。モデル record の無限フィールドはこの型の可縮性を要求し、`uniqueL` が単独の実現者からそれを供給する。

```agda
module ModelL = FOL.ZFModel 𝒮ʟ
open ModelL using ( SetOf )
```

## 数項列を集合に集める

周囲の集合 `ω` の要素はライブラリの数項なので、これが自然な候補である。その構成可能性の証明は `ord∈Lset-suc` を `ω` に適用し、このインポートされた段階定理をモジュールのパラメータ `lem` で具体化する。数項列とその要素の仕様の定義自体は、このパラメータを呼び出さない。

命題 `ω∈L` は、`isL` の定義が定める切り詰められた形を取る。切り詰める前の証人の一つは段階 `sucV ω` である。`ω-ord` は `ω` が順序数であることを、`suc-ord` はそのフォン・ノイマン後者 `sucV ω` も順序数であることを述べ、`ord∈Lset-suc` が `ω` をその段階に置く。要素 `ωʟ` は周囲の集合 `ω` とこの構成可能性の証明を組にするので、`x ∈ˢ ωʟ` はその基礎にある周囲の集合への所属である。

```agda
ω∈L : ⟨ isL ω ⟩
ω∈L = ∣ sucV ω , (suc-ord ω-ord , ord∈Lset-suc ω ω-ord) ∣₁

ωʟ : S
ωʟ = ω , ω∈L
```

残る作業は、`ωʟ` の要素が内部の数項ちょうどであることを確かめることである。クラス `isNumeralL` は要素 `x` について、ある自然数 `n` に対して `x` が数項列の第 `n` 項と構造的に等しいと述べる。索引付き選言として、これはどれかの添字が機能することを単に主張するのであって、ひとつを選ぶことはしない。仕様 `ω-specL` は次に、`ωʟ` への所属と `isNumeralL` が真理値として各点で一致することを証明し、`hasInfinityL` がこの実現者を、公理フィールドが要求する可縮性へ持ち上げる。仕様の両方向は、同じ二つの素材、すなわち `ω` への所属の周囲での特徴づけと、数項列の射影方程式 `numeralL-fst` を通る。

クラス `isNumeralL` は、台 `Lift ℕ` の上で、命題の族 `x ≈ˢ numeralL (lower n)` を選言する。`Lift` に一言ふれておく。`∃[ x ] P x` は台が作業レベルに住むことを要求するが、`ℕ` は `ℓ-zero` に住む。lift はまったく同じ要素を持つ純粋なレベル調整であり、`lower` が普通の添字を取り戻す。仕様 `ω-specL` は目標を真理値の間のパス `(x ∈ˢ ωʟ) ≡ isNumeralL x` として述べ、`⇔toPath` はこのパスの証明を二つの含意の証明に帰着させる。

```agda
isNumeralL : S → hProp (ℓ-suc ℓ)
isNumeralL x = ∃[ n ∶ Lift {ℓ-zero} {ℓ-suc ℓ} ℕ ] x ≈ˢ numeralL (lower n)

ω-specL : (x : S) → (x ∈ˢ ωʟ) ≡ isNumeralL x
ω-specL x = ⇔toPath
  (map₁ (λ { (k , p) → lift (lower k)
```

両方向とも、証人を命題的切り詰めの内部に保ったまま写す。順方向では、持ち上げられた添字を `k : Lift ℕ` とし、`n = lower k` と置く。`ω` への周囲の所属から `p : # n ≡ x .fst` が得られ、`sym p ∙ sym (numeralL-fst n)` が `x ≈ˢ numeralL n` を証明する。逆方向では、`q : x .fst ≡ (numeralL n) .fst` からパス `sym (q ∙ numeralL-fst n) : # n ≡ x .fst` を作り、必要な周囲の所属の証人を得る。したがって `ωʟ` の要素は内部数項ちょうどである。最後に `uniqueL` は明示的な実現者 `(ωʟ , ω-specL)` を可縮性の中心とし、その中心から任意の他の実現者へのパスを与えて、`SetOf isNumeralL` が可縮であることを証明する。

```agda
             , (sym p ∙ sym (numeralL-fst (lower k))) }))
  (map₁ (λ { (n , q) → lift (lower n)
             , (sym (q ∙ numeralL-fst (lower n))) }))

hasInfinityL : isContr (SetOf isNumeralL)
hasInfinityL = uniqueL isNumeralL (ωʟ , ω-specL)
```

## まとめ

構成可能集合 `ωʟ` は数項列 `numeralL` をちょうど集める。明示的な実現者と外延的一意性が、無限公理のフィールドに必要な可縮性を与える。証明は `ω` の構成可能性を示す際に `ord∈Lset-suc` を通じて排中律のパラメータを使い、要素の仕様そのものは上の二つの射影パスから従う。