集合と交わる最初の段階

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

読書案内 · 依存マップ

本章は、内部の選択の構成のための二つの材料を提供します。第一は最小段階についての補題です。順序数の性質がはじめて成立するとき、それは最小の段階で成立します。その段階が後者であるかどうかは自動ではありません。性質は零順序数ではじめて成立するかもしれないからです。本章は、議論に必要な条件付きの形を証明します。最小の段階のほかに、切り出しが単に存在するならば、すなわちその下の順序数 δ で、後者 sucV δ ですでに性質が成立しているならば、最小の段階は後者であり、一意な直前の段階をもちます。第二の材料は上界の順序数です。構成可能な集合に対し、その集合、その要素、その要素の要素、そして塔の極限段階を同時に含む一つの順序数があります。

この材料に仕えるのは、二つの鍵による比較です。異なる段階ではじめて現れた二つの集合は、誕生の順序数だけによって比較され、それ以外の何ものによっても比較されません。同じ段階ではじめて現れた集合どうしだけが、その段階の中の名前によって比較されます。第一の材料は、それぞれの誕生の順序数を、単なる存在ではなく確定した対象にします。第二の材料は、候補の族全体が必要とする材料が一つの段階の中に住むことを保証し、名前の比較に共通の場を与えます。

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

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

module L.Choice.FirstIntersectionStage {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where

本章は一つの仮定のもとで進みます。モデルのレベルの後続での排中律の実例であり、以下の主張はすべてその設定の中でなされます。

open import FOL.ZFStructure using ( module hPropStructure )
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ; ∈-irrefl )
open import V.Model {ℓ} using ( ∈sucV-elim; self∈sucV )

本章の問いは、はじめての出現についてのものです。構成可能な集合は、いつか塔に入ります。塔の住む周囲の階層は反射しない所属をもち、だからどの順序数も自分自身を含まず、後者の性質も分かっています。順序数は自分の後者の中に坐り、後者の要素はその順序数の要素か、その順序数自身のどちらかです。

open import L.Constructible {ℓ}
  using ( IsOrd; isPropIsOrd; isL; Lset; Lset-layer; Lset-out
        ; Lset-mono; layer-trans )

構成可能の側は、塔 Lset で答えます。塔は順序数で添字づけられ、順序数は階層の集合であり、ホストの宇宙レベルではありません。順序数性 IsOrd はそれ自体命題であり、塔には層の関係、外向きの分解、単調性があり、推移性が層の間で要素を運びます。

open import L.Ordinal {ℓ} using ( mem-ord; suc-ord; bound2; ω-ord )
open import L.Ordinal.Stages {ℓ} lem using ( suc∈or≡ )
open import L.Stage {ℓ} lem
  using ( isLeastOrd; stage; stage-ord; stage-mem )
open import L.Axioms.Basic {ℓ} using ( Lset-suc )

議論を支えるのは、比較と段階です。段階の下の順序数を段階そのものと比べることが、その段階がある後者を行き過ぎていないかの判定です。順序数の要素も後者もまた順序数です。各構成可能集合はその最初の順序数を携え、順序数性と所属とともに渡され、極小性は反駁として述べられます。二つの順序数には共通の上界があります。そして後者の恒等式は、次の段階がちょうど前の段階の定義可能な部分集合であると言います。何ものかが塔に入るのは、まさにこの一歩によってです。

import Cubical.Data.Sum as Sum
import Cubical.Data.Empty as Empty
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∥_∥₁ )

議論は三つの命題の動きで書かれます。場合への分裂、空型で終わる反駁、そして存在することがだけ分かっている存在です。

open import Cubical.Data.Sigma using ( Σ≡Prop )
open import Cubical.Foundations.HLevels using ( isProp× )
open import Cubical.HITs.CumulativeHierarchy.Base using ( setIsSet )

直前の段階は、順序数と命題的な証拠との対です。この種の対は第一成分で決まり、累積階層自身も集合なので、直前の段階の等しさは順序数成分の等しさに帰着します。

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

階層の無限の構成は、フォン・ノイマンの後者 sucV と、上界に含める極限段階 ω の両方を与えます。

open hPropStructure 𝒮ᵥ

構造の所属 ∈ˢ は、順序数性も段階も極小性もその中で述べられる関係です。

最小段階の直前の段階

問いは、何かが現れる最小の段階が後者であるか、そしてどの段階を後者とするかです。最小の段階だけでは後者とは限りません。性質は零からはじまるかもしれないからです。構成が産出するのは、「下に切り出しがある」という追加の仮定のもとでの、一意な直前の段階です。

