L における無限公理

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

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

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

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

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

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

open import FOL.ZFStructure using ( module hPropStructure )
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 )

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

open import L.Axioms.Basic {ℓ} using ( uniqueL )
open import L.Axioms.Numerals {ℓ} using ( numeralL; numeralL-fst )

import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∣_∣₁ )
open import Cubical.Functions.Logic using ( ⇔toPath )

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

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

open hPropStructure 𝒮ʟ

最後に、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
  (PT.map (λ { (k , p) → lift (lower k)

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

             , (sym p ∙ sym (numeralL-fst (lower k))) }))
  (PT.map (λ { (n , q) → lift (lower n)
             , (sym (q ∙ numeralL-fst (lower n))) }))

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

まとめ

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