環境の集合の一致

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

読書案内 · 依存マップ

充足関係の節には、L の内部で、ある基礎集合の上の与えられた長さの環境をちょうどすべて集めた一つの集合が必要です。これまでの章は二つの材料を別々に与えました。要素によってそのような集合を特徴づける論理式 envSetAt と、前章で構成した集合 envSet B m です。ある集合がこの記述を満たすのは、その各要素が集合として、基礎の上の長さ m の環境のグラフであるとき、かつそのときです。本章は、記述と構成済みの集合が一致することを証明します。一致には二つの読み方があります。充足の判断によって記述の集合スロットに置かれた集合は、構成済みの集合とちょうど同じ要素を持ち、また構成済みの集合それ自体が記述を満たすので、自分の基礎と長さを束縛する節は、構成済みのデータでスロットを埋めてから記述を引用できます。

どちらの読み方も、要素から復元された環境という一つの対象の上で行われます。単値性、数項による定義域、基礎への所属、そして数項と基礎の要素からなる対、という四つの内部の節が、ある集合がこのようなグラフであることを述べます。前の章はそこから割り当ての関数を復元し、その集合を関数の正準なグラフと同一視しました。本章の各段階は、この復元をいずれかの方向に走らせることと、名指されたスロットの一致する環境の間で環境の節の充足を運ぶ輸送の補題とに帰着します。

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

本書の常設のオプションは引き続き有効です。本章で唯一用いる非構成的な入力は、下のパラメータ lem として明示されます。

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

基礎語彙は「基礎語彙」の章の配置どおり全体として導入されます。排中律はオプションとしてではなくデータとして現れ、本章はこれをパラメータとして受け取ります。

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

モジュールパラメータはレベル ℓ-suc ℓ の排中律の実例で、二つの構造の充足の主張の住むレベルに一致します。これは、この章が引用する環境の集合を構成した章へそのまま渡されます。

open import FOL.ZFStructure using ( module hPropStructure )
import FOL.Absoluteness
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )
open import L.Constructible {ℓ} using ( 𝒮ʟ; isL; isL-trans )

言語を解釈する構造は二つであり、本章はその間を行き来します。周囲の構造 𝒮ᵥ は階層そのものであり、内側の構造 𝒮ʟ はそれを構成可能な集合のクラス isL に制限したものです。このクラスは推移的であり、isL-trans がそれを記録します。絶対性の機構は、まさにこの組の上で働くために導入されます。

open import L.Coding.Model {ℓ} using ( envOverAt; envOverAt-transport )
open import L.Coding.Expressions {ℓ} using ( envSetAt; extAt-out; extAt-in; extAt-in-both; numL )

二つの論理式とその読み方が本章の仕事を担います。環境の節 envOverAt は、候補のグラフが単値であり、その定義域が指定された定義域スロットの集合とちょうど一致し、値が指定された基礎集合に属し、その二つの集合の要素からなる対だけを含むことを述べ、輸送の補題は、名指されたスロットの一致する環境の間でこの節の充足を運びます。外延的な記述 envSetAt は、二つの全称含意の形で、ある集合の要素がちょうどそれらの環境であることを述べ、三つの読み方がこれらの含意をどちらの向きにもほどきます。

open import L.Coding.EnvironmentSet {ℓ} lem
  using ( envSet; envSet-in; envSet-out; envS; envOver; module Recover )

前の章から来るのは、構成済みの集合 envSet、その二つの所属の補題、正準なグラフの要素 envS、みずからの正準な環境で満たされる環境の節 envOver、そして復元のモジュールです。復元のモジュールは四つの節から環境を読み取り、その集合をその環境のグラフと同一視します。