後者は、それが後者とするものを決めます。少なくとも順序数の間ではそうです。候補の直前の段階を別のものと比べると、それぞれが相手の後者に属するので、それぞれは相手の要素か等しいかのどちらかであり、二つの順序数が互いに要素であることはあり得ません。推移性から一方が自分自身の要素になるからです。そこで、与えられた順序数の直前の段階であることは命題になり、これこそが、単に存在するだけの直前の段階を確定したものとして読める理由です。

最小の段階が直前の段階をもつには、二つの入力が要ります。分けて見る価値があります。第一は最小の段階そのものです。性質が成立する順序数 σ であり、極小性は反駁として述べられます。より小さい順序数は性質をもたない、と。第二は σ での切り出しの単なる存在です。σ の下の順序数 δ で、その後者 sucV δ ですでに性質が成立しているもの。切り出しがあれば、極小性が「後者が厳密に下にとどまる」ことを排除し、行き過ぎない比較は一つの場合を残します。切り出された順序数の後者はちょうど σ である、と。ゆえに最小の段階は後者であり、切り出された順序数がその直前の段階です。切り出しなしには何も従いません。性質は零順序数ではじめて成立するかもしれず、零の下には順序数がそもそも存在しないからです。

IsPredOf : S → S → Type (ℓ-suc ℓ)
IsPredOf σ δ = IsOrd δ × (sucV δ ≡ σ)

順序数 σ の候補の直前の段階 δ とは、そのフォン・ノイマンの後者が σ 自身であるような順序数です。両方の半分が要ります。順序数性は比較が使うものであり、等式は δ を σ に釘づけするものです。

private
  cycle₂ : (a b : S) → IsOrd a → ⟨ a ∈ˢ b ⟩ → ⟨ b ∈ˢ a ⟩ → Empty.⊥
  cycle₂ a b orda a∈b b∈a = ∈-irrefl a (orda .fst a∈b b∈a)

どの順序数も、自分の要素である順序数の要素にはなれません。推移性がこの所属を二歩の循環で a 自身へ運び、非反射性と衝突するからです。この二歩の不可能性こそ、二つの順序数が互いを含むことを禁じるものです。

  mem-branch : (δ δ' : S) → IsOrd δ → ⟨ δ' ∈ˢ sucV δ ⟩ → ⟨ δ ∈ˢ δ' ⟩ → δ ≡ δ'
  mem-branch δ δ' ordδ δ'∈sδ δ∈δ' =
    ∈sucV-elim {A = δ} {x = δ'} (setIsSet δ δ') δ'∈sδ
      (λ δ'∈δ → Empty.rec (cycle₂ δ δ' ordδ δ∈δ' δ'∈δ))
      (λ δ'≡δ → sym δ'≡δ)

所属の分岐はこう読みます。δ' は δ の後者の要素であり、かつ δ は δ' の要素である。結論は δ ≡ δ' でなければなりません。もし δ' が δ 自身の要素なら、二歩の循環が閉じてしまいます。だから δ' は δ 自身であり、消去はまさにそれを返します。

