定義可能な単射を内部コードにする

宇宙レベル ℓ と、この排中律のインスタンスを固定する。ここでの数学的な問題は、ホスト側の値を定める規則から、L が量化できる集合を得ることである。その規則自体が L に入るのではない。論理式が L のある集合上でその値を記述し、置換が構成可能な関数グラフを作り、単射性の証明がそのグラフに内部の基数比較で用いる符号を与える。

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

L の外側で値を定める規則を記述しても、それだけでは L が量化できる対象にはならない。モデルの内部で基数を比較するには、その値を順序対として記録する構成可能集合が必要である。そこで本章では、定義可能性と各点での一意性から、置換によってそのグラフを集める方法を考える。

唯一の古典的パラメータは、水準 ℓ-suc ℓ における排中律である。本章の初等的な段階、たとえば一意性の証明、所属の輸送、命題的切り詰めを命題へ消去する操作は構成的である。このパラメータが必要になるのは、一般の置換定理によって関数グラフを L の要素として集めるときである。選択公理はどの形でも用いない。

ここでは三種類の対象を区別する必要がある。論理式は、構成可能な台の要素を定数とする一階言語に属する。充足関係は、その論理式を L 上の構造で解釈する。そして pr は、基礎集合の順序対を周囲の階層で表すクラトフスキー符号である。後で定義の論理式を読むときは値が先、入力が後であるが、集められた関数グラフの項目は pr(入力,値) となる。

証明は三つの数学的な形を順に通る。再帰は、定義域、値を定める論理式、そして定義域の各点で充足する値のファイバーが可縮であることの証明からなる。そのグラフ構成は置換によって順序対を集め、一価性と正確な定義域を証明する。最後に injAt が、残る単射性の条件、すなわち同じ出力をもつ二つの項目の入力が等しいことを表す。

集合 a と b に対して、InjCode F a b はちょうど四つの成分をもつ。グラフ F が一価であること、その定義域が正確に a であること、単射的であること、そしてそこに現れるすべての値が b に属することである。四条件にはいずれも対応する対象言語の論理式があり、値域条件には先に構成した valuesInAt を用いる。InjL a b は、そのような F と符号の存在を命題的切り詰めに入れる。

open import Cubical.HITs.CumulativeHierarchy.Base using ( _∈_ )
open hPropView 𝒮ʟ using ( S )
open hPropView 𝒮ᵥ using ( _∈ˢ_ )
module AbsL = FOL.Absoluteness.Single 𝒮ᵥ isL isL-trans using ( _⊨ᵐ_ )
open AbsL using () renaming ( _⊨ᵐ_ to _⊨_ )

単射符号を一つの論理式として読む

InjCode の四条件は、グラフ、定義域、終域という三つの指定位置をもつ一つの対象論理式で表せる。最初の三つの連言は、一価性、正確な定義域、単射性の論理式を再利用する。最後の連言は入力と出力を量化し、グラフが両者を関係づけるなら出力が終域の位置に属すと述べる。したがってホスト層の値域フィールドを不可視と仮定するのではなく、このインターフェースで検査済みの論理式に結び付ける。

injCodeAt : ∀ {n} → Fin n → Fin n → Fin n → Formula S n
injCodeAt f A B = svAt f ∧̇ domAt f A ∧̇ injAt f
                  ∧̇ valuesInAt f B

module InjCodeAt {n : ℕ} (f A B : Fin n) (γ : Vec S n) where

private
  F D C : S
  F = lookup f γ
  D = lookup A γ
  C = lookup B γ

read : ⟨ γ ⊨ injCodeAt f A B ⟩ → InjCode F D C
read (sv , dm , ij , ran) =
    svAt-in zero (F ∷ D ∷ []) (λ x y y' p q → svAt-out f γ sv x y y' p q)
  , domAt-intro zero (suc zero) (F ∷ D ∷ []) (λ x →
        (λ h → rec₁ ((x .fst ∈ D .fst) .snd)
                 (λ { (y , p) → domAt-out f A γ dm x y p }) h)
      , (λ hx → domAt-in f A γ dm x hx))
  , injAt-in zero (F ∷ D ∷ []) (λ y x x' p q → injAt-out f γ ij y x x' p q)
  , valuesInAt-out f B γ ran

