数項列

本章ではモデル自身の空集合、対、和集合の演算から L 内部の自然数列を構成し、それが周囲のフォン・ノイマン数項へ射影されることを証明する。

数学的な問いはこうです。集合 a のフォン・ノイマン後者は a ∪ {a} ですが、L のモデルは自前の空集合、非順序対、和集合を標準的な実現者として供給します。それぞれ、所属の仕様を満たす集合の可縮な型の中心であり、確定記述の演算子 ℩ によって読み出されます。そのような中心は仕様をもつ演算であって計算規則ではありません。その定義自身は、基底の集合が周囲の階層が自前の対と和集合から作る集合と同じであるとは言っていません。したがって、この列を階層の数項列と比較する前に、射影方程式の族が必要です。各方程式は、モデルの演算が基底の集合を通して読めば階層の対応する演算である、と述べます。

各射影方程式の議論には固定した形があります。可縮な型の中心を、明示的に作った実現者と比較します。対の場合、その実現者は、二つの基底の集合の単に存在する共通段階 (isL-directed が供給する) に有界な対の構成を適用したものです。可縮性は中心からその実現者へのパスを与え、基底集合への射影関数をそのパスに適用すると、集合の間の等式が得られます。切り詰められたデータの消去が正当なのは、目標が階層の集合の間の等式、すなわち命題だからであり、これは階層の台が h-集合であることに依ります。射影方程式が手に入れば、内部の列と階層の列は一歩ずつ一致し、モデルの record が数項列に要求する二つの指定方程式も、階層自身の事実をそれらに沿って輸送して従います。

章全体が構成的です。排中律もサイズ変更も、実現者の型の可縮性を超える選択も用いません。本章が行わないのは、数項を一つの集合へ収集することです。その収集こそ無限公理自身の内容です。

鍵となる概念は一意な実現です。対の仕様は λ x → (x ≈ˢ a) ⊔ (x ≈ˢ b) であり、hasPairL a b は、それを実現する構成可能集合の型 SetOf が可縮であることを証明します。すなわち、標準的な実現者である中心と、中心から他のすべての実現者へのパスがあるのです。和集合も同様に hasUnionL によって仕様が与えられ証明されます。可縮性の証明は明示的なデータであって、単なる存在主張ではありません。中心と収縮の両方を含み、以下で選ばれるのはこの中心です。これが本章で用いる唯一の形の選択であり、それは可縮性そのものによって供給されます。

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

open import Base.Prelude
module L.Axioms.Numerals {ℓ : Level} where

open import FOL.ZFStructure using ( module hPropStructure )

射影方程式は両側を出会わせます。モデルの側には、hasPairL と hasUnionL とその実現の構成 PairOf と UnionOf、そして内部の空集合 ∅ʟ があります。周囲の側には、階層の非順序対 ⁅ _, _ ⁆ と和集合 ⋃_、後者 sucV、数項 #_ があります。両側を結ぶ入力は isL-directed です。これは、二つの構成可能集合の基底の集合を含む共通の順序数段階を、単に存在するものとして供給します。有界な対の構成が実現者を作るには、まさにそのような段階が必要です。二つの内部の演算は、まず定義されて初めて比較できます。

import FOL.ZFModel
open import V.Model {ℓ} using ( pair-singleton; module NumPin )
open import L.Constructible {ℓ} using ( 𝒮ʟ )
open import L.Axioms.Basic {ℓ}
  using ( hasPairL; hasUnionL; module PairOf; module UnionOf; isL-directed; ∅ʟ )

射影方程式は、周囲の階層の集合の間の等式です。たとえば fst (pairʟ a b) ≡ ⁅ fst a , fst b ⁆。この特定の等式の型が命題なのは、階層の台が h-集合だからであり、setIsSet が保証するのはまさにそれです。この命題性ゆえに、切り詰められた段階のデータをそこへ消去できます。任意の等式の型について命題性を主張しているのではありません。

