構成可能階層の中で順序数を位置付ける

この章を読むか、読書案内と依存マップで別のルートを選べます。

順序数が構成可能階層に現れる位置は所属によって制御されます。順序数は自身の後者段階までに現れ、自身の階数より前には現れない。本章では両方向を示し、段階の内部で順序数を認識する有界論理式を与えます。

塔について残された問い、そして無限公理が掛かっている問いはこうです。段階を一つ与えたとき、その時点までにどの順序数が現れているのか。答えはこれ以上なく簡潔です。Lset α に属する順序数はまさに α の要素であり、したがって塔の添字とその順序数的内容は一つ一つの段階で一致し、順序数は自身の直後の段階に初めて現れます。

両方向に実質的な仕事があります。一方は、順序数が早く現れないことを述べます。すなわち Lset α に属するなら α の要素である。こちらが難しい方向で、階数を経由します。ここで階数の構成が必要になる理由です。Lset α の集合はより早い段階のある Lset β の定義可能部分集合であり、帰納法によりその要素の階数は β 未満に抑えられるので、その集合自身の階数も有界です。順序数は自身の階数と一致するからです。

もう一方は、順序数が遅く現れないことを述べます。すなわち α の各要素はすでに Lset α に属する。これは、順序数が自身の直後の段階に現れるという証明すべき主張そのものを前提にすれば、直ちに帰納法で従います。循環は見かけだけです。帰納仮説は要素に対してこの主張を与え、必要なのはその要素だけです。

両者の揃うところ、段階の順序数は単一の論理式「順序数であること」で切り出せます。この式は Δ₀ です。推移性は有界量化だけで表せるからです。よって α は Lset α の定義可能部分集合であり、後者段階を与える定義可能冪集合の節を直ちに適用できます。

本章は固定された宇宙レベル ℓ の内部で働き、集合・所属・L の段階に関するすべての議論はこのレベルで行われます。レベル ℓ-suc ℓ における排中律を仮定します。その数学的な用途は順序数の三分法だけです。二つの順序数に対し、いずれかの向きの所属または等号という場合を一つ返します。以降の結論はすべて、次節で組み立てる二つの比較補題を通じてこの古典性を受け継ぎます。

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

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

module L.Ordinal.Stages {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where

ここで二種類の語彙が出会います。周囲の階層 V からは基本の操作が来ます。集合 S 上の所属 ∈ˢ、フォン・ノイマンの後者 sucV、所属に沿った帰納法と所属の非反射性です。構成可能な側からは、段階 Lset α 自身、定義可能部分集合の層 𝒟ₒ、そして段階への所属とその定義可能冪集合への所属を結ぶ二方向 Lset-in と Lset-out が来ます。本章の主張は完全にこの交わりの中にあります。すなわち、順序数が Lset α の間のどこに位置するかを問うのです。

open import FOL.ZFStructure using ( module hPropStructure )
open import FOL.Syntax using ( Formula; var; _∈̇_; _∧̇_; ∀̇∈ )
open import FOL.LevyHierarchy using ( Δ₀; δ-∈; δ-∧; δ-∀∈ )
open import FOL.Manipulation.ConstantMapping using ( mapFo )
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ; ∈-induction; ∈-irrefl )

順序数は述語 IsOrd として登場します。集合が順序数であるのは、それが伝播的であり、かつそのすべての要素が伝播的であるとき、そのときに限ります。これはフォン・ノイマンの読み方で、順序数 α はより小さい順序数全体の集合なので、順序数がある段階に現れたかを問うことは文字どおり所属の問題です。さらに前の章からは mem-ord と suc-ord という閉包の事実、すなわち順序数の要素は順序数であり順序数の後者は順序数であることが来ます。これにより議論中の各段階の添字が必ず真の順序数であることが保たれます。

open import V.Model {ℓ} using ( ∈sucV-elim; ∈sucV-inl; self∈sucV )
open import L.Definability {ℓ} using ( module DefOf )
open import L.Constructible {ℓ}
  using ( IsOrd; isTransV; Lset; Lset-layer; layer-trans
        ; 𝒟ₒ; 𝒟ₒ-intro; 𝒟ₒ-inv; Lset-mono; Lset-in; Lset-out )

すべての背後にある判定の手続きが ord-tri です。それぞれ順序数であると証明された二つの順序数を与えると、三つの場合のうちどれが成り立つか、すなわち a ∈ b、a = b、b ∈ a のいずれかを答えます。これは上述の排中律の仮定です。三分法は三つの場合を直和として返し、不可能な枝は空型に入ります。一方、命題的切り捨て ∣_∣₁ は、段階の分解を与える先行段階が単に存在することを記録します。