fill : InjCode F D C → ⟨ γ ⊨ injCodeAt f A B ⟩
fill (sv , dm , ij , ran) =
    svAt-in f γ (λ x y y' p q → svAt-out zero (F ∷ D ∷ []) sv x y y' p q)
  , domAt-intro f A γ (λ x →
        (λ h → rec₁ ((x .fst ∈ D .fst) .snd)
                 (λ { (y , p) → domAt-out zero (suc zero) (F ∷ D ∷ []) dm x y p }) h)
      , (λ hx → domAt-in zero (suc zero) (F ∷ D ∷ []) dm x hx))
  , injAt-in f γ (λ y x x' p q → injAt-out zero (F ∷ D ∷ []) ij y x x' p q)
  , valuesInAt-in f B γ ran

グラフの位置を存在量化すると InjL の論理式が得られ、残る二つの位置が定義域と終域を名指す。その意味論的な存在は初めから命題的に切り詰められており、InjL とちょうど一致する。先の read と fill をその切り詰めの内側で写せば、グラフを選ばずに両方向が得られる。

injLAt : ∀ {n} → Fin n → Fin n → Formula S n
injLAt A B = ∃̇ (injCodeAt zero (suc A) (suc B))

module InjLAt {n : ℕ} (A B : Fin n) (γ : Vec S n) where

private
  D C : S
  D = lookup A γ
  C = lookup B γ

read : ⟨ γ ⊨ injLAt A B ⟩ → InjL D C
read = map₁ (λ { (F , code) → F , InjCodeAt.read zero (suc A) (suc B) (F ∷ γ) code })

fill : InjL D C → ⟨ γ ⊨ injLAt A B ⟩
fill = map₁ (λ { (F , code) → F , InjCodeAt.fill zero (suc A) (suc B) (F ∷ γ) code })

内部の基数性とは、候補のどの要素にも候補からの単射が存在しないという主張である。次の論理式はそれをそのまま述べる。より小さいかもしれない要素を束縛した後、その候補への所属から injLAt 論理式の否定を導く。読み取りで変換する必要があるのは単射の論理式だけであり、外側の全称量化、含意、否定は IsCardinalL がすでに使う関数型へ計算される。

cardinalAt : ∀ {n} → Fin n → Formula S n
cardinalAt K = ∀̇ ((var zero ∈̇ var (suc K))
                  ⇒̇ ¬̇ injLAt (suc K) zero)

module CardinalAt {n : ℕ} (K : Fin n) (γ : Vec S n) where

private
  κ : S
  κ = lookup K γ

read : ⟨ γ ⊨ cardinalAt K ⟩ → IsCardinalL κ
read h δ δ∈κ inj = lower
  (h δ δ∈κ (InjLAt.fill (suc K) zero (δ ∷ γ) inj))

fill : IsCardinalL κ → ⟨ γ ⊨ cardinalAt K ⟩
fill c δ δ∈κ sat = lift
  (c δ δ∈κ (InjLAt.read (suc K) zero (δ ∷ γ) sat))

二つの型理論上の事実がこの証明を支える。依存対の第二成分が命題値なら、Σ≡Prop は第一成分の間のパスを対全体の間のパスへ持ち上げる。命題的切り詰めは、要素が存在するという事実だけを残す。グラフを読み戻す補題 pair-out は、行き先のファイバーが命題なので、命題的切り詰めに入った由来の証人をそこへ消去できる。最後の段階では ∣_∣₁ を用いて、具体的なグラフと符号を隠する。どちらの操作も、証人の族を大域的に選ばない。

台 S は L 上の構造から来る。要素 x : S は、周囲の集合 x .fst と、それが構成可能であることを示す命題値の証明からなる。所属の記法は周囲の階層から取るため、レコード内の式は x .fst ∈ˢ dom .fst のように基礎集合を明示的に比較する。構成が L の要素を返す必要があるときには、構成可能性の証明が第二成分として残っている。

記法 _⊨_ は、周囲の階層を構成可能集合に制限して得られる構造での充足関係を表す。したがって (y ∷ x ∷ []) ⊨ graph は、L の要素を graph の二つの自由な位置に入れて解釈する。AbsL という名前は、任意の論理式が L と周囲の階層との間で絶対的だと主張するものではない。本章で使うのは制限された構造の意味論と、すでに証明された置換定理である。

関数が定義可能であるとは何か

DefinableMap はまず L の二つの要素 dom と cod を指定し、それらが順序数や基数であるとは仮定しない。ホスト側の値を定める規則 fn は、x : S と x が dom に属する証拠 m の組に対してだけ定義される。定義域の外で値を与える必要はない。この型では fn x m が m に言及してもかまわない。所属は命題なので、そのような二つの証明は等しく、合同性によって対応する値も等しくなる。フィールド into は、選ばれた各値が cod に属することを証明する。

