この章を読むか、対話型目次と依存グラフで別のルートを選べます。

対話型目次 · 依存グラフ

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

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

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

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

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

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

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

open hPropView 𝒮ʟ

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

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

数項列を集合に集める

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

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

ω∈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 はこのパスの証明を二つの含意の証明に帰着させる。

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 が可縮であることを証明する。

             , (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 を通じて排中律のパラメータを使い、要素の仕様そのものは上の二つの射影パスから従う。