open import L.Ordinal {ℓ} using ( mem-ord; suc-ord )
open import L.Ordinal.Linear {ℓ} lem using ( ord-tri )
open import L.Rank {ℓ} using ( rank; rank-upper; rank-ord; rank-fix )

open import Cubical.Data.Sum as Sum using ( _⊎_; inl; inr )
import Cubical.Data.Empty as Empty

階数は、それを構築した章から入ってきます。集合 x に対して rank x は、累積階層の中で x がどの深さに位置するかを集めた順序数です。rank-ord がそれが順序数であることを証明し、rank-fix が順序数の階数をその順序数自身と同一視し、rank-upper がその要素の階数の上界からその集合の階数の上界を与えます。この三つの事実こそ、本章の難しい方向が消費するすべてです。

import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∣_∣₁ )
open import Cubical.HITs.CumulativeHierarchy.Properties
  using ( ∈∈ₛ; ∈-asFiber; ⟪_⟫; ⟪_⟫↪; extensionality; _⊆_ )
open import Cubical.HITs.CumulativeHierarchy.Constructions

周囲での所属と段階上の論理式を結ぶために、集合 A には選ばれた提示 ⟪ A ⟫ があり、∈-asFiber は A への所属から、その要素を指す添字を与えます。相互包含からは extensionality によって集合の等号が得られます。論理式の充足は hProp で直接解釈され、各論理式が表す hProp です。これらの対応により、集合、その添字、有界論理式の間を行き来できます。

  using ( module InfinitySet )
open InfinitySet using ( sucV )

open hPropStructure 𝒮ᵥ

二つの比較原理

三分法で残る数学的な場合は三つです。a ∈ b なら a は b の後者にも属し、a = b なら a は新たな最上要素としてその後者に属します。残る b ∈ a は包含 a ⊆ b によって排除されます。

集合 a と b が a ⊆ b を満たすとし、三分性で両者を比較します。a が b の要素なら、最初の補題は ∈sucV-inl を適用します。後者は b とその一元集合の合併なので、b の要素は自動的に sucV b の要素です。a が b と等しいなら、二番目の補題は、b が自身の後者に属するという事実 self∈sucV b をパス a ≡ b に沿って輸送します。三つの場合のうち二つはすでに閉じました。

private
  ∈-case : (a b : S) → ⟨ a ∈ˢ b ⟩ → ⟨ a ∈ˢ sucV b ⟩
  ∈-case a b a∈b = ∈sucV-inl a∈b

  ≡-case : (a b : S) → a ≡ b → ⟨ a ∈ˢ sucV b ⟩
  ≡-case a b a≡b = subst (λ w → ⟨ w ∈ˢ sucV b ⟩) (sym a≡b) (self∈sucV b)

残る場合は b ∈ a ですが、包含関係がこれを排除します。b ∈ a と a ⊆ b から b ∈ b が得られ、∈-irrefl に反するからです。この矛盾から目標 a ∈ sucV b が従います。したがって順序数 a、b について、包含 a ⊆ b は a ∈ sucV b を導きます。

  wit-case : (a b : S) → ((y : S) → ⟨ y ∈ˢ a ⟩ → ⟨ y ∈ˢ b ⟩)
           → ⟨ b ∈ˢ a ⟩ → ⟨ a ∈ˢ sucV b ⟩
  wit-case a b a⊆b b∈a = Empty.rec (∈-irrefl b (a⊆b b b∈a))

⊆→∈suc : (a b : S) → IsOrd a → IsOrd b
       → ((y : S) → ⟨ y ∈ˢ a ⟩ → ⟨ y ∈ˢ b ⟩) → ⟨ a ∈ˢ sucV b ⟩

ここが古典的な順序数比較の最初の使用箇所です。三分法の結果を得た後の推論は構成的であり、下の後者に関する二つ目の比較でも同じ原理を使います。

⊆→∈suc a b orda ordb a⊆b = Sum.rec
  (∈-case a b)
  (Sum.rec (≡-case a b) (wit-case a b a⊆b))
  (ord-tri a orda b ordb)

ここで β ∈ α とします。sucV β と α を三分法で比較すると、後者が α の中にあるか、α と等しいか、または α が sucV β の中にあります。型 Out β α は最初の二つを記録し、三つ目は β ∈ α と矛盾します。

ありえない場合は overshoot の内部で排除されます。その前提は同時には成り立たない二つの事実、すなわち α が sucV β に属し、しかも β が順序数 α に属するというものです。∈sucV-elim で sucV β の要素という事実を展開すると、α ∈ β か α = β の二つの場合が出ます。この消去原理は目標が命題であることを要求しますが、空型 ⊥* はまさに命題なので、どちらの分岐も矛盾で終えることができます。