record DefinableMap : Type (ℓ-suc (ℓ-suc ℓ)) where
  field
    dom cod : S
    fn      : (x : S) → ⟨ x .fst ∈ˢ dom .fst ⟩ → S
    into    : (x : S) (m : ⟨ x .fst ∈ˢ dom .fst ⟩) → ⟨ (fn x m) .fst ∈ˢ cod .fst ⟩

残るフィールドは、ホスト側の値を対象言語の論理式に結びつける。graph は二つの自由な位置をもち、S の要素を定数として含むことができ、Δ₀ 論理式である必要はない。各 x ∈ dom に対して、defines は選ばれた値を先、x を後に置いた環境で論理式が成り立つことを証明し、only は論理式を満たす任意の y がその選ばれた値と S の中で等しいことを証明する。これらの条件は dom の外の入力を制約せず、only は候補 y が cod に属するとも仮定しない。選ばれた値が終域に入ることは、別のフィールド into が与える。

    graph   : Formula S 
    defines : (x : S) (m : ⟨ x .fst ∈ˢ dom .fst ⟩)
            → ⟨ (fn x m ∷ x ∷ []) ⊨ graph ⟩
    only    : (x : S) (m : ⟨ x .fst ∈ˢ dom .fst ⟩) (y : S)
            → ⟨ (y ∷ x ∷ []) ⊨ graph ⟩ → y ≡ fn x m

グラフの項目を順序対として符号化する

関数グラフは集合として表すため、各入出力項目をまず順序対として表す。定義論理式は第一の意味論的な位置で値を、第二の位置で入力を読むが、集合による符号化は対応する項目を pr(入力,値) として格納する。グラフを構成し、後でその内容を読み戻すには、この二つの順序を区別し続ける必要がある。

L の内部でグラフを構成する

最初の構成が仮定するのは、定義可能性と関数性だけである。M から L の要素である完全な関数グラフを作り、その順序対の項目を正確に入れ、読み取る方法を得る。単射性は次の段階まで保留する。同じグラフ構成は、最小証人の表のように、目的上単射である必要のない定義可能な写像にも適用できるからである。

module Graph (M : DefinableMap) where

open DefinableMap M public

private
  R : Recursion
  R = record
    { dom = dom ; graph = graph
    ; funct = λ x m → (fn x m , defines x m)

        , λ { (y , h) → Σ≡Prop (λ w → ((w ∷ x ∷ []) ⊨ graph) .snd) (sym (only x m y h)) } }

open RecursionGraph R public
  using ( Mem; isPropMem; F; F-in; F-out; Fib; isPropFib; pair-out; γ; sv; dm )

ran : (x y : S) → ⟨ pr (x .fst) (y .fst) ∈ F .fst ⟩ → ⟨ y .fst ∈ cod .fst ⟩
ran x y h = subst (λ w → ⟨ w ∈ cod .fst ⟩) (sym e) (into x m)
  where
  m = (pair-out x y h) .fst
  e = (pair-out x y h) .snd

外部の単射性から符号化された単射へ

このグラフを単射の符号にするには、実質的に新しい仮定として単射性を加える必要がある。dom への所属の証明を伴う二つの入力について、選ばれた値の基礎集合が等しければ、入力の基礎集合も等しいと仮定する。fn の型は所属の証明に依存しているので、その引数は明示されたままである。証明無関係性は異なる所属の証明の間の整合性を保証するが、仮定自体は二つの入力で実際に与えられた証拠について述べられる。その結論は injAt の等号の条項が要求する強さと正確に一致する。

module Inj (M : DefinableMap)
           (inj : (x : S) (m : ⟨ x .fst ∈ˢ (DefinableMap.dom M) .fst ⟩)
                  (x' : S) (m' : ⟨ x' .fst ∈ˢ (DefinableMap.dom M) .fst ⟩)
                → (DefinableMap.fn M x m) .fst ≡ (DefinableMap.fn M x' m') .fst
                → x .fst ≡ x' .fst) where

open Graph M public

ij : ⟨ γ ⊨ injAt zero ⟩
ij = injAt-in zero γ (λ y x x' p q →
  let (m , e)   = pair-out x y p
      (m' , e') = pair-out x' y q
  in inj x m x' m' (sym e ∙ e'))

code : InjCode F dom cod
code = sv , dm , ij , ran

injL : InjL dom cod
injL = ∣ F , code ∣₁