import Cubical.HITs.PropositionalTruncation as PT
open import Cubical.HITs.CumulativeHierarchy.Base using ( _∈_ )
open import Cubical.HITs.CumulativeHierarchy.Constructions using ( module InfinitySet )
open InfinitySet using ( #_ )

環境の集合への所属からそれを表す環境を復号すると、切り詰められた証人だけが得られます。一方、目標となる充足と所属の主張はいずれも命題です。周囲の数項 # m が長さのスロットを埋めます。

open hPropStructure 𝒮ʟ

内側の構造を開くと、全章で使う充足の記法が固定されます。その台の要素、その所属関係、そして L の中で読まれる充足の判断です。

module AbsL = FOL.Absoluteness.Single 𝒮ᵥ isL isL-trans
open AbsL renaming ( _⊨ᵐ_ to _⊨_ )

絶対性のモジュールは構成可能な集合という推移的クラスの上で実例化され、その内側の充足関係には平易な _⊨_ の名が与えられます。本章が読む論理式はすべて L の上のものであり、それと競う読み方はほかにないからです。

記述から所属関係へ

最初のモジュールは、基礎集合 B、長さ k の環境 γ、その三つのスロット、長さ m、そして二つの等式を固定します。等式は、長さのスロットが m の数項で、基礎のスロットが B で埋められていることを述べます。前提は、γ が集合スロットを Ei に置いた記述を満たすことです。結論は要素の一致です。Ei の指す集合と構成済みの envSet B m は、ちょうど同じ集合を含みます。

どちらの方向も、同じ二つの材料の上を走ります。復元のモジュールは四つの節から環境を読み取り、その出所の集合をその環境の正準なグラフと同一視し、輸送の補題は、名指されたスロットの一致する環境の間を、まさにそれらの名指しの等式に沿って環境の節の充足を運びます。どちらの方向も、記述や構成を証明し直すことはありません。

private
  nn : ℕ → S
  nn j = # j , numL j

長さのスロットは数項で埋められ、その数項自身も L の要素でなければなりません。補助定義 nn がこれを作ります。周囲のフォン・ノイマン数項 # j に、その構成可能性の証明を対にしたものです。

module Ambient (B : S) {k : ℕ} (γ : S ^ k) (Ei di bi : Fin k) (m : ℕ)
  (qd : fst (lookup di γ) ≡ # m) (qb : fst (lookup bi γ) ≡ fst B)
  (hE : ⟨ γ ⊨ envSetAt Ei di bi ⟩) where

モジュールは、この問いの一つの実例のデータを集めます。B は基礎集合、γ は長さ k の環境で、三つのスロットに名前が付きます。Ei が候補の集合を、di が長さの数項を、bi が基礎を収めます。等式 qd と qb は、この二つのスロットが m の数項と B で埋められていることを述べ、hE は、γ が集合スロットを Ei に置いた記述を満たすことを述べます。このデータのもとで、Ei の指す集合と envSet B m が同じ要素をもつことが示されます。

  into : (z : S) → ⟨ fst z ∈ fst (lookup Ei γ) ⟩
       → ⟨ fst z ∈ fst (envSet B m) ⟩

最初の方向は、スロットの集合を内側へ読むものです。Ei の指す集合のどんな要素も、構成済みの envSet B m の要素です。

  into z hz = subst (λ w → ⟨ w ∈ fst (envSet B m) ⟩)
    (sym (Recover.recovers B m (z ∷ γ) zero (suc di) (suc bi) qd qb ov))
    (envSet-in B (Recover.g B m (z ∷ γ) zero (suc di) (suc bi) qd qb ov))

証明は、前の章の復元をこの要素そのものに向けて再利用します。仮定は z が Ei の指す集合に属することを言うので、記述は z で適用できます。復元は z から環境 g を読み取り、その正準なグラフが集合として z 自身であると同定します。構成済みの集合はそのような環境の正準なグラフをすべて含むので、この同定に沿って輸送すれば、要素 z は envSet B m の中に入ります。

    where
    ov : ⟨ (z ∷ γ) ⊨ envOverAt zero (suc di) (suc bi) ⟩
    ov = extAt-out Ei (envOverAt zero (suc di) (suc bi)) γ hE z hz

復元には、四つの節が z で成り立つことが要ります。記述が与えるのはまさにこれです。要素 z に適用すれば、z で拡張した環境の上の環境の節が得られ、長さと基礎のスロットは新しい項目のぶんだけ後ろへずれます。

  outof : (z : S) → ⟨ fst z ∈ fst (envSet B m) ⟩
        → ⟨ fst z ∈ fst (lookup Ei γ) ⟩

第二の方向は外向きに読むものです。構成済みの envSet B m のどんな要素も、Ei の指す集合の要素です。

  outof z hz = PT.rec (snd (fst z ∈ fst (lookup Ei γ)))
    (λ { (g , eg) →

構成済みの集合への所属は、切り詰められた証人を手渡します。それは環境 g であり、その正準なグラフが z です。目標は所属の主張、つまり命題なので、切り詰めは消去でき、証人を生み出すのは前の章の所属の特徴づけです。

      extAt-in Ei (envOverAt zero (suc di) (suc bi)) γ hE z
        (envOverAt-transport (B ∷ nn m ∷ envS B g ∷ []) (z ∷ γ)
          (suc (suc zero)) (suc zero) zero zero (suc di) (suc bi)
          (sym eg) (sym qd) (sym qb)
          (envOver B g)) })

復元された環境は、みずからの正準な環境、すなわち三つのスロットに B と m の数項とそのグラフが収まった環境で、環境の節を満たします。輸送の補題は、三つの等式に沿ってこの充足を拡張された環境 (z ∷ γ) へ運びます。正準なグラフを z と読み、数項を di の項目と読み、B を bi の項目と読むのです。記述はその内向きの含意を通して直ちに適用でき、z が Ei の指す集合に属すると結論されます。

    (envSet-out B m z hz)

輸送に渡される環境は、構成済みの集合の所属の特徴づけから来ます。この方向の出発点であった要素 z に適用されるのです。

構成した集合が記述を満たすこと

第二のモジュールは一致を逆向きに回し、生み出す方向を問います。構成済みの環境の集合それ自体は、この記述を満たすのでしょうか。集合のスロットに置き、他の二つのスロットに m の数項と基礎を置けば、答えは肯定的です。これこそ、自分の基礎と長さを束縛する節が、構成済みのデータでスロットを埋める際に必要とするものです。証明は以前と同じ二つの働きを、今度は記述の要求する順序で行います。構成済みの集合の各要素が要素ごとの節を満たすこと、そしてその節を満たす集合がすべて要素であることが示されます。

モジュールは充足に関する前提を一切仮定しません。三つの等式が、集合のスロットに構成済みの集合そのものが、長さのスロットに m の数項が、基礎のスロットに B が収まっていることを述べます。これだけから、γ での記述の全体が証明されます。

module AmbientHolds (B : S) {k : ℕ} (γ : S ^ k) (Ei di bi : Fin k) (m : ℕ)
  (qE : fst (lookup Ei γ) ≡ fst (envSet B m))
  (qd : fst (lookup di γ) ≡ # m) (qb : fst (lookup bi γ) ≡ fst B)
  where

三つの等式が前提のすべてです。集合のスロットを構成済みの集合で、長さのスロットを数項で、基礎のスロットを基礎で名指すのは、節が三つのスロットを構成済みのデータで埋めるときに行うことそのものであり、したがってモジュールが証明する記述は、そのような節が消費する形そのものです。

  holds : ⟨ γ ⊨ envSetAt Ei di bi ⟩
  holds = extAt-in-both Ei (envOverAt zero (suc di) (suc bi)) γ fwd bwd

記述は外延的なものです。Ei の指す集合がちょうどそれらの環境を含むことを述べ、その二つの全称含意を別々に証明してから結びます。モジュールの冒頭で予告した形が、ここで埋められます。

    where
    fwd : (z : S) → ⟨ fst z ∈ fst (lookup Ei γ) ⟩
        → ⟨ (z ∷ γ) ⊨ envOverAt zero (suc di) (suc bi) ⟩

順方向の含意が生み出す方向です。構成済みの集合の各要素は、拡張された環境の上で要素ごとの節を満たします。

    fwd z hz = PT.rec (snd ((z ∷ γ) ⊨ envOverAt zero (suc di) (suc bi)))
      (λ { (g , eg) → envOverAt-transport (B ∷ nn m ∷ envS B g ∷ []) (z ∷ γ)

所属 hz は、まず等式 qE に沿って構成済みの集合へと指し直され、前の章の所属の補題が切り詰められた環境を手渡します。反対側の目標は充足の判断の一つの節、つまり命題なので、切り詰められた証人を分解できます。

             (suc (suc zero)) (suc zero) zero zero (suc di) (suc bi)
             (sym eg) (sym qd) (sym qb) (envOver B g) })

復元された環境の環境の節は、読み取りの方向とまったく同じやり方で輸送されます。その正準な環境から判断の拡張された環境へ、グラフは要素 z と読み、数項は di の項目と読み、基礎は bi の項目と読まれます。残るのは節そのものであり、順方向の含意が負っているのはこれです。

      (envSet-out B m z (subst (λ w → ⟨ fst z ∈ w ⟩) qE hz))

輸送に渡される環境は、構成済みの集合の所属の特徴付けから来ます。qE が最初の一歩、すなわちその要素を envSet B m の要素として読み直す段階を供給します。

    bwd : (z : S) → ⟨ (z ∷ γ) ⊨ envOverAt zero (suc di) (suc bi) ⟩
        → ⟨ fst z ∈ fst (lookup Ei γ) ⟩

逆方向の含意は読み取りの方向です。拡張された環境の上で要素ごとの節を満たすものは、すべて Ei の指す集合に属します。

    bwd z h = subst (λ w → ⟨ fst z ∈ w ⟩) (sym qE)
      (subst (λ w → ⟨ w ∈ fst (envSet B m) ⟩)
        (sym (Recover.recovers B m (z ∷ γ) zero (suc di) (suc bi) qd qb h))
        (envSet-in B (Recover.g B m (z ∷ γ) zero (suc di) (suc bi) qd qb h)))

z での節は、復元の入力です。復元された環境の正準なグラフは集合として z と一致し、構成済みの集合はそのグラフを含みます。最初の輸送が復元されたグラフを z と読み、所属を envSet B m の中に着地させ、二度目の輸送が qE に沿って逆に走り、envSet B m への所属を Ei の指す集合への所属へ変えます。