private
  Out : S → S → Type (ℓ-suc ℓ)
  Out β α = ⟨ sucV β ∈ˢ α ⟩ ⊎ (sucV β ≡ α)

  overshoot : (β α : S) → IsOrd α → ⟨ β ∈ˢ α ⟩ → ⟨ α ∈ˢ sucV β ⟩ → Out β α
  overshoot β α ordα β∈α α∈sβ = Empty.rec*

最初の小場合では所属の鎖 α ∈ β ∈ α が得られます。α の推移性、すなわち第一成分 ordα .fst はこの鎖を合成して α ∈ α を与えます。次の場合は α = β に沿って β ∈ α を逆向きに輸送し、やはり α ∈ α を得ます。どちらも ∈-irrefl に反するので、不可能な第三の場合から必要な結論 Out β α が従います。

    (∈sucV-elim {A = β} {x = α} {P = Empty.⊥* {ℓ-suc ℓ}} Empty.isProp⊥* α∈sβ
      (λ α∈β → lift (∈-irrefl α (ordα .fst α∈β β∈α)))
      (λ α≡β → lift (∈-irrefl α (subst (λ w → ⟨ w ∈ˢ α ⟩) (sym α≡β) β∈α))))

suc∈or≡ : (β α : S) → IsOrd β → IsOrd α → ⟨ β ∈ˢ α ⟩
        → ⟨ sucV β ∈ˢ α ⟩ ⊎ (sucV β ≡ α)

本命の補題は、sucV β と α の間で三分性を回します。両者とも順序数であることが証明されており、sucV β は suc-ord によるものです。最初の二つの場合はすでに求められる形、所属か相等かを備えているので、そのまま返せます。

suc∈or≡ β α ordβ ordα β∈α = go (ord-tri (sucV β) (suc-ord ordβ) α ordα)
  where
  go : (⟨ sucV β ∈ˢ α ⟩ ⊎ ((sucV β ≡ α) ⊎ ⟨ α ∈ˢ sucV β ⟩)) → Out β α
  go (inl s∈α)        = inl s∈α
  go (inr (inl s≡α))  = inr s≡α

三つ目の場合 α ∈ sucV β はまさに overshoot の前提であり、仮定の β ∈ α を渡せば場合分けは閉じます。結論 suc∈or≡ は「行き過ぎない」ことの鋭い形です。α の下では、α の要素の後者段階が α を厳しく超えることは決してありません。

  go (inr (inr α∈sβ)) = overshoot β α ordα β∈α α∈sβ

そしてこれが奉仕する先が累積の補題です。自身の後者段階に現れた順序数は、それより後のすべての段階に現れます。ここで「後」とは、添字がその順序数の上にあることを意味します。

これは「β は sucV β に現れる」という各点ごとの主張と「α の各要素は Lset α に属する」という段階ごとの主張を結ぶ橋です。β ∈ α が与えられると、後者 sucV β は α の内部にあるか α と一致し、いずれの場合もより小さい段階への所属が Lset α への所属に運ばれます。

所属の場合は段階の単調性を使います。Lset-mono は、γ ∈ δ なら Lset γ が Lset δ に含まれることを述べるので、より早い段階の要素はより後の段階の要素です。ここでは γ = sucV β、δ = α で、まさに suc∈or≡ の最初の場合です。

private
  cumul-∈ : (β α : S) → ⟨ sucV β ∈ˢ α ⟩ → ⟨ β ∈ˢ Lset (sucV β) ⟩
          → ⟨ β ∈ˢ Lset α ⟩
  cumul-∈ β α s∈α = Lset-mono {α = α} {β = sucV β} s∈α {x = β}

  cumul-≡ : (β α : S) → sucV β ≡ α → ⟨ β ∈ˢ Lset (sucV β) ⟩ → ⟨ β ∈ˢ Lset α ⟩

相等の場合は退化したものです。sucV β が厳密には下にない、つまり α と等しいときには、Lset (sucV β) への所属はすでに Lset α への所属であり、パスに沿った輸送がこれを文字どおりのものにします。Lset-cumul は二つの順序数の証明と出現の仮定を受け取り、suc∈or≡ で場合分けをします。

  cumul-≡ β α s≡α = subst (λ w → ⟨ β ∈ˢ Lset w ⟩) s≡α

Lset-cumul : (β α : S) → IsOrd β → IsOrd α → ⟨ β ∈ˢ α ⟩
           → ⟨ β ∈ˢ Lset (sucV β) ⟩ → ⟨ β ∈ˢ Lset α ⟩
Lset-cumul β α ordβ ordα β∈α β∈Lsβ =
  Sum.rec (λ s∈α → cumul-∈ β α s∈α β∈Lsβ)

結果の形に注意してください。これはすべての β ∈ α に対して β ∈ Lset α と無条件に述べているのではありません。後者段階での出現は依然として仮定だからです。最後の定理がその仮定を帰納法で供給し、この補題は仮定を段階の内容へ変えるまさにその一歩です。

          (λ s≡α → cumul-≡ β α s≡α β∈Lsβ)
          (suc∈or≡ β α ordβ ordα β∈α)