import Cubical.Data.Empty as Empty
import Cubical.HITs.PropositionalTruncation as PT
open import Cubical.HITs.CumulativeHierarchy.Base using ( setIsSet )
open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( ⁅_,_⁆; ⋃_; module InfinitySet )

コードを読みやすくする約束が二つあります。構造 𝒮ʟ は集合論のモデルとして提示された構成可能宇宙であり、そのモデルのパッケージを開くと、SetOf、すなわち台の要素とその実現の仕様の対の型、そして ℩、すなわち可縮な SetOf の型の中心の第一成分を返す演算子が使えます。全体を通して、台 S の要素への fst は周囲の階層の基底の集合を取り出します。射影方程式が比較するのはまさにこの基底の集合です。

open InfinitySet using ( sucV; #_ )

open hPropStructure 𝒮ʟ

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

モデル自身の演算

確定記述の演算子は、実現者の型の可縮性を演算に変えます。pairʟ と unionʟ は hasPairL と hasUnionL の中心を選び、後者はそれらを合成します。

以下を支配する区別が一つあります。可縮な型から選んだ中心は、仕様をもつ演算であって計算規則ではありません。可縮性の証明は、pairʟ a b の基底の集合を階層の対 ⁅ fst a , fst b ⁆ へ簡約するものではありません。実際に与えるのは、中心からすべての実現者へのパスであり、次節の射影方程式は、そのパスに沿って中心を明示的に作った実現者と比較することで得られます。三つの演算はすべて opaque と宣言され、以後の使用はその構成ではなく、仕様と射影方程式を通して読まれます。

演算子 ℩ は可縮性の証明を受け取り、その中心の第一成分、すなわち台 S の要素を返します。これを hasPairL a b と hasUnionL a に適用すれば、構成可能集合の上の二つの関数が得られます。入力は台の要素、つまり構成可能性の証明書とともにまとめられた集合なので、各演算は入力がすでに持つもののほかに引数を必要としません。

opaque
  pairʟ : S → S → S
  pairʟ a b = ℩ (hasPairL a b)

  unionʟ : S → S
  unionʟ a = ℩ (hasUnionL a)

内部の後者は両者を合成します。sucʟ a = unionʟ (pairʟ a (pairʟ a a))。内側の対は a とそれ自身の非順序対です。後で基底の集合に適用される一元集合の法則がこの内側の対を {a} と同一視し、外側の対の二つの項は a とその一元集合になります。したがって、式が a ∪ {a} へ崩れるのはそのためです。ここで扱うのは外側の非順序対とその二つの項であって、順序対やその成分ではありません。

  sucʟ : S → S
  sucʟ a = unionʟ (pairʟ a (pairʟ a a))

射影方程式

可縮性により取り出した演算を周囲の階層の非順序対および和集合と同一視し、内部の後者について射影方程式を得る。

可縮な型の中心は、一見すると階層が作るであろう集合ではありません。ここで演算は opaque なので、本章では定義を展開せず、射影方程式を通して階層の演算と比較するからです。しかし可縮性が語るのは存在にとどまらず、すべての実現者がまさに中心である、ということです。そこで証明は、手元にある段階のデータから明示的な実現者を作り、それに収縮を適用して中心からその実現者へのパスを得ます。各収縮は、目標が階層の集合の間の等式であるような切り詰められたデータの消去の内部で適用されます。その目標が命題なのは階層の台が h-集合だからであり、これが消去を正当化します。

主張はまず目標を固定します。取り出した対の基底の集合が、階層が基底の集合たちに作る非順序対と等しいこと。消去 PT.rec が isL-directed の単に存在する共通段階のデータを開きますが、これが正当なのは、目標は等式 fst (pairʟ a b) ≡ ⁅ fst a , fst b ⁆ であり、setIsSet (fst (pairʟ a b)) ⁅ fst a , fst b ⁆ がこの等式の型を命題だと証明することだからです。内部では、届くデータ σ , oσ , fa∈ , fb∈ がちょうど PairOf.mkPair が消費するものであり、mkPair はそこから実現者を構成します。証明書が供給するパスは中心からその実現者へ向かうものであり、逆向きではありません。

  pairʟ-fst : (a b : S) → fst (pairʟ a b) ≡ ⁅ fst a , fst b ⁆
  pairʟ-fst a b = PT.rec (setIsSet (fst (pairʟ a b)) ⁅ fst a , fst b ⁆)
    (λ { (σ , (oσ , (fa∈ , fb∈))) →
         cong (λ (e : SetOf (PairOf.Q a b)) → fst (fst e))
           (hasPairL a b .snd (PairOf.mkPair a b σ oσ fa∈ fb∈)) })

最後の一歩は、中心と明示的に構成した実現者を同一視します。収縮 hasPairL a b .snd は任意の実現者に対して、中心からその実現者へ向かうパスを与えます。これを mkPair a b σ oσ fa∈ fb∈ に適用すると、型 SetOf (PairOf.Q a b) の中のパスが得られます。この型は台の要素をその実現の仕様とともにまとめたものです。射影関数 λ e → fst (fst e) をこのパスに適用することで、台の要素を読み取りつぎにその基底の集合を読み取りる射影が、このパスを基底の集合の間の等式に変え、目標が閉じます。切り詰められた共通段階のデータが消去される先はこの集合の等式だけであり、その命題性は setIsSet が供給します。和集合の場合は、入力が一つ少ないだけの同じ議論です。UnionOf.mkUnion は fst a を含む一つの段階を必要とするだけで、証明書 a .snd はまさにそのような、単に存在する段階のデータなので、消去はそれを直接消費します。

    (isL-directed (fst a) (fst b) (a .snd) (b .snd))

  unionʟ-fst : (a : S) → fst (unionʟ a) ≡ ⋃ (fst a)
  unionʟ-fst a = PT.rec (setIsSet (fst (unionʟ a)) (⋃ (fst a)))
    (λ { (σ , (oσ , fa∈)) →
         cong (λ (e : SetOf (UnionOf.Q a)) → fst (fst e))

結果を読めば fst (unionʟ a) ≡ ⋃ (fst a)、モデルの和集合の演算の基底の集合は、階層が基底の集合に作る和集合です。対の方程式と合わせて、モデルの対と和集合から組み立てた集合は、基底の集合を通して読めば、階層の演算から組み立てた同じ集合になります。射影方程式の用途はまさにここにあります。二つの後者の演算を、ひいては二つの数項列を、一歩ずつ比較することです。

           (hasUnionL a .snd (UnionOf.mkUnion a σ oσ fa∈)) })
    (a .snd)

後者の方程式は、射影方程式を合成したものであり、そこに階層自身の {a, a} と {a} の同一視が加わります。外側の和集合を展開し、つぎに外側の対、つぎに内側の対を展開し、最後に重複した一元集合を潰せば、残るのは階層の後者です。

各段階では一つの関数を既存の等式に適用し、入れ子の位置を一つずつ書き換えるだけなので、合成は外から内へ進みます。各因子の向きが重要です。対の方程式は取り出した中心から階層の対へ向かうので、周囲の「対の和集合」という関数をその等式に適用することが項全体を階層の形へ運び、pair-singleton は最後に、宣言どおりの向きで使われます。

最初の三つの因子は外側から順に書き換えます。pairʟ a (pairʟ a a) における和集合の射影方程式は fst (unionʟ ...) ≡ ⋃ (fst (pairʟ a (pairʟ a a))) を与えます。外側の方程式 pairʟ-fst a (pairʟ a a) に関数 ⋃_ を適用すると、引数は ⋃ ⁅ fst a , fst (pairʟ a a) ⁆ へ書き換わります。つぎに内側の方程式 pairʟ-fst a a に関数 λ w → ⋃ ⁅ fst a , w ⁆ を適用すると、⋃ ⁅ fst a , ⁅ fst a , fst a ⁆ ⁆ が得られます。内側の重複した対は pair-singleton によって一元集合と等しく、最後の因子は同じ周囲の関数の中でこの等式を用います。

  sucʟ-fst : (a : S) → fst (sucʟ a) ≡ sucV (fst a)
  sucʟ-fst a =
      unionʟ-fst (pairʟ a (pairʟ a a))
    ∙ cong ⋃_ (pairʟ-fst a (pairʟ a a))
    ∙ cong (λ w → ⋃ ⁅ fst a , w ⁆) (pairʟ-fst a a)

最後の因子は、階層自身の法則が入る場所です。pair-singleton (fst a) は、重複した対 ⁅ fst a , fst a ⁆ を一元集合 ⁅ fst a ⁆ と同一視するパスです。同じ関数をこのパスに適用すれば、項は ⋃ ⁅ fst a , ⁅ fst a ⁆ ⁆ となり、これはまさに sucV (fst a) です。したがってこの因子の連なりは主張を検証します。内部の後者は、基底の集合を通して読めば階層の後者なのです。

    ∙ cong (λ w → ⋃ ⁅ fst a , w ⁆) (pair-singleton (fst a))

数項列の構成

原始再帰により内部の零と後者から numeralL を定義し、帰納法で周囲の数項との等しさ numeralL-fst を証明します。

後者の方程式が手に入れば、列は自然数上の通常の再帰で書け、一度の帰納法で階層の数項へ射影されることが示されます。第 0 の段階は内部の空集合であり、その基底の集合は文字どおり空集合です。

この節が供給するのは、各数項を台の要素として、その所属の振る舞いとともに得ることです。すべての数項を一つの集合に収集するのではなく、無限公理を証明するのでもありません。列は後者の方程式の繰り返しにすぎないので、帰納法で内容のあるのは一歩だけで、零の場合は計算です。

定義は二つの節からなります。第 0 の段階は ∅ʟ、すなわち内部の空集合であり、その後の各段階は内部の後者を直前のものに適用したものです。再帰が自然数の添字の上で行われるので、列は明示的な関数 ℕ → S です。∅ʟ、pairʟ、unionʟ はいずれもそのような要素を返し、内部の後者は繰り返しのたびにこれを保つので、各段階は台の要素になっています。したがって各段階は構成可能性の証明書とともにまとめて手に入ります。

  numeralL : ℕ → S
  numeralL zero    = ∅ʟ
  numeralL (suc n) = sucʟ (numeralL n)

  numeralL-fst : (n : ℕ) → fst (numeralL n) ≡ # n
  numeralL-fst zero    = refl

周囲の数項との整列は n 上の帰納法で証明します。零では両辺とも空集合に計算されるので、パスは refl です。後続では、sucʟ-fst を numeralL n に適用して fst (numeralL (suc n)) を sucV (fst (numeralL n)) と同一視し、帰納法の仮定 fst (numeralL n) ≡ # n の上の関数 sucV を帰納の一歩を後者の内部へ運びます。合成は # (suc n) を定義する再帰と同じ形をしているので、二つの列はすべての段階で一致します。

  numeralL-fst (suc n) = sucʟ-fst (numeralL n) ∙ cong sucV (numeralL-fst n)

二つの指定方程式

numeralL-zero は内部の零に要素がないことを示し、numeralL-suc は次の数項の要素が直前の数項の要素とその数項自身からなることを特徴づけます。

モデルの record は数項列にこの二つの法則を要求します。零が空であること、そして各後者の要素が前者の要素に前者自身を加えたものにちょうど等しいこと。どちらも派生した演算ではなく所属を通して述べられています。この言い回しゆえに証明は短くなります。どちらも階層の数項についての事実であり、射影の族 numeralL-fst に沿って輸送されるからです。ここで確定記述の演算子が展開されることは一切ありません。

運び役はモジュール NumPin です。これは周囲の階層に値をとる列 a : ℕ → V ℓ と整列 q : (n : ℕ) → a n ≡ # n を受け取り、その列に対する二つの指定方程式を返します。こちらの列は基底の集合の族 λ k → fst (numeralL k) と整列 numeralL-fst を供給します。

第 0 の方程式は反駁の形をしています。列の第 0 段階の要素 z から空のホスト型の要素が得られるので、得られる関数型は hProp の設定ではそれ自身が命題です。pinZero は仮定された所属を段階 0 での整列に沿って輸送し、fst (numeralL zero) への所属を # zero への所属に変え、その後、階層自身の「∅ には要素がない」という事実が証明を閉じます。輸送は一方向にだけ進みます。列からライブラリの数項へ、です。

numeralL-zero : (z : S) → ⟨ z ∈ˢ numeralL zero ⟩ → Empty.⊥
numeralL-zero z = NumPin.pinZero (λ k → fst (numeralL k)) numeralL-fst (fst z)

numeralL-suc : (n : ℕ) (z : S)
             → (⟨ z ∈ˢ numeralL (suc n) ⟩
                  → ⟨ (z ∈ˢ numeralL n) ⊔ (z ≈ˢ numeralL n) ⟩)

後者の方程式は一対の含意であり、その第二の成分が語るのは構造の関係 ≈ˢ です。この制限構造では、その基底はパス fst z ≡ fst (numeralL n) です。順方向では、numeralL (suc n) の要素が段階 suc n での整列に沿って # (suc n) への所属へ輸送され、そこで階層自身の sucV の所属の分析が、単に存在するものとして、それを # n の要素である場合と # n そのものである場合に分けます。各枝はさらに段階 n での逆向きの整列に沿って列へ輸送し戻されます。逆方向では、numeralL n の要素は # n へ輸送されたうえで ∈sucV-inl によって # (suc n) へ置かれ、numeralL n と等しい要素はパスを # n へ運び、階層自身の「集合は自分自身の後続に属する」という事実を使います。どちらの向きも、列 λ k → fst (numeralL k) と整列 numeralL-fst に対する pinSuc の出力を fst z に実例化したものです。

             × (⟨ (z ∈ˢ numeralL n) ⊔ (z ≈ˢ numeralL n) ⟩
                  → ⟨ z ∈ˢ numeralL (suc n) ⟩)
numeralL-suc n z = NumPin.pinSuc (λ k → fst (numeralL k)) numeralL-fst n (fst z)

まとめ

numeralL は L の内部におけるフォン・ノイマン数項のコピーであり、モデルの record が要求する零と後者の正確な所属法則を満たします。

本章の議論には三つの層があります。内部の後者は、一意存在が可縮中心として手渡す演算から組み立てられ、射影方程式がそれらの演算の基底の集合を、命題の水準で、階層の非順序対・和集合・後者と同一視します。つぎに自然数上の再帰が内部の空集合から内部の後者を繰り返し、帰納法により numeralL-fst、すなわち各段階の基底の集合を周囲の数項 # n と整列させるパスの族が証明されます。最後に、この整列へ NumPin を適用して numeralL-zero と numeralL-suc が従い、二つの所属法則が内部の列に対して成り立ちます。場合分けの分析はすべて階層の数項の上で行われます。

ここで確立されるのは個々の数項についての事実です。各 numeralL n が L の内部に存在し、正しい所属の振る舞いをもつこと。本章には段階たちを一つの集合へ収集する主張はなく、無限は証明されません。射影方程式の用途は数項にとどまらず、モデルの対と和集合から組み立てられたものは、基底の集合を通して読めば、階層の演算から組み立てた同じものです。