後者演算について閉じた順序数段階の数項

有限順序数は論理式コードに用いる数項を与えます。本章では、段階の順序数添字が零を含み、後者演算について閉じていれば、すべての数項がその段階に属することを示します。まず各順序数をその後者の段階に含む単調な段階族を扱い、その結果を構成可能階層に適用します。

本章は宇宙レベル ℓ を固定し、レベル ℓ-suc ℓ の排中律を明示的なパラメータ lem として受け取ります。数項を順序数の内部へ入れる初等的な帰納法はこれを用いません。この仮定を持ち回るのは、構成可能な場合への特化に必要な素材、すなわち順序数がその後者を添字とする段階に現れるという定理が、古典的な順序数段階の章に由来するからです。

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

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

module L.Coding.NumeralBound {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where

数項の二つの表現を区別します。周囲の数項 # k は V ℓ の有限 von Neumann 順序数であり、模型の数項 numeralL k は底集合が # k である L の要素です。まず周囲の順序数について上界を証明し、その後で射影等式 numeralL-fst により模型での表現へ結果を移します。

open import FOL.ZFStructure using ( module hPropStructure )
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )
open import L.Constructible {ℓ} using ( IsOrd; Lset; Lset-mono )
open import L.Axioms.Numerals {ℓ} using ( numeralL; numeralL-fst )
open import L.Ordinal {ℓ} using ( numeral-ord )

周囲の数項は累積階層そのものの中に住んでいます。∅ はその空集合、# k は要素を k 個持つ有限のフォン・ノイマン順序数、sucV は a ↦ a ∪ {a} という後者の操作です。# (suc k) は定義上 sucV (# k) に等しいので、λ が sucV について閉じていれば零以降のすべての数項が自動的に覆われます。ここでの真理値は hProp に直接まとめられたレベル ℓ-suc ℓ の命題であり、各所属の主張は命題です。

open import L.Ordinal.Stages {ℓ} lem using ( ord∈Lset-suc )