自身の階数より前に現れるものはない

集合が Lset α に属すれば、その階数は α で抑えられます。階数が自身と一致する順序数に適用すると、その順序数がより早い段階には現れないことが分かります。

こちらが難しい方向です。段階の添字についての帰納法で示します。Lset α の集合は、ある β ∈ α に対する Lset β の定義可能部分集合の中にあり、したがって Lset β の部分集合です。すると帰納仮説によりその各要素の階数は β の中にあります。その集合自身の階数、すなわちそれらの階数の後者の合併は β に含まれ、比較により β の後者の内部、ひいては α の内部に置かれます。

帰納についての記法上の一点を述べると、切り詰められた存在の要素であることはそれ自体切り詰められており、帰納は明示的な要素ではなく切り詰められた形 β ∈ᵗ α の上で述べられます。目標は所属の主張、つまり命題なので、PT.rec によるこの切り詰めの消去は正当です。

主張はすべての順序数 α にわたって量化されており、∈-induction は α の関数としての述語全体に適用され、順序数の証明は引数として携行されます。帰納は α への所属に沿って行われるので、α における帰納仮説が語るのは α の要素 β であって、何らかの順序による「より早い段階」ではありません。

rank-Lset : (α : S) → IsOrd α → (x : S) → ⟨ x ∈ˢ Lset α ⟩ → ⟨ rank x ∈ˢ α ⟩
rank-Lset = ∈-induction
  {P = λ α → IsOrd α → (x : S) → ⟨ x ∈ˢ Lset α ⟩ → ⟨ rank x ∈ˢ α ⟩} step
  where
  step : (α : S)

鍵となる一歩は、x ∈ Lset α が何を意味するかを明かすことです。Lset-out により、x はある β ∈ α の上の定義可能部分集合の層に単に (merely) 属するにすぎません。層への所属もまた切り詰められていますが、結論 rank x ∈ α は命題なので、PT.rec が切り詰めを消去し、繊維 β、β∈α、x∈𝒟ₒLβ を与えられたものとして扱えます。

       → (∀ β → β ∈ᵗ α → IsOrd β → (x : S) → ⟨ x ∈ˢ Lset β ⟩ → ⟨ rank x ∈ˢ β ⟩)
       → IsOrd α → (x : S) → ⟨ x ∈ˢ Lset α ⟩ → ⟨ rank x ∈ˢ α ⟩
  step α IH ordα x x∈Lα = PT.rec (snd (rank x ∈ˢ α)) fromStage (Lset-out α x x∈Lα)
    where
    fromStage : Σ[ β ∈ S ] (⟨ β ∈ˢ α ⟩ × ⟨ x ∈ˢ 𝒟ₒ (Lset β) ⟩) → ⟨ rank x ∈ˢ α ⟩

繊維の内部では、帰納仮説を動かすのに必要なものがすべて取り戻されます。順序数 α の要素 β は mem-ord によってそれ自身順序数であり、これこそが帰納仮説を β で発火させるものです。

    fromStage (β , β∈α , x∈𝒟ₒLβ) = rankx∈α
      where
      ordβ : IsOrd β
      ordβ = mem-ord {A = α} ordα β β∈α
      x⊆Lβ : (y : S) → ⟨ y ∈ˢ x ⟩ → ⟨ y ∈ˢ Lset β ⟩

Lset β の上での x の定義可能性は、x がその部分集合であることを意味します。𝒟ₒ-inv が証明書をほどき、DefOf.Def∋⊆A がそれを包含 x ⊆ Lset β に変えます。これを帰納仮説と組み合わせると、x の各要素 y の階数は β の中にあります。そして rank-upper は、まさにこのような要素の階数の上界を与えられれば、rank x 自身を β に含めます。

      x⊆Lβ = DefOf.Def∋⊆A (Lset β) x (𝒟ₒ-inv (Lset β) x x∈𝒟ₒLβ)
      ry∈β : (y : S) → ⟨ y ∈ˢ x ⟩ → ⟨ rank y ∈ˢ β ⟩
      ry∈β y y∈x = IH β β∈α ordβ y (x⊆Lβ y y∈x)

      rankx⊆β : (z : S) → ⟨ z ∈ˢ rank x ⟩ → ⟨ z ∈ˢ β ⟩
      rankx⊆β = rank-upper x β ordβ ry∈β