ord-suc-inj : (δ δ' : S) → IsOrd δ → sucV δ ≡ sucV δ' → δ ≡ δ'
ord-suc-inj δ δ' ordδ e =
  ∈sucV-elim {A = δ'} {x = δ} (setIsSet δ δ') δ∈sδ'
    (mem-branch δ δ' ordδ δ'∈sδ)
    (λ δ≡δ' → δ≡δ')

後者の演算は順序数の上で単射です。後者の等式から、δ は sucV δ' の要素です。消去は二つの読みを示します。δ が δ' の要素なら、所属の分岐が循環を閉じて等式を与え、さもなくば δ ははじめから δ' です。後者は、それの後者とするものを決めます。

  where
  δ∈sδ' : ⟨ δ ∈ˢ sucV δ' ⟩
  δ∈sδ' = subst (λ w → ⟨ δ ∈ˢ w ⟩) e (self∈sucV δ)
  δ'∈sδ : ⟨ δ' ∈ˢ sucV δ ⟩
  δ'∈sδ = subst (λ w → ⟨ δ' ∈ˢ w ⟩) (sym e) (self∈sucV δ')

消去に渡す二つの所属は、順序数が自分の後者の中に坐るという既存の事実から、等式とその逆向きに沿って輸送したものです。

isPropPredOf : (σ : S) → isProp (Σ[ δ ∈ S ] IsPredOf σ δ)
isPropPredOf σ (δ , (ordδ , e)) (δ' , (ordδ' , e')) =
  Σ≡Prop (λ d → isProp× (isPropIsOrd d) (setIsSet (sucV d) σ))
    (ord-suc-inj δ δ' ordδ (e ∙ sym e'))

したがって、同じ順序数のどの二つの直前の段階も等しくなります。第一成分は単射性により一致し、残りのデータは命題なので、直前の段階の型全体が命題になります。これこそ、単に存在するだけの直前の段階を確定したものとして使える理由です。切り詰めを命題値の対象へほどくのは、つねに正当です。

module _ (P : S → hProp (ℓ-suc ℓ)) where

最小段階の議論は、順序数の性質ごとに一度だけ書かれます。性質はパラメータであり、以下のどこでもその内側を読むことはありません。

  Carved : S → Type (ℓ-suc ℓ)
  Carved σ = Σ[ δ ∈ S ] (⟨ δ ∈ˢ σ ⟩ × ⟨ P (sucV δ) ⟩)

σ での切り出しとは、議論が動くデータです。σ より厳密に下の順序数 δ で、その後者がすでに性質を帯びているもの。切り出しが単に存在するだけでも、最小の段階が δ のはるか上にあることはあり得ません。性質はすでに sucV δ で成立しているからです。

  private
    below-case : (σ δ : S) → isLeastOrd P σ → IsOrd δ → ⟨ P (sucV δ) ⟩
               → ⟨ sucV δ ∈ˢ σ ⟩ → sucV δ ≡ σ
    below-case σ δ least ordδ m s∈σ =
      Empty.rec (least (sucV δ) (suc-ord ordδ) m s∈σ)

下の分岐は、後者が最小の段階より厳密に下にとどまる場合を扱います。極小性は反駁として述べられており、この分岐の仮定はその前提そのものなので、least がまず矛盾を与えます。Empty.rec がその矛盾を、この分岐が負うパス sucV δ ≡ σ へ消去します。

    same-case : (σ δ : S) → sucV δ ≡ σ → sucV δ ≡ σ
    same-case σ δ e = e

等しい場合は何の仕事も要りません。この場合に渡されたのは、後者が最小の段階と等しいという同定そのものだからです。

    atCarve : (σ : S) → IsOrd σ → isLeastOrd P σ
            → Carved σ → Σ[ δ ∈ S ] IsPredOf σ δ
    atCarve σ ordσ least (δ , (δ∈σ , m)) = δ , (ordδ , suc≡σ)

atCarve は切り出しを確定した直前の段階に変えます。証人 δ はそのまま残り、その順序数性は順序数 σ への所属から回復し、sucV δ を σ に釘づけする等式が場合分析の内容です。

      where
      ordδ : IsOrd δ
      ordδ = mem-ord {A = σ} ordσ δ δ∈σ

δ の順序数性は順序数 σ から受け継がれます。順序数の要素は順序数だからです。

      suc≡σ : sucV δ ≡ σ
      suc≡σ = Sum.rec (below-case σ δ least ordδ m) (same-case σ δ)
        (suc∈or≡ δ σ ordδ ordσ δ∈σ)

δ ∈ σ のもとで、suc∈or≡ はその後者に二つの可能性だけを残します。σ より厳密に下にとどまるか、σ と等しいかです。極小性が前者を退けるので、後者が必要な等式を与えます。

  predOf : (σ : S) → IsOrd σ → isLeastOrd P σ → ∥ Carved σ ∥₁
         → Σ[ δ ∈ S ] IsPredOf σ δ
  predOf σ ordσ least = PT.rec (isPropPredOf σ) (atCarve σ ordσ least)

predOf は、存在することだけ分かっている切り出しを消費し、直前の段階を返します。切り詰められた入力は「直前の段階の型が命題である」という事実へ消去されるので、仮の切り出しの間で選択が行われることはありません。切り詰めがどの切り出しを渡しても、答えは同じ確定した直前の段階です。

  carveAt : (σ z : S) → ⟨ z ∈ˢ Lset σ ⟩
          → ((δ : S) → ⟨ z ∈ˢ Lset (sucV δ) ⟩ → ⟨ P (sucV δ) ⟩)
          → ∥ Carved σ ∥₁

carveAt は、最小の段階の要素 z から切り出しを作ります。そこには、z がどこかの後者の段階で現れるなら、性質はすでにそこで成立するという観察が伴います。これは塔への下降の形そのものです。段階への出現とは、より前の段階の定義可能冪集合の内側への出現であり、後者の恒等式により、どの定義可能冪集合も後者の段階です。

  carveAt σ z z∈Lσ k = PT.map
    (λ { (δ , (δ∈σ , z∈𝒟)) → δ , (δ∈σ
      , k δ (subst (λ w → ⟨ z ∈ˢ w ⟩) (sym (Lset-suc δ)) z∈𝒟)) })
    (Lset-out σ z z∈Lσ)

塔は z の所属を切り詰めた形で分解します。σ の下のある段階 δ で、z が Lset δ の定義可能冪集合の中にある、というものです。写像は切り詰めの内側だけで行われます。後者の恒等式を逆向きに読んで、z を 𝒟ₒ (Lset δ) から Lset (sucV δ) へ運び、観察 k がその後者で発火し、できた切り出しが切り詰めへ注入し戻されます。

集合の下方全体を収める一つの段階

この節では、段階の推移性と順序数の上界から、集合の要素、その要素の要素、そして極限段階 ω を同時に含む一つの層を得る。

構成にはもう一つ、上界が要ります。それを得るのに比較は関わりません。段階は推移的であり、集合の段階はすでにその要素を、その次にはその要素の要素を収めています。最初の段階も他の段階と同じ段階なので、それで足ります。

もう一つ確定すべき順序数は、塔の極限段階です。先の比較は対象言語で書かれ、各アリティの無定数の論理式 Formula ⊥* n の符号は、いずれも Lset ω に属します。そのような符号は自由変数をもち得るので、これらは文ではなく論理式です。後者の段階の要素の完全な名前は、符号より多くを語ります。アリティと、より前の段階から取ったパラメータのベクトルも名指すのです。ここで作る界が覆うのは符号のほうで、ω ∈ β と単調性が Lset ω を Lset β へ持ち上げます。パラメータが界の下にあるのは別の理由によるもので、次の事実がまさにそれを記録します。集合の要素とその要素の要素が同じ層に落ちる、と。

stage-below : (a : S) (p : ⟨ isL a ⟩) (x : S) → ⟨ x ∈ˢ a ⟩
            → ⟨ x ∈ˢ Lset (stage a p) ⟩
stage-below a p x x∈a =
  layer-trans (Lset-layer (stage a p)) x∈a (stage-mem a p)

段階は推移的であり、a の最初の段階もまた段階です。だから a の要素 x は、塔の a 自身の段階での層の中にあります。推移性が所属を、集合からその集合を収める層へ運ぶのです。

stage-below₂ : (a : S) (p : ⟨ isL a ⟩) (x y : S) → ⟨ y ∈ˢ x ⟩ → ⟨ x ∈ˢ a ⟩
             → ⟨ y ∈ˢ Lset (stage a p) ⟩
stage-below₂ a p x y y∈x x∈a =
  layer-trans (Lset-layer (stage a p)) y∈x (stage-below a p x x∈a)

推移性を二度適用すれば、二層下まで届きます。a の要素の要素も同じ層の中にあります。それは x に属し、x はその層に属するからです。

stageBound : (a : S) (p : ⟨ isL a ⟩)
           → Σ[ β ∈ S ] (IsOrd β × ⟨ ω ∈ˢ β ⟩ × ⟨ stage a p ∈ˢ β ⟩)
stageBound a p = bound2 ω (stage a p) ω-ord (stage-ord a p)

支配されなければならない二つの順序数は、極限段階 ω と集合自身の最初の段階です。bound2 は両方の上にある一つの順序数を、その順序数性の証明とともに返します。

bound-below₂ : (a : S) (p : ⟨ isL a ⟩) (x y : S) → ⟨ y ∈ˢ x ⟩ → ⟨ x ∈ˢ a ⟩
             → ⟨ y ∈ˢ Lset (stageBound a p .fst) ⟩
bound-below₂ a p x y y∈x x∈a =
  Lset-mono (stageBound a p .snd .snd .snd) (stage-below₂ a p x y y∈x x∈a)

塔の単調性が、二層下の事実を最初の段階から、界順序数の段階へ引き上げます。今や一つの層が、a とその要素、その要素の要素、そして比較が読む論理式の符号を同時に収めます。

まとめ

本章の再利用可能な成果は、最小段階が後者である場合のその一意な直前の段階と、選択の構成を支えるのに十分な上界順序数です。最小段階の補題は条件付きであり、その条件こそが内容です。順序数の性質の最小の段階を σ とすると、性質は零順序数ではじめて成立してもよく、そのときは下に切り出すべきものが何もありません。σ での切り出しが単に存在するならば、すなわち σ の下の順序数で、その後者がすでに性質をもつものがあれば、carveAt がそれを作り、predOf が isPropPredOf で切り詰めを閉じて、それを一意な直前の段階に変えます。後者がその後者とするものを決める理由は ord-suc-inj です。stageBound が上界の順序数を供給します。それは集合自身の段階の上にあり、したがってその要素やそのまた要素の上にあり、塔の極限段階、すなわち論理式の符号が住む段階の上にもあります。