open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( ∅; module InfinitySet )
open InfinitySet using ( #_; sucV )

議論に現れる三つの所属は役割が異なります。# k ∈ λ は有限順序数を添字の下に置き、# k ∈ T (sucV (# k)) はそれを自身の後者段階に置き、# k ∈ T λ が求める上界です。いずれも命題として述べられるため、帰納と後の輸送は証明の選び方に依存しませんが、それらを結ぶ推論には後者閉包、順序数段階の性質、単調性の各仮定が必要です。

open hPropStructure 𝒮ᵥ

単調な段階族に対する上界

λ が零を含み後者演算について閉じているとします。帰納法で各数項 # k を λ に入れます。同じ数項を T λ に入れるには、numeral-ord k と後者段階の仮定から # k ∈ T (sucV (# k)) を得ます。後者閉包が添字の関係 sucV (# k) ∈ λ を与え、単調性から # k ∈ T λ が従います。

本節は、所属 ⟨_∈ˢ_⟩ を備えた固定された台 S、その上の任意の写像 T、および T に関する二つの仮定に対して述べられます。第一の T-mono は、段階添字の所属 β ∈ α と x ∈ T β とから x ∈ T α を導きます。第二の T-ord が錨です。順序数 δ は、その自身の後者を添字とする段階 T (sucV δ) に属します。

module BoundOver
  (T : S → S)
  (T-mono : {α β : S} → ⟨ β ∈ˢ α ⟩ → {x : S} → ⟨ x ∈ˢ T β ⟩ → ⟨ x ∈ˢ T α ⟩)
  (T-ord : (δ : S) → IsOrd δ → ⟨ δ ∈ˢ T (sucV δ) ⟩)
  (lam : S) (ordλ : IsOrd lam)

残りのパラメータは添字 λ を記述します。λ は集合であり、順序数であることの証明を持ち、∅ を含み、sucV について閉じています。証明 ordλ は λ 自身が正当な順序数段階の添字であることを記録します。帰納法が消費するのは二つの閉包の事実だけです。

  (succλ : (d : S) → ⟨ d ∈ˢ lam ⟩ → ⟨ sucV d ∈ˢ lam ⟩)
  (∅∈λ : ⟨ ∅ ∈ˢ lam ⟩) where

周囲の数項はすべて λ に入ります。その証明は直前に仮定した二つの閉包の事実だけを用います。これが議論の純粋に帰納的な半分です。排中律も、T の性質も、さらには λ の順序数であることの証明さえも入りません。

k についての帰納法です。基底の場合は、# 0 が ∅ そのものなので仮定 ∅∈λ がそのまま答えます。帰納の段では、# (suc k) は定義上 sucV (# k) に等しいので、帰納仮説 # k ∈ λ に succλ を適用して # (suc k) ∈ λ が得られます。小さい場合は形を示します。0 = ∅ ∈ λ、次に {∅} = sucV ∅ ∈ λ、さらに数項 2 = sucV (sucV ∅) ∈ λ と、各段階で後者についての閉包を一度ずつ使います。

  #∈λ : (k : ℕ) → ⟨ (# k) ∈ˢ lam ⟩
  #∈λ zero    = ∅∈λ
  #∈λ (suc k) = succλ (# k) (#∈λ k)

λ への所属は添字のレベルでの主張ですが、段階 T λ への所属は別の主張であり、λ の閉包だけでなく T の二つの性質を必要とします。道は数項自身の後者の段階を経由します。

二つの段階が合成されます。まず δ = # k に対して T-ord を用い、数項が順序数であることを numeral-ord k が証明していれば、# k は T (sucV (# k)) に入ります。次に T-mono が所属を添字 sucV (# k) から添字 λ へ引き上げます。必要な前提 # (suc k) ∈ λ はまさに #∈λ (suc k) であり、それは sucV (# k) ∈ λ に展開され、T-mono が要求する添字間の所属に一致します。こうして要素 # k は T λ に収まり、最初の段階では順序数であることの証明が実質的な仕事を果たします。

  #∈Tλ : (k : ℕ) → ⟨ (# k) ∈ˢ T lam ⟩
  #∈Tλ k = T-mono {α = lam} {β = sucV (# k)} (#∈λ (suc k))
    {x = # k} (T-ord (# k) (numeral-ord k))

構成可能階層における数項

構成可能な段階は単調であり、各順序数はその後者を添字とする段階に属します。したがって一般の上界の議論を L に適用できます。この所属関係を、モデルの要素として与えた数項についても述べます。

抽象の実体化は、証人を指名するだけで済みます。段階族 T には Lset を与え、Lset-mono が順序数添字の所属に沿う単調性を供給し、ord∈Lset-suc が「各順序数は Lset (sucV α) に属する」という錨を供給します。定理 ord∈Lset-suc がこの特殊化に必要な古典的仮定を担います。数項についての帰納そのものは、先に示した初等的な閉包の議論のままです。λ に関する仮定はそのまま渡されるので、BoundOver の内部で T λ について証明されたことはすべて Lset lam についても使えます。

module Bound (lam : S) (ordλ : IsOrd lam)
             (succλ : (d : S) → ⟨ d ∈ˢ lam ⟩ → ⟨ sucV d ∈ˢ lam ⟩)
             (∅∈λ : ⟨ ∅ ∈ˢ lam ⟩) where

  open BoundOver Lset Lset-mono ord∈Lset-suc lam ordλ succλ ∅∈λ public

モデルの内部では、数項は周囲の順序数そのものではなく、その順序数を指し示す第一成分を持つ対 numeralL k です。この上界は、帰納法を繰り返すのではなく、一度の輸送でこの提示へ移ります。

等式 numeralL-fst k はホスト理論における経路 fst (numeralL k) ≡ # k です。この経路に沿って所属の型族を輸送すると、# k に関する証明が fst (numeralL k) に関する証明へ移ります。sym は、既に得た # k の所属から、求める fst (numeralL k) の所属へ向かうようにパスを整えます。これにより #∈Tλ k が模型の数項についての主張に変わります。

  num∈λ : (k : ℕ) → ⟨ fst (numeralL k) ∈ˢ Lset lam ⟩
  num∈λ k = subst (λ w → ⟨ w ∈ˢ Lset lam ⟩) (sym (numeralL-fst k)) (#∈Tλ k)