残るのは、rank x ∈ sucV β を rank x ∈ α へ持ち上げることです。rank x と β はどちらも順序数で、前者は rank-ord によるものなので、最初の節の ⊆→∈suc が両者の包含に適用され、rank x は β の後者の中に置かれます。続いて ∈sucV-elim が既知の β ∈ α と比較します。rank x が β の要素なら、α の伝播性が所属を一段押し上げ、rank x が β と等しいなら、パスが β ∈ α を直接輸送します。いずれの場合も階数は α に着地し、帰納は完成します。

      rankx∈α : ⟨ rank x ∈ˢ α ⟩
      rankx∈α = ∈sucV-elim {A = β} {x = rank x} (snd (rank x ∈ˢ α))
        (⊆→∈suc (rank x) β (rank-ord x) ordβ rankx⊆β)
        (λ rx∈β → ordα .fst rx∈β β∈α)
        (λ rx≡β → subst (λ w → ⟨ w ∈ˢ α ⟩) (sym rx≡β) β∈α)

順序数に対しては結論が単純になります。階数は順序数を固定するからです。Lset α に属する順序数は α の要素です。これが本章の特徴付けの下界を、使える形にしたものです。

この一歩は輸送です。rank-fix x ordx がパス rank x ≡ x を与え、それに沿った代入が階数の上界 rank x ∈ α を所属 x ∈ α に変えます。方向に注意してください。上の帰納法が保証するのは、段階への出現が添字への所属を強いるということで、その逆ではありません。

ord∈Lset→∈ : (α : S) → IsOrd α → (x : S) → IsOrd x → ⟨ x ∈ˢ Lset α ⟩
           → ⟨ x ∈ˢ α ⟩
ord∈Lset→∈ α ordα x ordx x∈Lα =
  subst (λ w → ⟨ w ∈ˢ α ⟩) (rank-fix x ordx) (rank-Lset α ordα x x∈Lα)

順序数であることを有界量化で表す

集合が推移的で、そのすべての要素も推移的であるという性質は、有界量化子だけで表せます。したがってこの論理式は、推移的な段階と周囲の宇宙の間で順序数を絶対的に認識します。

この述語は二つの節からなり、どちらもすでに有界です。集合が推移的であるとは、その要素の要素がすべてその要素であることであり、その要素がすべて推移的であるとは、同じ性質が一段下で成り立つことです。無界な量化子は現れないので論理式は Δ₀ であり、定数も現れないため、定数の改名の一連の操作はすべて不要になります。

添字は de Bruijn 方式です。各有界量化子は新しい変数 0 を束縛し、既存の変数を外側へ押しやるので、二つの束縛子の後では候補の順序数は添字 2 にあります。

最初の節は伝播性を述べます。その有界量化子 ∀̇∈ は、一段外で束縛された値の要素を渡ります。de Bruijn 添字で読むと、一つの束縛子の後では要素は添字 0、候補は添字 1 にあり、二つ目の束縛子の内部では原子式が y ∈ x を要求し、y は 0、x は 2 へ押しやられています。論理式は定数のアルファベット K について多形ですがどの定数も使わないので、同じ構文があらゆる解釈に奉仕します。

φ-ord : ∀ {ℓk} {K : Type ℓk} → Formula K 1
φ-ord =
  (∀̇∈ (var zero) (∀̇∈ (var zero) (var zero ∈̇ var (suc (suc zero)))))
  ∧̇
  (∀̇∈ (var zero)

二番目の節はもう一段量化子を重ねます。候補の要素 x、x の要素 y、y の要素 z は候補へ戻らねばならず、これは候補の各要素が伝播的であることを述べます。三つの束縛子の後では、最内の変数は 0、候補は 3 にあります。証明書 φ-ord-Δ₀ は同じ三種の基本的な証明書、原子式の所属に対する δ-∈、有界量化子に対する δ-∀∈、連言に対する δ-∧ から、論理式の構成に一歩ずつ対応して組み上げられます。

    (∀̇∈ (var zero) (∀̇∈ (var zero) (var zero ∈̇ var (suc (suc zero))))))

φ-ord-Δ₀ : ∀ {ℓk} {K : Type ℓk} → Δ₀ (φ-ord {K = K})
φ-ord-Δ₀ = δ-∧ (δ-∀∈ (δ-∀∈ δ-∈)) (δ-∀∈ (δ-∀∈ (δ-∀∈ δ-∈)))

一つの段階に属する順序数

有界な順序数論理式による分出は、ある段階に属する順序数をちょうど集めます。その所属の仕様は、内部と周囲の宇宙の両方で使えます。

段階を一つ固定します。推移的な段階についての有界絶対性を使うと、周囲の階層における論理式の充足は順序数述語の二つの節にちょうど展開され、二者は引数を並べ替えるだけで交換できます。すると、この式が切り出す定義可能部分集合は α 自身です。その要素はその段階の順序数なので、階数の方向により α の要素であり、逆に α の要素は、累積によってすでに現れた順序数なので、この式を充足します。

累積には、α の各要素が自身の後者段階で現れることが必要です。それはこの定理自身の結論なので、ここでは仮定として入り、次の節の帰納法がまさにそれを供給します。

順序数 α とその証明を固定します。段階 A = Lset α は層であり、layer-trans がそれを集合としての A の伝播性へ引き上げます。Δ₀ 論理式が A の内部の充足と周囲の宇宙の間で絶対的であるための前提は、これが唯一です。L.Definability の章の定義可能性の機構は A に対して開かれているので、以下の defSet φ は常に φ が A から定義する部分集合を意味します。

module OrdAt (α : S) (ordα : IsOrd α) where
  private
    A = Lset α
    Atrans = layer-trans (Lset-layer α)
    module DefA = DefOf A

A の要素は繊維 ⟪ A ⟫ を通して現れます。添字 m が A の要素 ⟪ A ⟫↪ m を名指すのです。論理式 φ は φ-ord を台 ⟪ A ⟫ 上に実例化したもので、自由変数の枠を一つ持ち、環境 ⟪ A ⟫↪ m ∷ [] がそれを占めます。φ は定数を含まないので、mapFo DefA.ι φ は定数の解釈 ι を通した改名にすぎず、この論理式については構文的には何も変えません。ここの充足記号 ⊨ᵛ は、絶対性の精緻化が与える周囲の充足です。

    module RefA = DefA.Refine Atrans
    open RefA.Abs using ( _⊨ᵛ_ )

    φ : Formula ⟪ A ⟫ 1
    φ = φ-ord {K = ⟪ A ⟫}

  ⊨ᵛ→ord : (m : ⟪ A ⟫) → ⟨ (⟪ A ⟫↪ m ∷ []) ⊨ᵛ (mapFo DefA.ι φ) ⟩

最初の方向は、充足を順序数述語へと読み込みます。連言の充足は対であり、その第一成分は、提示された要素 x = B に対する最初の有界節の適用にほかなりません。x ∈ B かつ y ∈ x なるすべての y が B へ戻る、というものです。これは B の伝播性の逐語的な表述なので、この対の第一射影は B が伝播的である証明になります。

         → IsOrd (⟪ A ⟫↪ m)
  ⊨ᵛ→ord m sat = transB , memTransB
    where
    B = ⟪ A ⟫↪ m
    transB : isTransV B

第二成分は二番目の節で、量化子がもう一段深く入れ子になります。x ∈ B、y ∈ x、z ∈ y に対して要素 z は B へ戻る。これは B の各要素 x がそれ自身伝播的であることをまさに述べるので、第一射影と合わせて、充足のデータは B に対する IsOrd の証明にほかなりません。

    transB {x} {y} y∈x x∈B = sat .fst x x∈B y y∈x
    memTransB : (x : S) → ⟨ x ∈ˢ B ⟩ → isTransV x
    memTransB x x∈B {y} {z} z∈y y∈x = sat .snd x x∈B y y∈x z z∈y

  ord→⊨ᵛ : (m : ⟪ A ⟫) → IsOrd (⟪ A ⟫↪ m)
         → ⟨ (⟪ A ⟫↪ m ∷ []) ⊨ᵛ (mapFo DefA.ι φ) ⟩

逆向きの方向は、順序数の証明から充足を組み立てます。その第一成分は x ∈ B と y ∈ x を受け取り y ∈ B を返さねばなりませんが、IsOrd の対の第一成分、つまり B の伝播性が、引数を正しい順に並べてまさにそれを行います。

  ord→⊨ᵛ m ord = c1 , c2
    where
    B = ⟪ A ⟫↪ m
    c1 : (x : S) → ⟨ x ∈ˢ B ⟩ → (y : S) → ⟨ y ∈ˢ x ⟩ → ⟨ y ∈ˢ B ⟩
    c1 x x∈B y y∈x = ord .fst y∈x x∈B

第二成分は三つの所属を B へとつなげる必要があり、IsOrd の対の二番目の節はこの連鎖そのものです。したがって φ の充足と順序数述語は両方向で交換可能です。二つの表現は同じ数学的条件を述べています。この同値を得ると、主張が形を成します。φ が選ぶ定義可能部分集合は α に等しい、というもので、二つの包含から extensionality で証明され、α の各要素がすでに A に現れているという明示的な仮定 α⊆A のもとで述べられます。

    c2 : (x : S) → ⟨ x ∈ˢ B ⟩ → (y : S) → ⟨ y ∈ˢ x ⟩
       → (z : S) → ⟨ z ∈ˢ y ⟩ → ⟨ z ∈ˢ x ⟩
    c2 x x∈B y y∈x z z∈y = ord .snd x x∈B z∈y y∈x

  defSet-φ-ord : ((β : S) → ⟨ β ∈ˢ α ⟩ → ⟨ β ∈ˢ A ⟩) → DefA.defSet φ ≡ α
  defSet-φ-ord α⊆A = extensionality (DefA.defSet φ) α (sub₁ , sub₂)

定義可能部分集合から α への包含は、本章の階数の方向が真価を発揮する場所です。定義可能部分集合への所属は ∈∈ₛ によって提示のレベルの事実へ展開されるので、sub₁ は、y が defSet φ に単に (merely) 属するという証明とともに y を受け取り、y ∈ α を作り出さねばなりません。

    where
    sub₁ : ⟨ DefA.defSet φ ⊆ α ⟩
    sub₁ y y∈ₛ = ∈∈ₛ {a = y} {b = α} .fst
      (y∈α (∈∈ₛ {a = y} {b = DefA.defSet φ} .snd y∈ₛ))
      where

ここでは三つの変換が積み重なります。定義可能部分集合への y の所属は、部分集合が段階に含まれるため defSet⊆A によって A への所属を与えます。次に繊維 ∈-asFiber がその周囲の所属をその表示に置き換えます。添字 m とパス q で、これらは単に (merely) 存在するにすぎません。

      y∈α : ⟨ y ∈ˢ DefA.defSet φ ⟩ → ⟨ y ∈ˢ α ⟩
      y∈α y∈def = ord∈Lset→∈ α ordα y ordy y∈A
        where
        y∈A = DefA.defSet⊆A φ y y∈def
        fib = ∈-asFiber {a = y} {b = A} y∈A

パス q は y の所属を提示された要素 ⟪ A ⟫↪ m の所属へ輸送します。φ は Δ₀ で A は推移的なので、abs-defSet は defSet φ への所属という hProp と、一要素の環境における mapFo ι φ の周囲での充足という hProp を同一視します。これらのパスに沿った置換から必要な sat が得られます。パス輸送そのものは、対象が命題であることを要求しません。

        m = fib .fst
        q = fib .snd
        sat : ⟨ (⟪ A ⟫↪ m ∷ []) ⊨ᵛ (mapFo DefA.ι φ) ⟩
        sat = subst ⟨_⟩ (RefA.abs-defSet φ φ-ord-Δ₀ m)
                (subst (λ w → ⟨ w ∈ˢ DefA.defSet φ ⟩) (sym q) y∈def)

sat から、含意 ⊨ᵛ→ord が提示された要素の IsOrd 証明を返し、q に沿った輸送がそれを y 自身の証明に変えます。次に ord∈Lset→∈、つまり階数の方向が、y を α の中に置きます。よって定義可能部分集合の任意の要素はその段階の順序数であり、段階の添字がそれを含みます。

        ordy : IsOrd y
        ordy = subst IsOrd q (⊨ᵛ→ord m sat)

    sub₂ : ⟨ α ⊆ DefA.defSet φ ⟩
    sub₂ y y∈ₛ = ∈∈ₛ {a = y} {b = DefA.defSet φ} .fst
      (y∈def (∈∈ₛ {a = y} {b = α} .snd y∈ₛ))

逆向きの包含は、同じ回路を逆にたどります。α の要素 y は、mem-ord による順序数の証明をすでに手にした状態でやって来ます。仮定 α⊆A が繊維 m、q を通して y を段階の内部に提示し、ord→⊨ᵛ がその環境における φ の周囲の充足を与えます。

      where
      y∈def : ⟨ y ∈ˢ α ⟩ → ⟨ y ∈ˢ DefA.defSet φ ⟩
      y∈def y∈α = subst (λ w → ⟨ w ∈ˢ DefA.defSet φ ⟩) q
        (subst ⟨_⟩ (sym (RefA.abs-defSet φ φ-ord-Δ₀ m)) sat)
        where

絶対性が今度は逆方向へ変換します。Δ₀ 論理式の周囲の充足は ⟪ A ⟫↪ m の defSet φ への所属であり、q に沿った輸送がその所属を y 自身の上に、定義可能部分集合の内部に着地させます。どの場所でも選択は行われません。各繊維 m、q は、それを生んだまさにその y の上で、局所的に使われるだけです。

        ordy = mem-ord {A = α} ordα y y∈α
        y∈A = α⊆A y y∈α
        fib = ∈-asFiber {a = y} {b = A} y∈A
        m = fib .fst
        q = fib .snd

二つの包含が閉じ、defSet-φ-ord が結論を述べます。有界論理式が Lset α から切り出す部分集合は、まさに α である、と。ここまでのすべては α⊆A を条件とします。次の節がこの条件を取り除き、本章の主定理がそこに収まります。

        sat : ⟨ (⟪ A ⟫↪ m ∷ []) ⊨ᵛ (mapFo DefA.ι φ) ⟩
        sat = ord→⊨ᵛ m (subst IsOrd (sym q) ordy)

順序数は自身の後者段階に現れる

各順序数は、有界な順序数論理式によって選ばれる自身の定義可能部分集合である。したがって α は Lset α の定義可能冪集合、すなわち後者段階に属する。

残る溝は、前節で仮定せざるを得なかった包含 α ⊆ Lset α である。これは所属に関する帰納法で埋める。帰納法の仮定は、α の各要素 β に対して定理そのものを与える。すなわち β は Lset (sucV β) に現れ、第一節の累積補題によって Lset α へ持ち上げられる。すべての要素が累積し終えると、論理式が Lset α から α を分出し、次の段階の定義における和の一つの枝がこれを含む。循環は見かけにすぎない。帰納法の仮定が扱うのは α 自身ではなく要素だからである。

帰納法の前に二つの小事実をまとめておく。一つ目は定義可能冪集合から段階への一方通行の橋である。α が 𝒟ₒ (Lset α) に属する、すなわち α が Lset α の定義可能部分集合であるという証明は、α が自身の後者に属することを述べる self∈sucV α と合わせて、Lset-in が必要とするデータそのものである。二行目からは定理そのものが始まり、所属に関する帰納法の原理を直接適用する。帰納法で示される命題は、各順序数へ相対化された定理そのものだ。

private
  𝒟ₒ→Lset-suc : (α : S) → ⟨ α ∈ˢ 𝒟ₒ (Lset α) ⟩ → ⟨ α ∈ˢ Lset (sucV α) ⟩
  𝒟ₒ→Lset-suc α α∈𝒟ₒ = Lset-in (sucV α) α α (self∈sucV α) α∈𝒟ₒ

ord∈Lset-suc : (α : S) → IsOrd α → ⟨ α ∈ˢ Lset (sucV α) ⟩
ord∈Lset-suc = ∈-induction

帰納段は、α の各要素 β に対して定理の β における結論を受け取り、α における結論を組み立てなければならない。前節がすでに目標を唯一の仮定 α ⊆ Lset α に帰着させているため、この段がするのはその包含を組み立てて橋の補題に渡すことだけである。α が順序数であることと帰納法の仮定のほかには何も使わない。

  {P = λ α → IsOrd α → ⟨ α ∈ˢ Lset (sucV α) ⟩} step
  where
  step : (α : S) → (∀ β → β ∈ᵗ α → IsOrd β → ⟨ β ∈ˢ Lset (sucV β) ⟩)
       → IsOrd α → ⟨ α ∈ˢ Lset (sucV α) ⟩
  step α IH ordα = 𝒟ₒ→Lset-suc α α∈𝒟ₒ

包含は要素ごとに組み立てられる。α の各 β に対し、順序数 α の要素であることで β 自身も順序数となり、帰納法の仮定がそれを Lset (sucV β) に置く。第一節の累積補題は、sucV β が α に属するか等しいかというちょうどこの形のために設計されたもので、それによって β は Lset α へ持ち上げられる。前の二つの比較補題がここで効いてくる。場合分けは一度で全要素を同時に扱う。

    where
    α⊆A : (β : S) → ⟨ β ∈ˢ α ⟩ → ⟨ β ∈ˢ Lset α ⟩
    α⊆A β β∈α = Lset-cumul β α ordβ ordα β∈α (IH β β∈α ordβ)
      where
      ordβ = mem-ord {A = α} ordα β β∈α

α ⊆ Lset α が手に入れば、前節の結論がそのまま使える。φ-ord が Lset α から選び出す定義可能部分集合は α 自身である。証明は切り詰めによって単に与えられればよい。𝒟ₒ の要素は何らかの定義論理式と一致の証明を必要とするだけであり、φ-ord と OrdAt の外延性の議論の対がまさにそのような証拠になる。橋の補題が続いて α を Lset (sucV α) へ移し、帰納法と定理が同時に完成する。

    α∈𝒟ₒ : ⟨ α ∈ˢ 𝒟ₒ (Lset α) ⟩
    α∈𝒟ₒ = 𝒟ₒ-intro (Lset α) α
      ∣ φ-ord {K = ⟪ Lset α ⟫} , OrdAt.defSet-φ-ord α ordα α⊆A ∣₁

まとめ

これで順序数の段階の上限が正確になった。α は Lset (sucV α) に現れ、Lset β に現れるなら α ∈ β である。有界な順序数論理式により、後の内部議論でこれらの事実を利用できる。

ord∈Lset-suc は順序数が自身の後者の段階に現れることを述べ、ord∈Lset→∈ はそれより早くは現れないことを述べる。二者を合わせると、Lset α の順序数は α の要素ちょうどである。本章は第一節の二つの比較を通して古典的であり、それ以外に使ったものはすべて構成的であった。モジュール L.Stage はこの結果を ω に適用し、無限公理の証明を完成させる。