Bedrockこの章を読むか、対話型目次と依存グラフで別のルートを選べます。
対話型目次 · 依存グラフモジュールは宇宙レベル ℓ を固定し、本書の常の形式に従って古典的な仮定を明示的に受け取る。ℓ-suc ℓ での排中律が引数として渡され、大域的に仮定されることはなく、本章の各定理はどのレベルの実例を使うかを正確に記録する。
module L.GCH.SkolemHull {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where
本章は、構成可能段階の中の始集合の Skolem 包を作り、包が段階の中で初等的であることを示し、所属を保つ全単射によって推移的集合へ崩壊させ、充足関係と有界論理式が崩壊を越えてどう移るかを整理する。重要なのは、包そのものはコードで与えられた像にすぎず、推移性は Mostowski 崩壊の後に初めて得られる、という点である。
本章は古典論理に依拠し、仮定はここで入る。包の構成は問いの充足可能性を判定し、外延性の証明は両方向で所属を判定し、初等性の移送は二重否定を除去する。これらの段階はどれも排中律を消費する。
open import Cubical.Relation.Nullary using ( decRec )
open import Cubical.HITs.PropositionalTruncation using ( map2 )
open import Cubical.Data.Sum using () renaming ( map to sumMap )
open import Cubical.Data.Vec using ( _++_ )
対象言語は本書の一階の言語である。論理式は項から等号と所属で作られ、命題の結合子、非有界と有界の量化子の下で閉じている。述語 Δ₀ は、すべての量化子が有界である論理式を選び出す。
述語 Δ₀ は論理式の構造に沿う帰納的な証拠である。その構成子は原子式・結合子・有界量化子を覆うが、非有界量化子に対応する構成子はない。この証拠が後の絶対性の議論を支え、countFo と constantsFo は定数の各出現を記録する。
パラメータ抽象は定数の出現を追加の環境変数で置き換え、定数写像と定数改名は意味を保って定数アルファベットを変える。renameTm は文脈写像に沿って変数の位置を改名し、これにより以下で suc による弱化が得られる。周囲の階層は外延性とともに開かれる。同じ要素をもつ集合は等しい、という性質である。
提示は、埋め込みをもつ小さな型で集合の要素を索引づけ、その繊維が提示された要素を名指す。崩壊は任意の台 X から推移的な像を構成し、崩壊写像を X 上で単射にするために制限された所属関係の外延性を用いる。Δ₀ の小ささは、有界に定義できるクラスを集合へ分離する。空集合は各定義可能性後続に属し、Lset-suc は後続添字の段階を直前の段階の定義可能冪集合と同一視する。
構成可能な段階 Lset α は推移的であり、その構成は指数について単調なので、より大きな指数はより大きな段階を与える。包の議論で繰り返し使う順序数の事実は、順序数の要素が順序数であること、ω が順序数であること、数項が ω に属すること、空集合が順序数であることである。
整列順序には最小要素の選択子が伴う。述語を満たす要素の存在の切り詰められた主張から、述語を満たし整列順序で最小の要素を返す。段階の所属のランクによる特徴づけと、段階の台に制限した段階の順序がこの選択子に入力を供給し、和と単元を符号化する仕組みが、後で使う有限の始集合を作る。
本章の環境は台の要素のベクトルであり、その演算は成分ごとに行われる。関数を環境へ写すこと、索引で参照すること、要素を一つ加えて延ばすこと、そして連結である。第二成分が命題である対は、要素を、決して区別しない証拠とともに記録する。
空型は矛盾を表す。⊥*-rec はその要素から任意の目標へ消去し、isProp⊥ は目標が矛盾であるとき命題的切り詰めの消去を可能にする。存在論理式の充足と提示された集合への所属は命題的切り詰めで表され、証人を選ばずに存在だけを保持する。
累積階層は添字型と評価で集合を提示する。包では有限木型 Code を添字型とし、論理式は証人コードの一部であるが、それ自体がコードなのではない。構成は、空集合、和、非順序対と一元集合の構成、そして無限順序数とその後続を供給する。
open import Cubical.HITs.CumulativeHierarchy.Base using ( V; sett )
open import Cubical.HITs.CumulativeHierarchy.Constructions
using ( ∅; _∪_; ⁅_,_⁆; ⁅_⁆s; union-ax; pairing-ax; module InfinitySet
; SetPackage; SingletonPackage ) -- lint-agda: keep (SetPackage via record projection)
open InfinitySet using ( ω; sucV )
小さな所属の関係 _∈ₛ_ と、周囲の所属 _∈ˢ_ への橋 ∈∈ₛ は、集合の提示された読みと、階層の中での読みをつなぐ。提示が内部的に記録することは、宇宙で成り立つことと同じである。
open import Cubical.HITs.CumulativeHierarchy.Properties
using ( _∈ₛ_; ∈∈ₛ; ⟪_⟫; ⟪_⟫↪; extensionality )
周囲の構造を開くことで、修飾のない等号と所属の記号は周囲の関係を表す。一方、制限された各構造は固有の意味論的解釈をもつ。
open hPropView 𝒮ᵥ
SemV は、以下で充足関係を具体化するときに使う固定長の周囲環境を与える。定数が 𝒮ʟ を動く論理式では、出現回数によって定数を含まない場合を識別できる。そのとき erase は、充足を変えずに定数領域を空の型へ置き換える。
module SemV = FOL.Semantics 𝒮ᵥ using ( module At )
module CS = hPropView 𝒮ʟ using ( S )
module Cnt = FOL.Manipulation.ConstantOccurrences.ZeroOccurrences CS.S using ( erase; erase-inv )
空の定数領域では、Δ₀-small は各有界論理式の各環境での真理値が一段低い宇宙の命題と同値であることを示す。分出にはさらに separateFromSmall を適用する必要がある。そして項代数が始まる。構造、その台を周囲の宇宙へ写す写像、そして台の上の整列順序を引数とするのである。
module D0 = Δ₀Small {ℓc = ℓ-suc ℓ} {K = ⊥* {ℓ-suc ℓ}} (λ b → ⊥*-rec b)
using ( Δ₀-small )
module TermAlgebra (𝒮 : ZFStructureₕ (ℓ-suc ℓ))
(toSet : ZFStructure.S 𝒮 → V ℓ)
(wo : SWO (ZFStructure.S 𝒮))
(junk : ZFStructure.S 𝒮)
{K : Type ℓ} (emb : K → ZFStructure.S 𝒮) where
残りの引数は、既定の要素 junk と、K で索引づけられた基底の生成元の族である。K を始集合の提示と同一視するのは、後の包の実例である。既定の値は簿記のためのもので、後の構成がそれを調べることはない。
ここで隠すのは引数構造の修飾されていない Agda 名 _∈ˢ_ だけであり、充足関係 _⊨₀_ の原子的所属は引き続き 𝒮 によって解釈される。台の名前を替えるのは、本章が周囲の台を指すときの曖昧さをなくすためである。
open ZFStructure 𝒮 hiding ( _∈ˢ_ ) renaming ( S to S𝒮 )
項代数の充足は、自明に空な定数領域のもとで述べられる。評価される論理式は、定数記号を使わずに作られたものだけで、純粋な所属と等号の言語であり、充足は命題値である。この節の各問いと閉包の主張は、すべてこの読みを用いる。
private module Sem = FOL.Semantics 𝒮
module At0 = Sem.At (⊥* {ℓ}) ⊥*-rec using ( _⊨_ )
_⊨₀_ : {n : ℕ} → Vec S𝒮 n → Formula (⊥* {ℓ}) n → hProp (ℓ-suc ℓ)
_⊨₀_ = At0._⊨_
コードは、基底の生成元の上の有限な木の代数を作る。基のコードは生成元を名指し、証人のコードは、アリティが suc k の問いと k 個の引数のコードを記録する。Code は帰納型なので各コードは有限木であり、cs の各成分はその直接の引数部分木である。各部分木は基コードでも証人コードでもかまわない。
data Code : Type ℓ where
base : K → Code
wit : (k : ℕ) → Formula (⊥* {ℓ}) (suc k) → Vec Code k → Code
Sat k ψ vs は、任意の引数のベクトル vs のもとで ψ を満たす要素の単なる存在である。閉包の定理は後に vs をコードの値として特殊化する。充足可能性は切り詰められた存在として述べられ、証人を産み出すことなく、存在を主張するだけである。
Sat : (k : ℕ) → Formula (⊥* {ℓ}) (suc k) → Vec S𝒮 k → Type (ℓ-suc ℓ)
Sat k ψ vs = ∥ Σ[ a ∶ S𝒮 ] ⟨ (a ∷ vs) ⊨₀ ψ ⟩ ∥₁
satDecision : (k : ℕ) (ψ : Formula (⊥* {ℓ}) (suc k)) (vs : Vec S𝒮 k)
→ Dec (Sat k ψ vs)
satDecision k ψ vs = Sem.decideSatisfaction ⊥*-rec lem vs (∃̇ ψ)
探索述語は、問いにすでに格納された論理式によって表示される。その環境は候補を新しい先頭の枠に置き、その後ろに固定された引数ベクトルを続ける。ホスト述語は定義によりまさにこの充足判断なので、読み取りの証明は反射律である。
searchPredicate : (k : ℕ) (ψ : Formula (⊥* {ℓ}) (suc k)) (vs : Vec S𝒮 k)
→ Sem.FormulaPredicate S𝒮 (⊥* {ℓ}) ⊥*-rec
(λ a → (a ∷ vs) ⊨₀ ψ)
searchPredicate k ψ vs = Sem.presented (suc k) ψ (λ a → a ∷ vs) (λ a → refl)
この切り詰められた存在が与えられれば、search は、引数 wo として渡された特定の狭義整列順序のもとで最小の充足要素を返す。最小とはその整列順序での最小のことであり、所属に関する極小でもランクの比較でもない。
search : (k : ℕ) (ψ : Formula (⊥* {ℓ}) (suc k)) (vs : Vec S𝒮 k)
→ Sat k ψ vs → S𝒮
search k ψ vs w = leastOfFormula wo (searchPredicate k ψ vs) lem w .fst
コードのベクトルは成分ごとに評価され、単一のコードの評価と相互に定義される。証人のコードの引数の値は、その成分のコードの値である。
mutual
vals : {m : ℕ} → Vec Code m → Vec S𝒮 m
vals [] = []
vals (c ∷ cs') = val c ∷ vals cs'
充足可能な証人のコードは最小の充足要素へ評価され、充足しない証人のコードは junk へ評価される。すべてのコードが像に値を供給するため、junk が包の中に現れることもある。しかし val-wit が示すのは、充足可能性が与えられれば junk は無関係だということである。
val : Code → S𝒮
val (base m) = emb m
val (wit k ψ cs) = decRec (search k ψ (vals cs)) (λ _ → junk)
(satDecision k ψ (vals cs))
この小さな補題は、命題の目標に要素があると分かったとき、古典的な判定がどのように使われるかを記録する。判定が左枝なら、命題性によりその要素は x と同一視され、消去結果は f x になる。右枝なら、その否定は x と矛盾するため、その場合は不可能である。
sum-stuck : {X : Type (ℓ-suc ℓ)} (x : X) (px : isProp X)
→ (f : X → S𝒮) (g : (X → ⊥₀) → S𝒮) (s : Dec X)
→ decRec f g s ≡ f x
sum-stuck x px f g (yes x') = sym (cong f (px x x'))
sum-stuck x px f g (no h) = ⊥₀-rec (h x)
証人コードに格納された問いの充足可能性の証拠が与えられると、この補題は、そのコードの値が探索の最小の充足要素と同一視されることを示す。既定の枝は反証され、証人のある枝が探索を実行する。
val-wit : (k : ℕ) (ψ : Formula (⊥* {ℓ}) (suc k)) (cs : Vec Code k)
→ (w : Sat k ψ (vals cs)) → val (wit k ψ cs) ≡ search k ψ (vals cs) w
val-wit k ψ cs w = sum-stuck w squash₁ (search k ψ (vals cs)) (λ _ → junk)
(satDecision k ψ (vals cs))
コードのベクトルの評価は、その上で評価を写すことと同じであり、簡単な再帰で示される。これにより、後の主張は環境の再帰的な形と写した形の間を自由に行き来できる。
vals≡map : {m : ℕ} (cs : Vec Code m) → vals cs ≡ map val cs
vals≡map [] = refl
vals≡map (c ∷ cs') = cong₂ _∷_ refl (vals≡map cs')
包の提示は、階層が集合を提示するのと同じ仕方である。コードの族と評価による。包はすべてのコードの値の像であり、異なるコードが同じ値に評価されうるので、提示は要素を重複して持ちえる。したがって包の中の所属は、コードの存在の切り詰められた主張にすぎず、包が推移的であることや、最小の閉じた集合であることは、本章では主張されない。
Hull : V ℓ
Hull = sett Code (λ c → toSet (val c))
提示の中の所属は直接である。どのコードの値も包の要素であり、その証人はそのコード自身である。
inHull : (c : Code) → ⟨ toSet (val c) ∈ˢ Hull ⟩
inHull c = ∣ c , refl ∣₁
こうして、充足可能な符号化された問いはどれも、包の中に充足する証人をもつ。この定理が主張するのはこの閉包の性質であり、包のすべての要素を成功した最小の証人として特徴づけるものではない。
closed : (k : ℕ) (ψ : Formula (⊥* {ℓ}) (suc k)) (cs : Vec Code k)
→ Sat k ψ (vals cs)
→ ∥ Σ[ a ∶ S𝒮 ]
(⟨ toSet a ∈ˢ Hull ⟩ × ⟨ (a ∷ vals cs) ⊨₀ ψ ⟩) ∥₁
closed k ψ cs w = ∣ a , a∈H , sat ∣₁
証人を改めて探す必要はない。項代数がすでに割り当てた値、すなわち探索が返した最小の充足要素がそれである。
where
a : S𝒮
a = search k ψ (vals cs) w
選択子は a と IsLeast の二成分、すなわち a が問いを満たす証明と、それより真に小さい充足要素がない証明を返す。この行は前者を射影する。
pa : ⟨ (a ∷ vals cs) ⊨₀ ψ ⟩
pa = leastOfFormula wo (searchPredicate k ψ (vals cs)) lem w .snd .fst
証人が包に属することは、まさにこの問いのために作られた証人のコードから来る。その値は val-wit によって探索の結果と同一視され、すべてのコードの値は包の中にある。
a∈H : ⟨ toSet a ∈ˢ Hull ⟩
a∈H = subst (λ z → ⟨ toSet z ∈ˢ Hull ⟩) (val-wit k ψ cs w)
(inHull (wit k ψ cs))
充足は記録された成分であり、閉包の節はこれで完成である。
sat : ⟨ (a ∷ vals cs) ⊨₀ ψ ⟩
sat = pa
台の写像に沿って充足関係を移す
包が作られ閉じたので、本章は二つ目の作業、構造の間の充足の移送に移る。移送は、周囲の台の上の二つの述語に対して述べられる。
module SatTransfer (MA MB : S → hProp (ℓ-suc ℓ)) where
源の台は、周囲の台の各要素と、それが第一の述語を満たすことの証明の対である。その論理式は、このような対のもとでのみ読まれる。
SA : Type (ℓ-suc ℓ)
SA = Σ[ x ∶ S ] ⟨ MA x ⟩
目標の台は、第二の述語に対する同じ構成であり、そこの充足は同じ論理式の目標の読みである。
SB : Type (ℓ-suc ℓ)
SB = Σ[ x ∶ S ] ⟨ MB x ⟩
源の構造は、対になった台のもとで論理式を読む。項の辞書は変数を対の要素として評価し、充足は命題値である。
module SemA = FOL.Semantics (𝒮ᵥ ↾ MA)
using ( module At )
module SemB = FOL.Semantics (𝒮ᵥ ↾ MB)
using ( module At )
open SemA.At SA id renaming ( _⊨_ to _⊨ᴬ_ ; ⟦_⟧ to ⟦_⟧ᴬ )
目標の構造は、反対側で同じことを行い、固有の充足と固有の項の辞書をもつ。
open SemB.At SB id renaming ( _⊨_ to _⊨ᴮ_ ; ⟦_⟧ to ⟦_⟧ᴮ )
移送は二つの原理で組織される。一致とは、すべての論理式と環境に対して、左の充足と写された環境での写された論理式の充足が等しい、という命題の等式である。次に述べる証人の原理は存在量化の逆向きを支える。目標側の存在が成り立つとき、その像が行列を充足する q : SA が単に存在すればよいのである。
Agree : (SA → SB) → Type (ℓ-suc (ℓ-suc ℓ))
Agree g = (n : ℕ) (φ : Formula SA n) (δ : Vec SA n)
→ (δ ⊨ᴬ φ) ≡ (map g δ ⊨ᴮ mapFo g φ)
Witness : (SA → SB) → Type (ℓ-suc ℓ)
Witness g = (n : ℕ) (φ : Formula SA (suc n)) (δ : Vec SA n)
この q が、すでに選ばれた目標側の証人の逆像である必要はない。この原理が主張するのは、その像が行列を充足する内側の点の存在の切り詰められた主張であり、これがまさに存在量化の逆方向が消費する形である。
→ ⟨ map g δ ⊨ᴮ mapFo g (∃̇ φ) ⟩
→ ∥ Σ[ q ∶ SA ] ⟨ (g q ∷ map g δ) ⊨ᴮ mapFo g φ ⟩ ∥₁
移送のモジュールは、写像と原子的な仮定を受け取る。原子的な所属と等号には、g を越えた双方向の一致が必要である。そうして初めて、帰納の中の所属と等号のアトムが命題のパスになる。
module Along (g : SA → SB)
(at∈ : (n : ℕ) (t u : Term SA n) (δ : Vec SA n)
→ (δ ⊨ᴬ (t ∈̇ u)) ≡ (map g δ ⊨ᴮ mapFo g (t ∈̇ u)))
(at≐ : (n : ℕ) (t u : Term SA n) (δ : Vec SA n)
→ (δ ⊨ᴬ (t ≐ u)) ≡ (map g δ ⊨ᴮ mapFo g (t ≐ u)))
(wit : Witness g) where
証人の原理が第三の仮定であり、移送のデータはこれでそろう。
最初の弱化補題は源の構造で述べられる。suc による改名は各既存変数を環境の新しい先頭要素の後へずらすため、x ∷ δ での評価は δ での評価に戻り、定数は影響を受けない。
private
renA : {n : ℕ} (t : Term SA n) (x : SA) (δ : Vec SA n)
→ ⟦ renameTm suc t ⟧ᴬ (x ∷ δ) ≡ ⟦ t ⟧ᴬ δ
renA (con c) x δ = refl
renA (var i) x δ = refl
同じ弱めは目標の構造でも成立する。次の主張は、写しと弱めの比較を始める。
renB : {n : ℕ} (t : Term SB n) (x : SB) (δ : Vec SB n)
→ ⟦ renameTm suc t ⟧ᴮ (x ∷ δ) ≡ ⟦ t ⟧ᴮ δ
renB (con c) x δ = refl
renB (var i) x δ = refl
mapTm-ren : {n : ℕ} (t : Term SA n)
写しと弱めは項の上で交換する。これは定義的なことで、弱めた項の写しは、改名された各成分を順に弱める。
→ mapTm g (renameTm suc t) ≡ renameTm suc (mapTm g t)
mapTm-ren (con c) = refl
mapTm-ren (var i) = refl
写して弱めた項を任意の目標点 x と写された環境で評価した値は、写された項を写された環境で評価した値と一致する。
renG : {n : ℕ} (t : Term SA n) (x : SB) (δ : Vec SA n)
→ ⟦ mapTm g (renameTm suc t) ⟧ᴮ (x ∷ map g δ) ≡ ⟦ mapTm g t ⟧ᴮ (map g δ)
renG t x δ = cong (λ u → ⟦ u ⟧ᴮ (x ∷ map g δ)) (mapTm-ren t)
∙ renB (mapTm g t) x (map g δ)
項に対する所属は弱めで変わらず、その形は有界の場合が消費するものである。次の補題が、副条件の移送そのものを述べる。
memRen : {n : ℕ} (t : Term SA n) (x : SB) (δ : Vec SA n)
→ (x .fst ∈ˢ (⟦ mapTm g (renameTm suc t) ⟧ᴮ (x ∷ map g δ)) .fst)
≡ (x .fst ∈ˢ (⟦ mapTm g t ⟧ᴮ (map g δ)) .fst)
memRen t x δ = cong (λ s → x .fst ∈ˢ s .fst) (renG t x δ)
memPath : {n : ℕ} (t : Term SA n) (q : SA) (δ : Vec SA n)
有界量化子の副条件は、写像を越えて移る。連鎖は、源の構造で弱めることから始まり、ずらした環境のもとで所属の原子的な仮定を適用する。
→ (q .fst ∈ˢ (⟦ t ⟧ᴬ δ) .fst)
≡ ((g q) .fst ∈ˢ (⟦ mapTm g t ⟧ᴮ (map g δ)) .fst)
memPath {n} t q δ =
cong (λ s → q .fst ∈ˢ s .fst) (sym (renA t q δ))
∙ at∈ (suc n) (var zero) (renameTm suc t) (q ∷ δ)
連鎖は、目標の構造での弱めで終わる。これで、どの有界の場合の副条件も、写像の両側で読める。
∙ memRen t (g q) δ
古典的な段階は一度だけまとめられる。命題に対する二重否定の除去は排中律から従う。全称の場合の順方向では、目標側の反例を仮定し、それを否定された行列の存在証人として包み、Witness で内側へ引き戻して矛盾を導く。最後に dne が必要な目標側の真理を与える。
dne : (P : hProp (ℓ-suc ℓ)) → (((⟨ P ⟩) → ⊥₀) → ⊥₀) → ⟨ P ⟩
dne P h = decRec (λ p → p)
(λ (np : ⟨ P ⟩ → ⊥₀) → ⊥₀-rec (h np)) (lem P)
帰納は十の場合を通って始まる。最初の二つは仮定そのものであり、at∈ と at≐ である。命題の結合子は成分ごとに運ばれる。命題の上の合取・選言・含意は成分で決まるからである。
agree : Agree g
agree n (t ∈̇ u) δ = at∈ n t u δ
agree n (t ≐ u) δ = at≐ n t u δ
agree n (φ ∧̇ ψ) δ = cong₂ _⊓_ (agree n φ δ) (agree n ψ δ)
agree n (φ ∨̇ ψ) δ = cong₂ _⊔_ (agree n φ δ) (agree n ψ δ)
含意も同じく成分ごとに運ばれ、偽は一定である。存在の節は同値で始まる。順方向は、内側での存在の充足が、写された環境のもとで写された存在の充足へ写ることを述べる。
agree n (φ ⇒̇ ψ) δ = cong₂ _⇒_ (agree n φ δ) (agree n ψ δ)
agree n ⊥̇ δ = refl
agree n (∃̇ ψ) δ = ⇔toPath fwd bwd
where
fwd : ⟨ δ ⊨ᴬ (∃̇ ψ) ⟩ → ⟨ map g δ ⊨ᴮ mapFo g (∃̇ ψ) ⟩
順方向は内側の証人の切り詰めを消去して証人を写す。逆方向こそ、証人の原理が働く場所である。外側の充足を証人の原理に渡すと、その像が行列を充足する内側の点が返り、一致がその充足を運び戻す。
fwd = rec₁ ((map g δ ⊨ᴮ mapFo g (∃̇ ψ)) .snd)
(λ { (q , hq) → ∣ g q , subst ⟨_⟩ (agree (suc n) ψ (q ∷ δ)) hq ∣₁ })
bwd : ⟨ map g δ ⊨ᴮ mapFo g (∃̇ ψ) ⟩ → ⟨ δ ⊨ᴬ (∃̇ ψ) ⟩
bwd h = map₁ (λ { (q , hq) →
q , subst ⟨_⟩ (sym (agree (suc n) ψ (q ∷ δ))) hq }) (wit n ψ δ h)
全称の節が古典的な部分である。順方向は、すべての内側の点が行列を充足すると仮定し、外側の点 x を固定して、x が像の中で行列を充足することを示す。証明は二重否定の除去から始まり、ここで排中律が移送に入る。
agree n (∀̇ ψ) δ = ⇔toPath fwd bwd
where
fwd : ((q : SA) → ⟨ (q ∷ δ) ⊨ᴬ ψ ⟩)
→ (x : SB) → ⟨ (x ∷ map g δ) ⊨ᴮ mapFo g ψ ⟩
fwd h x = dne ((x ∷ map g δ) ⊨ᴮ mapFo g ψ) λ nx →
もし x が失敗するなら、写された環境は x で否定された行列を充足する。その否定に証人の原理を施すと、像が否定を充足する内側の点が返り、その点での一致が、すべての内側の点が行列を充足するという仮定と矛盾する。
rec₁ isProp⊥ (λ { (q , hq) →
lower (hq (subst ⟨_⟩ (agree (suc n) ψ (q ∷ δ)) (h q))) })
(wit n (¬̇ ψ) δ ∣ x , (λ yes → lift (nx yes)) ∣₁)
bwd : ((x : SB) → ⟨ (x ∷ map g δ) ⊨ᴮ mapFo g ψ ⟩)
→ (q : SA) → ⟨ (q ∷ δ) ⊨ᴬ ψ ⟩
逆方向は直接である。すべての内側の点は外側の台へ写るからである。有界全称は、補助の論理式で始まる。それは、名前を替えた上界への所属と、行列の否定を連言したもので、「上界には属するが行列は成立しない」という古典的な読みである。
bwd h q = subst ⟨_⟩ (sym (agree (suc n) ψ (q ∷ δ))) (h (g q))
agree n (∀̇∈ t ψ) δ = ⇔toPath fwd bwd
where
mat : Formula SA (suc n)
mat = (var zero ∈̇ renameTm suc t) ∧̇ ¬̇ ψ
順方向は、上界の中のすべての内側の点が行列を充足するなら、写された上界に属するすべての外側の点が写された行列を充足する、と述べる。証明は再び二重否定の除去から始まり、外側の点が失敗すると仮定する。
fwd : ((q : SA) → ⟨ q .fst ∈ˢ (⟦ t ⟧ᴬ δ) .fst ⟩ → ⟨ (q ∷ δ) ⊨ᴬ ψ ⟩)
→ (x : SB) → ⟨ x .fst ∈ˢ (⟦ mapTm g t ⟧ᴮ (map g δ)) .fst ⟩
→ ⟨ (x ∷ map g δ) ⊨ᴮ mapFo g ψ ⟩
fwd h x hx =
dne ((x ∷ map g δ) ⊨ᴮ mapFo g ψ) λ nx →
証人の原理を補助の論理式に施すと、内側の点 q が返る。その像は上界に属するが、行列を反証する。像の上界への所属は、弱めと memPath を通して運び戻され、一致が行列の内側での充足を像へ持ち上げて、失敗と矛盾する。
rec₁ isProp⊥ (λ { (q , hq) →
lower (hq .snd (subst ⟨_⟩ (agree (suc n) ψ (q ∷ δ))
(h q (subst ⟨_⟩ (sym (memPath t q δ))
(subst ⟨_⟩ (memRen t (g q) δ) (hq .fst)))))) })
(wit n mat δ ∣ x , (subst ⟨_⟩ (sym (memRen t x δ)) hx
補助の適用は証人の記録で閉じ、その第二成分は像における行列の失敗、すなわち否定された行列である。逆方向は、像のもとの外側の充足と内側の副条件から、内側の行列の充足が出ることを述べる。
, (λ yes → lift (nx yes))) ∣₁)
bwd : ((x : SB) → ⟨ x .fst ∈ˢ (⟦ mapTm g t ⟧ᴮ (map g δ)) .fst ⟩
→ ⟨ (x ∷ map g δ) ⊨ᴮ mapFo g ψ ⟩)
→ (q : SA) → ⟨ q .fst ∈ˢ (⟦ t ⟧ᴬ δ) .fst ⟩ → ⟨ (q ∷ δ) ⊨ᴬ ψ ⟩
bwd h q hq =
逆方向は、内側の点の像のもとで外側の充足を適用する。副条件は memPath で、行列は一致で運ばれる。有界存在は、副条件と行列自身を連言した補助の行列で始まる。
subst ⟨_⟩ (sym (agree (suc n) ψ (q ∷ δ)))
(h (g q) (subst ⟨_⟩ (memPath t q δ) hq))
agree n (∃̇∈ t ψ) δ = ⇔toPath fwd bwd
where
mat : Formula SA (suc n)
補助の行列は、副条件と行列の連言であり、順方向は、内側の証人の対が外側の証人の対へ写ると述べる。証明は、切り詰めの上の一回の写しである。
mat = (var zero ∈̇ renameTm suc t) ∧̇ ψ
fwd : ∥ Σ[ q ∶ SA ] (⟨ q .fst ∈ˢ (⟦ t ⟧ᴬ δ) .fst ⟩ × ⟨ (q ∷ δ) ⊨ᴬ ψ ⟩) ∥₁
→ ∥ Σ[ x ∶ SB ] (⟨ x .fst ∈ˢ (⟦ mapTm g t ⟧ᴮ (map g δ)) .fst ⟩
× ⟨ (x ∷ map g δ) ⊨ᴮ mapFo g ψ ⟩) ∥₁
fwd = map₁ (λ { (q , hq , hψ) →
二つの成分は別々に運ばれる。副条件は memPath で、行列は一致によって運ばれる。逆方向はその逆を述べ、外側の証人の対が内側の対を与える。
g q , (subst ⟨_⟩ (memPath t q δ) hq ,
subst ⟨_⟩ (agree (suc n) ψ (q ∷ δ)) hψ) })
bwd : ∥ Σ[ x ∶ SB ] (⟨ x .fst ∈ˢ (⟦ mapTm g t ⟧ᴮ (map g δ)) .fst ⟩
× ⟨ (x ∷ map g δ) ⊨ᴮ mapFo g ψ ⟩) ∥₁
→ ∥ Σ[ q ∶ SA ] (⟨ q .fst ∈ˢ (⟦ t ⟧ᴬ δ) .fst ⟩ × ⟨ (q ∷ δ) ⊨ᴬ ψ ⟩) ∥₁
逆方向は、補助の形で読んだ外側の対に証人の原理を走らせ、内側の点とその像の対を得る。成分は、弱めと memPath、そして一致によって運び戻される。
bwd h = map₁ (λ { (q , hq) →
q , ( subst ⟨_⟩ (sym (memPath t q δ))
(subst ⟨_⟩ (memRen t (g q) δ) (hq .fst))
, subst ⟨_⟩ (sym (agree (suc n) ψ (q ∷ δ))) (hq .snd)) })
(wit n mat δ (map₁ (λ { (x , hx , hψ) →
二つの成分が有界存在の移送を閉じ、十場合の帰納が完了する。
x , (subst ⟨_⟩ (sym (memRen t x δ)) hx , hψ) }) h))
段階内部の Tarski-Vaught 判定条件
順序数の指数 α に対し、段階 Lset α を周囲の構造とすれば、上の移送からその内部での初等性が得られる。
module AtStage (α : S) (ordα : IsOrd α) where
段階は推移的である。その理由は正確にはこうである。Lset-layer α が α における層の推移性の証明を与え、layer-trans がそれを Lset α の推移性へ変える。順序数性の仮定はここでは使われず、下の整列順序のために取ってある。
Ltr : isTransV (Lset α)
Ltr = layer-trans (Lset-layer α)
推移性により、有界論理式は Lset α の内部と宇宙全体とで絶対的になる。したがって、段階に制限した構造を Tarski-Vaught の議論の外側の意味論として使える。
module AbsL = FOL.Absoluteness.Single 𝒮ᵥ (λ x → x ∈ˢ Lset α) Ltr
using ( SM; 𝒮M; _⊨ᵐ_; ⟦_⟧ᵐ; abs₀ )
段階の台は、Lset α に属する要素の型である。以下のどの包の要素も、どの段階での読みも、この型の中にある。
SL : Type (ℓ-suc ℓ)
SL = AbsL.SM
前章の段階の順序は、この台の上の整列順序に制限される。この段階に含まれる台 M を固定し、段階への包含を仮定する。
wL : SWO SL
wL = orderAt α ordα
module AtM (M : S) (M⊆L : (x : S) → ⟨ x ∈ˢ M ⟩ → ⟨ x ∈ˢ Lset α ⟩) where
部分構造の台は、周囲の台の要素と、それが M に属することの証明の対である。論理式はこのような対のもとでのみ読まれる。
SM : Type (ℓ-suc ℓ)
SM = Σ[ x ∶ S ] ⟨ x ∈ˢ M ⟩
部分構造の意味論は、周囲の意味論の M への制限である。項は制限の内側で評価され、充足は命題値である。
module SemM = FOL.Semantics (𝒮ᵥ ↾ (λ x → x ∈ˢ M))
using ( module At )
open SemM.At SM id renaming ( _⊨_ to _⊨ᵐ_ ; ⟦_⟧ to ⟦_⟧ᵐ )
段階への包含は、台の各要素をその段階での所属と対にする。これは包含の仮定が供給する。
inL : SM → SL
inL c = c .fst , M⊆L (c .fst) (c .snd)
初等性は、この包含のもとで充足が変わらないことを、台のすべての論理式と環境に対して述べる。これは命題の間のパスであり、二つの原子式についての合同性と証人の原理がこの形で合成される。
Elementary : Type (ℓ-suc (ℓ-suc ℓ))
Elementary = (n : ℕ) (φ : Formula SM n) (δ : Vec SM n)
→ (δ ⊨ᵐ φ) ≡ (map inL δ AbsL.⊨ᵐ (mapFo inL φ))
Tarski-Vaught の判定条件は、初等性の証人の形である。段階がある環境の像のもとで存在の論理式を充足するなら、台のある要素の像がそこで行列を充足する。充足が命題値なので、単に存在すれば足りる。
TarskiVaught : Type (ℓ-suc ℓ)
TarskiVaught = (n : ℕ) (φ : Formula SM (suc n)) (δ : Vec SM n)
→ ⟨ map inL δ AbsL.⊨ᵐ (mapFo inL (∃̇ φ)) ⟩
→ ∥ Σ[ q ∶ SM ] ⟨ (inL q ∷ map inL δ) AbsL.⊨ᵐ (mapFo inL φ) ⟩ ∥₁
各点での包含は環境の参照と可換である。これは項の一致に必要な変数の場合である。
private
lookup-inL : {n : ℕ} (i : Fin n) (δ : Vec SM n)
→ lookup i (map inL δ) ≡ inL (lookup i δ)
lookup-inL zero (c ∷ δ) = refl
lookup-inL (suc i) (c ∷ δ) = lookup-inL i δ
項は包含の両側で一致する。台の項は、部分構造で読んでも、写して段階で読んでも、同じ底の要素に評価される。定数は固定的で、変数は参照に従う。そして移送の仕組みが、二つの所属の述語のもとで具体化される。
tm-agree : (n : ℕ) (t : Term SM n) (δ : Vec SM n)
→ (⟦ t ⟧ᵐ δ) .fst ≡ (AbsL.⟦ mapTm inL t ⟧ᵐ (map inL δ)) .fst
tm-agree n (con c) δ = refl
tm-agree n (var i) δ = sym (cong (λ p → p .fst) (lookup-inL i δ))
module Tr = SatTransfer (λ x → x ∈ˢ M) (λ x → x ∈ˢ Lset α)
初等性は、共有の帰納を具体化して得られる。二つの原子式の場合は、今証明した充足関係の合同性から得られ、証人の原理がちょうど Tarski-Vaught の実例で、ブールと量化子の場合は共有の本体が運ぶ。二つの合同性と判定条件を除けば、段階に固有のことは何も使われない。
TV→elem : TarskiVaught → Elementary
TV→elem tv = Tr.Along.agree inL
(λ n t u δ → cong₂ _∈ˢ_ (tm-agree n t δ) (tm-agree n u δ))
(λ n t u δ → cong₂ _≈ˢ_ (tm-agree n t δ) (tm-agree n u δ))
tv
始集合を最小の証人について閉じる
始集合 X がこの段階に含まれ、指数 α が空集合を含むと仮定する。空集合が Lset α に属するのは、∅ が順序数 α の中にあり、基底の層で符号化されているからである。
module Hull (X : S) (X⊆L : (x : S) → ⟨ x ∈ˢ X ⟩ → ⟨ x ∈ˢ Lset α ⟩)
(∅∈α : ⟨ ∅ ∈ˢ α ⟩) where
∅∈Lsetα : ⟨ ∅ ∈ˢ Lset α ⟩
∅∈Lsetα = Lset-in α ∅ ∅ ∅∈α (∅∈𝒟ₒ ∅)
始集合の提示の埋め込みは、段階の台の中に着地する。各索引は X の要素を名指し、包含の仮定がその要素が段階 Lset α に属することを証明する。
inStg : ⟪ X ⟫ → SL
inStg m = ⟪ X ⟫↪ m , X⊆L (⟪ X ⟫↪ m) (member X m)
項代数は、段階の制限された構造のもとで具体化される。台は第一射影で宇宙へ写され、証人の探索は段階の整列順序を使い、既定の値は空集合、基のコードは X の提示で索引づけられる。包はこうして段階の中で育つ。
module T = TermAlgebra AbsL.𝒮M (λ p → p .fst) wL (∅ , ∅∈Lsetα) {K = ⟪ X ⟫} inStg
open T using ( Code; base; val; Hull; inHull )
包は段階の中にある。すべての要素はあるコードの値であり、コードの値は項代数自身の型づけによって段階 Lset α の要素である。証明は切り詰められた提示を消去し、同一視に沿って輸送する。
Hull⊆L : (x : S) → ⟨ x ∈ˢ Hull ⟩ → ⟨ x ∈ˢ Lset α ⟩
Hull⊆L x x∈H = rec₁ ((x ∈ˢ Lset α) .snd) go x∈H
where
go : Σ[ c ∶ Code ] ((val c) .fst ≡ x) → ⟨ x ∈ˢ Lset α ⟩
go (c , q) = subst (λ z → ⟨ z ∈ˢ Lset α ⟩) q ((val c) .snd)
所属は、切り詰められた存在としてしか読み戻せない。包の要素はあるコードの値であるが、コードは選ばれない。異なるコードが同じ値に評価しうるので、これが提示の正直な形である。
hull-member : (x : S) → ⟨ x ∈ˢ Hull ⟩
→ ∥ Σ[ c ∶ Code ] ((val c) .fst ≡ x) ∥₁
hull-member x x∈H = x∈H
逆方向には切り詰めは要らない。提示自身の導入規則により、どのコードの値も要素である。
val-in-Hull : (c : Code) → ⟨ (val c) .fst ∈ˢ Hull ⟩
val-in-Hull c = inHull c
始集合は要素ごとに包に入る。X の要素 x は索引によって提示され、x における提示の繊維がその索引を返す。
module XInM (x : S) (x∈X : ⟨ x ∈ˢ X ⟩) where
mx : ⟪ X ⟫
mx = fiber X x∈X .fst
繊維は、提示された要素を x と同一視するパスを運び、所属を運ぶときの道すじになる。
x≡val : ⟪ X ⟫↪ mx ≡ x
x≡val = fiber X x∈X .snd
その索引での基のコードは、提示された要素、すなわち x へ評価される。輸送によって、x の包の中の所属が着地する。
inM : ⟨ x ∈ˢ Hull ⟩
inM = subst (λ z → ⟨ z ∈ˢ Hull ⟩) x≡val (inHull (base mx))
一度組み立てれば、始集合の包への包含は一つの補題になる。
X⊆M : (x : S) → ⟨ x ∈ˢ X ⟩ → ⟨ x ∈ˢ Hull ⟩
X⊆M x x∈X = XInM.inM x x∈X
充足関係は崩壊同型で不変である
同型の前後で充足関係を比較するため、集合 M、PM と、M の要素を PM の要素へ送る台の写像 p を固定する。
module IsoInv (M : S) (PM : S)
(p : S → S)
(p∈ : (x : S) → ⟨ x ∈ˢ M ⟩ → ⟨ p x ∈ˢ PM ⟩)
(iso-fwd : (x y : S) (x∈ : ⟨ x ∈ˢ M ⟩) (y∈ : ⟨ y ∈ˢ M ⟩)
→ ⟨ y ∈ˢ x ⟩ → ⟨ p y ∈ˢ p x ⟩)
(iso-bwd : (x y : S) (x∈ : ⟨ x ∈ˢ M ⟩) (y∈ : ⟨ y ∈ˢ M ⟩)
→ ⟨ p y ∈ˢ p x ⟩ → ⟨ y ∈ˢ x ⟩)
(p-inj : (x y : S) (x∈ : ⟨ x ∈ˢ M ⟩) (y∈ : ⟨ y ∈ˢ M ⟩)
→ p x ≡ p y → x ≡ y)
(surj : (z : S) (z∈ : ⟨ z ∈ˢ PM ⟩)
→ ∥ Σ[ y ∶ S ] (⟨ y ∈ˢ M ⟩ × (p y ≡ z)) ∥₁)
where
閉性の条件 p∈ に加えて、写像 p には四つの仮定を置く。iso-fwd は所属を保存し、iso-bwd は所属を反映し、最後の二つの引数は M 上の単射性と終域 PM への全射性を述べる。
写像 p は M 上で単射であり、PM へ単に全射である。保存と反映と合わせて、これらはまさに二つの構造の間の所属の同型のデータである。
源の台は、M の各要素とその所属の証明を対にする。本章のどの制限された構造とも同じである。
SM : Type (ℓ-suc ℓ)
SM = Σ[ x ∶ S ] ⟨ x ∈ˢ M ⟩
終域の台は、PM の各要素とその所属の証明を対にする。
SPM : Type (ℓ-suc ℓ)
SPM = Σ[ x ∶ S ] ⟨ x ∈ˢ PM ⟩
同型は、対になった台へ持ち上がる。底の要素に p を施し、像の中での所属を証明するのである。
g : SM → SPM
g m = p (m .fst) , p∈ (m .fst) (m .snd)
module SemM = FOL.Semantics (𝒮ᵥ ↾ (λ x → x ∈ˢ M))
using ( module At )
module SemPM = FOL.Semantics (𝒮ᵥ ↾ (λ x → x ∈ˢ PM))
using ( module At )
open module Mse = SemM.At SM id public renaming ( _⊨_ to _⊨ᵐ_ ; ⟦_⟧ to ⟦_⟧ᵐ )
終域の意味論は、PM に制限した構造で写された項と論理式を解釈する。
open module Pse = SemPM.At SPM id public renaming ( _⊨_ to _⊨ᵖᵐ_ ; ⟦_⟧ to ⟦_⟧ᵖᵐ )
全射は対になった台へ持ち上がる。終域 PM のすべての要素は M のある点の像であり、底の要素の等しさは、PM への所属が命題であるため、対の等しさへ持ち上がる。
surj' : (p' : SPM) → ∥ Σ[ q ∶ SM ] (g q ≡ p') ∥₁
surj' (z , z∈) = map₁ (λ { (y , y∈ , e) →
(y , y∈) , Σ≡Prop (λ w → ⟨ w ∈ˢ PM ⟩isProp) e }) (surj z z∈)
一般の充足関係の移送定理を、M と PM への所属述語に適用できる。所属の保存と反映が、その所属原子式の場合を与える。
module Tr = SatTransfer (λ x → x ∈ˢ M) (λ x → x ∈ˢ PM)
写像 p は環境に各索引ごとに施されるので、参照は一度に一つずつ簡約できる。
private
lookup-g : {n : ℕ} (i : Fin n) (δ : Vec SM n)
→ p ((lookup i δ) .fst) ≡ (lookup i (map g δ)) .fst
lookup-g zero (m ∷ δ) = refl
lookup-g (suc i) (m ∷ δ) = lookup-g i δ
項は写像 p のもとで一致する。M の項の値に p を施すことは、写された項を写された環境で評価することと等しくなる。定数は固定的で、変数は参照に従う。所属の原子式がここで述べられる。
tm-agree : {n : ℕ} (t : Term SM n) (δ : Vec SM n)
→ p ((⟦ t ⟧ᵐ δ) .fst) ≡ (⟦ mapTm g t ⟧ᵖᵐ (map g δ)) .fst
tm-agree (con m) δ = refl
tm-agree (var i) δ = lookup-g i δ
at∈ : (n : ℕ) (t u : Term SM n) (δ : Vec SM n)
原子項の所属は両方向に移る。順方向は、内側の所属を項の等式に沿って運び、所属を保存する iso-fwd に渡す。
→ (δ ⊨ᵐ (t ∈̇ u)) ≡ (map g δ ⊨ᵖᵐ mapFo g (t ∈̇ u))
at∈ n t u δ = ⇔toPath
(λ h → subst (λ z → ⟨ (⟦ mapTm g t ⟧ᵖᵐ (map g δ)) .fst ∈ˢ z ⟩) (tm-agree u δ)
(subst (λ z → ⟨ z ∈ˢ p ((⟦ u ⟧ᵐ δ) .fst) ⟩) (tm-agree t δ)
(iso-fwd ((⟦ u ⟧ᵐ δ) .fst) ((⟦ t ⟧ᵐ δ) .fst) ((⟦ u ⟧ᵐ δ) .snd)
順方向の輸送は、p を施した後の所属に着地する。逆方向は、同型を通してその所属を反映し、項の等式に沿って内側の所属を復元する。
((⟦ t ⟧ᵐ δ) .snd) h)))
(λ h → iso-bwd ((⟦ u ⟧ᵐ δ) .fst) ((⟦ t ⟧ᵐ δ) .fst) ((⟦ u ⟧ᵐ δ) .snd)
((⟦ t ⟧ᵐ δ) .snd)
(subst (λ z → ⟨ p ((⟦ t ⟧ᵐ δ) .fst) ∈ˢ z ⟩) (sym (tm-agree u δ))
(subst (λ z → ⟨ z ∈ˢ (⟦ mapTm g u ⟧ᵖᵐ (map g δ)) .fst ⟩)
逆方向が所属の節を閉じる。項の等式に導かれた同型を通した反映が、内側の所属をちょうど返す。等号の原子式と証人の原理は、残りの仮定が扱う。
(sym (tm-agree t δ)) h)))
アトムの項の等号は、等式の両辺に崩壊を施すことで移る。順方向は、M における値の等式を取り、cong で p を施し、項の同約によって両辺を写された項へ運ぶ。
at≐ : (n : ℕ) (t u : Term SM n) (δ : Vec SM n)
→ (δ ⊨ᵐ (t ≐ u)) ≡ (map g δ ⊨ᵖᵐ mapFo g (t ≐ u))
at≐ n t u δ = ⇔toPath
(λ h → subst (λ z → z ≡ (⟦ mapTm g u ⟧ᵖᵐ (map g δ)) .fst) (tm-agree t δ)
(subst (λ z → p ((⟦ t ⟧ᵐ δ) .fst) ≡ z) (tm-agree u δ) (cong p h)))
逆方向は、単射性が活きる場所である。崩壊した両辺が等しいことから、p-inj がもとの値の等しさを取り戻す。二つの向きで、等号のアトムが命題の間のパスになる。
(λ h → p-inj ((⟦ t ⟧ᵐ δ) .fst) ((⟦ u ⟧ᵐ δ) .fst) ((⟦ t ⟧ᵐ δ) .snd)
((⟦ u ⟧ᵐ δ) .snd)
(subst (λ z → z ≡ p ((⟦ u ⟧ᵐ δ) .fst)) (sym (tm-agree t δ))
(subst (λ z → (⟦ mapTm g t ⟧ᵖᵐ (map g δ)) .fst ≡ z)
(sym (tm-agree u δ)) h)))
証人の原理は全射から作られる。像の中の外側の証人 p' は、単に、M のある q の崩壊である。その同一視に沿って充足を運ぶと、内側の証人と、像の中での充足が得られる。
wit : Tr.Witness g
wit n ψ δ h = rec₁ squash₁
(λ { (p' , hp) → map₁
(λ { (q , gq≡p) →
q , subst (λ z → ⟨ (z ∷ map g δ) ⊨ᵖᵐ mapFo g ψ ⟩) (sym gq≡p) hp })
全射の補題が逆像を供給し、二つの輸送が合わさって、移送の証人の原理になる。
(surj' p') }) h
原子の場合と証人原理がそろうと、共有の帰納により、環境を崩壊で写し、定数を g で付け替えても充足関係が保たれることが分かる。
agree : (n : ℕ) (φ : Formula SM n) (δ : Vec SM n)
→ (δ ⊨ᵐ φ) ≡ (map g δ ⊨ᵖᵐ mapFo g φ)
agree = Tr.Along.agree g at∈ at≐ wit
一致は、後で合成するために二つの片方向の形で記録される。順方向には、内側の充足から、写された環境での写された論理式の充足が得られる。
iso-inv : (n : ℕ) (φ : Formula SM n) (δ : Vec SM n)
→ ⟨ δ ⊨ᵐ φ ⟩ → ⟨ map g δ ⊨ᵖᵐ mapFo g φ ⟩
iso-inv n φ δ = subst ⟨_⟩ (agree n φ δ)
逆方向は、外側の充足を内側の充足へ戻す。本章は次に、外延性をもつ集合 X の崩壊のもとでこの不変性を具体化し、所属の同型と単射性を伴って崩壊を開く。
iso-inv-bwd : (n : ℕ) (φ : Formula SM n) (δ : Vec SM n)
→ ⟨ map g δ ⊨ᵖᵐ mapFo g φ ⟩ → ⟨ δ ⊨ᵐ φ ⟩
iso-inv-bwd n φ δ = subst ⟨_⟩ (sym (agree n φ δ))
module CollapseIso (X : S) (Xext : isExt X) where
module C = Collapse X using ( module InjExt; π; πX; πX-intro; πX-member )
X の外延性こそ、崩壊が必要とするものである。制限された構造は単射となり、X の上の所属と崩壊の像の上の所属の間の同型が使えるようになる。
module CI = C.InjExt Xext using ( iso; π-inj )
目標の台は崩壊像 πX であり、その点はちょうど X の要素の崩壊値である。
PM : S
PM = C.πX
写像 p は各集合をその Mostowski 崩壊値へ送る。
p : S → S
p = C.π
X の要素は像の中に着地する。これは、像に対する崩壊自身の導入規則によるものである。
p∈ : (x : S) → ⟨ x ∈ˢ X ⟩ → ⟨ p x ∈ˢ PM ⟩
p∈ = C.πX-intro
所属は崩壊に沿って順方向に保存される。X の中で y が x に属するなら、y の崩壊は x の崩壊に属する。これが所属の同型の第一成分である。
iso-fwd : (x y : S) (x∈ : ⟨ x ∈ˢ X ⟩) (y∈ : ⟨ y ∈ˢ X ⟩)
→ ⟨ y ∈ˢ x ⟩ → ⟨ p y ∈ˢ p x ⟩
iso-fwd x y x∈ y∈ = CI.iso x y x∈ y∈ .fst
所属は逆方向にも反映される。崩壊された所属は、X の中の本当の所属から生じたものに限る。二つの向き合わせて、崩壊が所属について忠実であることが言える。
iso-bwd : (x y : S) (x∈ : ⟨ x ∈ˢ X ⟩) (y∈ : ⟨ y ∈ˢ X ⟩)
→ ⟨ p y ∈ˢ p x ⟩ → ⟨ y ∈ˢ x ⟩
iso-bwd x y x∈ y∈ = CI.iso x y x∈ y∈ .snd
崩壊は X の上で単射である。崩壊が等しい二つの要素は等しい。所属への忠実さと単射性が、要素の上の同型の二つの半分である。
p-inj : (x y : S) (x∈ : ⟨ x ∈ˢ X ⟩) (y∈ : ⟨ y ∈ˢ X ⟩)
→ p x ≡ p y → x ≡ y
p-inj = CI.π-inj
像のすべての点は X の要素から来る。全射は切り詰められており、証人を選ばずに逆像の存在を主張する。これがまさに、証人の原理が消費する形である。
surj : (z : S) (z∈ : ⟨ z ∈ˢ PM ⟩)
→ ∥ Σ[ y ∶ S ] (⟨ y ∈ˢ X ⟩ × (p y ≡ z)) ∥₁
surj = C.πX-member
外延的な集合 X では、崩壊は所属を保存かつ反映し、X 上で単射であり、πX のすべての点を覆う。
module I = IsoInv X PM p p∈ iso-fwd iso-bwd p-inj surj
using ( SM; SPM; g; surj'; iso-inv; iso-inv-bwd; _⊨ᵐ_; _⊨ᵖᵐ_; ⟦_⟧ᵐ; ⟦_⟧ᵖᵐ )
Skolem 包は初等的である
したがって、X 上の構造と πX 上の構造の間で充足関係を双方向に移せる。
module HullElemDown (α : S) (ordα : IsOrd α)
(X : S) (X⊆L : (x : S) → ⟨ x ∈ˢ X ⟩ → ⟨ x ∈ˢ Lset α ⟩) (∅∈α : ⟨ ∅ ∈ˢ α ⟩) where
これを Lset α 内の Skolem 包に適用すると、初等性は Tarski-Vaught の証人条件に帰着する。
module ASt = AtStage α ordα using ( module AbsL; module AtM; module Hull; SL )
module H = ASt.Hull X X⊆L ∅∈α
using ( module T; Hull⊆L; hull-member )
M : S
M = H.T.Hull
部分構造の仕組みは包のもとで具体化され、その論理式には周囲の読みが与えられる。包の台のすべての要素にはコードがある。コードは切り詰められた提示によって存在し、値と包含の同一視は、段階の所属の命題値性によって持ち上がる。
module A = ASt.AtM M H.Hull⊆L using ( Elementary; SM; module SemM; TV→elem; inL )
module Mse = A.SemM.At A.SM id using ( _⊨_ )
codeOf : (q : A.SM) → ∥ Σ[ c ∶ H.T.Code ] (H.T.val c ≡ A.inL q) ∥₁
codeOf q = map₁ (λ { (c , e) → c , Σ≡Prop (λ z → ⟨ z ∈ˢ Lset α ⟩isProp) e })
(H.hull-member (q .fst) (q .snd))
コードは、一つの要素から有限の環境へ持ち上がる。空の環境は空のベクトルで符号化され、再帰の場合は、新しいコードを、すでに作られたコードの列に加える。
codeEnv : {n : ℕ} (δ : Vec A.SM n)
→ ∥ Σ[ ds ∶ Vec H.T.Code n ]
(map H.T.val ds ≡ map A.inL δ) ∥₁
codeEnv [] = ∣ [] , refl ∣₁
codeEnv (q ∷ δ) = map2
構成の場合は、二つの切り詰められた存在を一つに合成する。延びたコードのベクトルの評価は、包含された環境にちょうど等しくなる。
(λ { (c , ec) (ds , eds) → c ∷ ds , cong₂ _∷_ ec eds })
(codeOf q) (codeEnv δ)
成分ごとの写像は有限環境の連結も保つ。したがって、自由変数の値と定数出現を置き換える値を、Tarski-Vaught の議論に用いる一つの符号化環境へまとめられる。
inL-++ : {n m : ℕ} (δ : Vec A.SM n) (σ : Vec A.SM m)
→ map A.inL (δ ++ σ) ≡ map A.inL δ ++ map A.inL σ
inL-++ [] σ = refl
inL-++ (q ∷ δ) σ = cong (A.inL q ∷_) (inL-++ δ σ)
tv : (n : ℕ) (ψ : Formula A.SM (suc n)) (δ : Vec A.SM n)
この主張は Tarski-Vaught の条件そのものである。段階が包含された環境のもとで存在の論理式を充足するなら、単に、包のある要素がそこで行列を充足する。証明はまず環境の符号化を消去し、探索の閉包へ進む。
→ ⟨ map A.inL δ ASt.AbsL.⊨ᵐ (mapFo A.inL (∃̇ ψ)) ⟩
→ ∥ Σ[ q ∶ A.SM ]
⟨ (A.inL q ∷ map A.inL δ) ASt.AbsL.⊨ᵐ (mapFo A.inL ψ) ⟩ ∥₁
tv n ψ δ h = rec₁ squash₁ takeEnvironment (codeEnv params)
where
パラメータ抽象は各定数出現を追加の自由変数に置き換える。得られる論理式は定数領域が空で、アリティが countFo ψ だけ増えるが、ψ の論理構造はすべて保たれる。
bodyFo : Formula (⊥* {ℓ}) (suc (n + countFo ψ))
bodyFo = absFo ψ
抽象された本体のための環境は、もとの環境に定数の出現を続けたものである。抽象は定数を余分な自由変数に変えるので、一つのベクトルが探索に必要なすべてを運ぶ。
params : Vec A.SM (n + countFo ψ)
params = δ ++ constantsFo ψ
この結合環境のコードが得られると、最小証人についての閉性から包内の証人が得られる。抽象後の論理式ともとのパラメータ付き論理式との意味論的同一視により、必要な Tarski-Vaught の証人が従う。
takeEnvironment : Σ[ ds ∶ Vec H.T.Code (n + countFo ψ) ]
(map H.T.val ds ≡ map A.inL params)
→ ∥ Σ[ q ∶ A.SM ]
⟨ (A.inL q ∷ map A.inL δ) ASt.AbsL.⊨ᵐ
(mapFo A.inL ψ) ⟩ ∥₁
探索の閉包は、符号化された環境のもとで走る。その評価の記録に、符号化の等式と、連結の上の包含の分配を合成すると、コードの評価が包含された引数であることが得られる。
takeEnvironment (ds , eds) = map₁ finish (H.T.closed _ bodyFo ds witness)
where
vals-env : H.T.vals ds
≡ map A.inL δ ++ map A.inL (constantsFo ψ)
vals-env = H.T.vals≡map ds ∙ eds ∙ inL-++ δ (constantsFo ψ)
重要な同一視はこう述べる。符号化された環境のもと、裸の探索の意味論で読んだ抽象された本体は、包含された環境のもと、段階の意味論で読んだ本体と同じ命題だと。
body-path : (b : ASt.SL)
→ ((b ∷ H.T.vals ds) H.T.⊨₀ bodyFo)
≡ ((b ∷ map A.inL δ) ASt.AbsL.⊨ᵐ mapFo A.inL ψ)
body-path b =
cong (λ ε → ε H.T.⊨₀ bodyFo) (cong (b ∷_) vals-env)
このパスは二つの意味論的な整合則を合成する。⊨-abs はパラメータ抽象と拡張環境を結び、⊨-map は付け替えと写された環境を結ぶ。
∙ sym (⊨-abs ASt.AbsL.𝒮M A.inL ψ
(b ∷ map A.inL δ))
∙ sym (⊨-map ASt.AbsL.𝒮M A.inL id ψ
(b ∷ map A.inL δ))
存在の論理式の段階での充足が、体のパスに沿って裸の読みへ運ばれ、探索の閉包が必要とする充足可能性の証人が、ちょうど生み出される。
witness : H.T.Sat (n + countFo ψ) bodyFo (H.T.vals ds)
witness = map₁ (λ { (b , hb) →
b , subst ⟨_⟩ (sym (body-path b)) hb }) h
探索は、符号化された環境のもとで抽象された本体を満たす、包の中の最小の証人を返す。変換は、これをもとの論理式に対する Tarski-Vaught の対へ変える必要がある。
finish : Σ[ a ∶ ASt.SL ]
( ⟨ a .fst ∈ˢ M ⟩
× ⟨ (a ∷ H.T.vals ds) H.T.⊨₀ bodyFo ⟩ )
→ Σ[ q ∶ A.SM ]
⟨ (A.inL q ∷ map A.inL δ) ASt.AbsL.⊨ᵐ (mapFo A.inL ψ) ⟩
証人は、部分構造の台へ読み戻される。底の集合は包であり、所属は今産み出されたものである。
finish (a , a∈H , ha) = q , sat
where
q : A.SM
q = a .fst , a∈H
証人の段階への包含は、証人そのものである。二つの台は、命題値の所属の証明だけが違い、それは反射性によって同一視される。
q≡a : A.inL q ≡ a
q≡a = Σ≡Prop (λ z → ⟨ z ∈ˢ Lset α ⟩isProp) refl
証人のもとの本体の充足は、体のパスに沿って段階の意味論へ、そして証人の同一視に沿って部分構造の台へ運ばれる。これが、もとの論理式と環境に対する Tarski-Vaught の結論にほかならない。
sat : ⟨ (A.inL q ∷ map A.inL δ) ASt.AbsL.⊨ᵐ (mapFo A.inL ψ) ⟩
sat = subst (λ b → ⟨ (b ∷ map A.inL δ) ASt.AbsL.⊨ᵐ
(mapFo A.inL ψ) ⟩)
(sym q≡a) (subst ⟨_⟩ (body-path a) ha)
したがって、Tarski-Vaught 条件から包の Lset α における初等性が得られる。
elem : A.Elementary
elem = A.TV→elem tv
パラメータなし論理式を周囲の宇宙で読む
定数領域が空の論理式では、定数の非自明な付け替えなしに周囲の充足関係を比較できる。
module AtP = SemV.At (⊥* {ℓ-suc ℓ}) (λ b → ⊥*-rec b) using ( _⊨_ )
パラメータなしの論理式の周囲の充足は、再利用のために名付けられる。重要な観察はこうである。パラメータなしの論理式は、改名しても変わらない。写し直す定数がないからである。
_⊨ₚ_ : {n : ℕ} → Vec S n → Formula (⊥* {ℓ-suc ℓ}) n → hProp (ℓ-suc ℓ)
_⊨ₚ_ = AtP._⊨_
embed-map : {ℓ₁ ℓ₂ : Level} {K : Type ℓ₁} {K' : Type ℓ₂} (f : K → K')
{n : ℕ} (φ : Formula (⊥* {ℓ-suc ℓ}) n)
→ mapFo f (embed φ) ≡ embed φ
証明は、写しの法則と、空の領域の埋め込みが出現の上で恒等であるという事実を合成する。改名が動かすものは何も残っていない。
embed-map f φ =
mapFo-comp ⊥*-rec f φ
∙ cong (λ h → mapFo h φ) (funExt (λ b → ⊥*-rec b))
opaque
isOrdAt : Formula (⊥* {ℓ-suc ℓ}) 1
順序数性は、一つの枠をもつ有界論理式によって、引数自身が推移的であり、そのすべての要素も推移的であることとして表される。
isOrdAt =
(∀̇∈ (var zero) (∀̇∈ (var zero) (var zero ∈̇ var (suc (suc zero)))))
∧̇ (∀̇∈ (var zero) (∀̇∈ (var zero) (∀̇∈ (var zero) (var zero ∈̇ var (suc (suc zero))))))
Δ₀ の証拠は外側の連言を通り、第一の節の二つと第二の節の三つの有界量化子をたどって、所属の原子式に至る。
Δ₀-isOrdAt : Δ₀ isOrdAt
Δ₀-isOrdAt =
δ-∧ (δ-∀∈ (δ-∀∈ δ-∈))
(δ-∀∈ (δ-∀∈ (δ-∀∈ δ-∈)))
二つの読み取り補題は、isOrdAt の充足と順序数述語を双方向に正確に対応させる。
module Amb where
opaque
unfolding isOrdAt
論理式から順序数性を読み出すとは、二つの有界の節を、順序数の述語の二つの欄へ開くことである。引数の推移性と、すべての要素の推移性である。
isOrdAt-out : (x : S) → ⟨ (x ∷ []) ⊨ₚ isOrdAt ⟩ → IsOrd x
isOrdAt-out x h =
( λ {x₁} {y} y∈x₁ x₁∈x → h .fst x₁ x₁∈x y y∈x₁ )
, ( λ a a∈x {x₁} {y} y∈x₁ x₁∈a → h .snd a a∈x x₁ x₁∈a y y∈x₁ )
逆に、IsOrd の二つの成分から二つの有界な節が従う。三つの枠をもつ版は中央の自由な枠について同じ述語を表し、ほかの二つの自由な枠は論理式に現れない。
isOrdAt-in : (x : S) → IsOrd x → ⟨ (x ∷ []) ⊨ₚ isOrdAt ⟩
isOrdAt-in x o =
( λ a a∈x b hb → o .fst {a} {b} hb a∈x )
, ( λ a a∈x b b∈a c hc → o .snd a a∈x {b} {c} hc b∈a )
isOrd-at-p : Formula (⊥* {ℓ-suc ℓ}) 3
三つの枠をもつ論理式の最初の連言支は、引数の要素の要素が引数の要素であること、すなわち第二の枠で読まれる推移性を言う。
isOrd-at-p =
(∀̇∈ (var (suc zero))
(∀̇∈ (var zero) (var zero ∈̇ var (suc (suc (suc zero))))))
∧̇ (∀̇∈ (var (suc zero))
(∀̇∈ (var zero)
第二の連言支は、引数の各要素 a が推移的であること、すなわち c ∈ b ∈ a ならば c ∈ a であることを述べる。
(∀̇∈ (var zero) (var zero ∈̇ var (suc (suc zero))))))
その有界性の証拠は、同じ再帰に従う。続いて消去の補題が始まる。定数の出現をもたない論理式に対して、定数を消去しても Δ₀ の証拠は、場合ごとに保たれる。
Δ₀-isOrd-at-p : Δ₀ isOrd-at-p
Δ₀-isOrd-at-p = δ-∧ (δ-∀∈ (δ-∀∈ δ-∈)) (δ-∀∈ (δ-∀∈ (δ-∀∈ δ-∈)))
erase-Δ₀ : {m : ℕ} (φ : Formula CS.S m) (p : countFo φ ≡ 0)
→ Δ₀ φ → Δ₀ (Cnt.erase φ p)
erase-Δ₀ (t ∈̇ u) p δ-∈ = δ-∈
アトムはそのまま通り、命題の結合子は構造的に消去が施されるので再帰する。
erase-Δ₀ (t ≐ u) p δ-≐ = δ-≐
erase-Δ₀ (φ ∧̇ ψ) p (δ-∧ c d) = δ-∧ (erase-Δ₀ φ _ c) (erase-Δ₀ ψ _ d)
erase-Δ₀ (φ ∨̇ ψ) p (δ-∨ c d) = δ-∨ (erase-Δ₀ φ _ c) (erase-Δ₀ ψ _ d)
erase-Δ₀ (φ ⇒̇ ψ) p (δ-⇒ c d) = δ-⇒ (erase-Δ₀ φ _ c) (erase-Δ₀ ψ _ d)
erase-Δ₀ ⊥̇ p δ-⊥ = δ-⊥
有界量化子の場合は本体について再帰する。
erase-Δ₀ (∀̇∈ t φ) p (δ-∀∈ c) = δ-∀∈ (erase-Δ₀ φ _ c)
erase-Δ₀ (∃̇∈ t φ) p (δ-∃∈ c) = δ-∃∈ (erase-Δ₀ φ _ c)
erase-Δ₀ (∃̇ φ) p ()
erase-Δ₀ (∀̇ φ) p ()
凝縮に必要な包のデータ
非有界量化子の場合は、それに対応する Δ₀ の構成子が存在しないため不可能である。
module HullStage (lam : S) (ordλ : IsOrd lam)
(succλ : (d : S) → ⟨ d ∈ˢ lam ⟩ → ⟨ sucV d ∈ˢ lam ⟩)
(X : S) (X⊆L : (x : S) → ⟨ x ∈ˢ X ⟩ → ⟨ x ∈ˢ Lset lam ⟩) (∅∈λ : ⟨ ∅ ∈ˢ lam ⟩) where
枠組みは、指数が要素の後続を認める段階、その段階に含まれる始集合、そして空集合の指数への所属を受け取る。
Lset lam の内部で、始集合は Skolem 包 M を生成する。M の各要素は段階内にとどまる。
module ASt = AtStage lam ordλ
using ( module AbsL; module AtM; module Hull; Ltr; SL; wL )
もとの集合と予備値である空集合は、いずれも包の構成の中に表示される。
module H = ASt.Hull X X⊆L ∅∈λ
using ( module T; module XInM; Hull⊆L; X⊆M; hull-member
; val-in-Hull; ∅∈Lsetα; inStg )
この集合 M は凝縮の議論の台であり、その初等性と Mostowski 崩壊が議論のデータになる。
M : S
M = H.T.Hull
包 M に対し、その Mostowski 崩壊を π、崩壊像を πX とする。包の点を崩壊したものはすべて πX に属し、πX の各要素は包の点から得られ、πX は推移的である。さらに、包の推移的な点は崩壊によって固定される。
module C = Collapse M
using ( module InjExt; π; πX; πX-intro; πX-member; πX-trans; fixes )
凝縮の議論では、崩壊像について二つの性質を仮定する。第一に、順序数 δ が像に属するなら、段階 Lset δ も像に属する。第二に、包の各要素の崩壊は、像に属する順序数を添字とするある段階に属する。この閉性と被覆の性質により、崩壊像を L の一つの段階と同定できる。
module Condense
(levelIn : (δ : S) → IsOrd δ → ⟨ δ ∈ˢ C.πX ⟩ → ⟨ Lset δ ∈ˢ C.πX ⟩)
(cover : (y : S) → ⟨ y ∈ˢ M ⟩
→ ∥ Σ[ γ ∶ S ] (IsOrd γ × ⟨ γ ∈ˢ C.πX ⟩ × ⟨ C.π y ∈ˢ Lset γ ⟩) ∥₁)
where
分出によって、πX の要素のうち順序数であるものちょうどからなる集合を作る。したがって β は崩壊像の順序数部分を表す。分出の述語は順序数性を述べる有界の論理式であり、Δ₀ の証拠によってどの環境でも小さいものである。
β-sep : Σ[ s ∶ S ]
(∀ y → (y ∈ˢ s) ≡ ((y ∈ˢ C.πX) ⊓ ((y ∷ []) ⊨ₚ isOrdAt)))
β-sep = separateFromSmall C.πX (λ y → (y ∷ []) ⊨ₚ isOrdAt)
(λ y → D0.Δ₀-small Δ₀-isOrdAt (y ∷ []))
この順序数部分を β と書く。以下では、β 自身が順序数であり、β が添字づける階層が崩壊像と一致することを示す。
β : S
β = β-sep .fst
β に属することは、πX に属し、さらにその要素を自由変数に割り当てたとき無定数の順序数公式を満たすことと同値である。
β-spec : (y : S) → (y ∈ˢ β) ≡ ((y ∈ˢ C.πX) ⊓ ((y ∷ []) ⊨ₚ isOrdAt))
β-spec = β-sep .snd
同値の第一の射影は、ベータのすべての要素が崩壊の像の要素であることを示す。
β∈πX : (δ : S) → ⟨ δ ∈ˢ β ⟩ → ⟨ δ ∈ˢ C.πX ⟩
β∈πX δ δ∈β = subst ⟨_⟩ (β-spec δ) δ∈β .fst
第二成分は、この無定数一自由変数公式の充足を、周囲の宇宙での順序数性へ変換する。
β-ord : (δ : S) → ⟨ δ ∈ˢ β ⟩ → IsOrd δ
β-ord δ δ∈β = Amb.isOrdAt-out δ (subst ⟨_⟩ (β-spec δ) δ∈β .snd)
逆に、崩壊の像の順序数はベータの中にある。所属と順序数性という定義の二つの成分が供給され、定義の同値がそれをベータの内部へ運び戻す。
ord∈β : (δ : S) → ⟨ δ ∈ˢ C.πX ⟩ → IsOrd δ → ⟨ δ ∈ˢ β ⟩
ord∈β δ δ∈πX oδ = subst ⟨_⟩ (sym (β-spec δ)) (δ∈πX , Amb.isOrdAt-in δ oδ)
β が順序数であることを示すため、その二つの定義条件を確かめる。第一は推移性である。z ∈ x ∈ β ならば z ∈ β でなければならない。
β-isOrd : IsOrd β
β-isOrd = β-trans , β-mem
where
β-trans : isTransV β
β-trans {x = x} {y = z} z∈x x∈β =
推移性は、中間の所属のもとで崩壊の像の推移性を使い、中間の点の順序数性を周囲の論理式から読む。第二の欄は、ベータのすべての要素が順序数、したがって推移的であることから従う。
subst ⟨_⟩ (sym (β-spec z))
( C.πX-trans {x = x} {y = z} z∈x (β∈πX x x∈β)
, Amb.isOrdAt-in z (mem-ord {A = x} (β-ord x x∈β) z z∈x) )
β-mem : (x : S) → ⟨ x ∈ˢ β ⟩ → isTransV x
β-mem x x∈β = β-ord x x∈β .fst
覆いの仮定は、包の要素から崩壊の要素へ一度持ち上がる。崩壊の要素は、単に、包のある要素の崩壊なので、その要素の覆いが同一視に沿って運ばれる。
covered : (x : S) → ⟨ x ∈ˢ C.πX ⟩
→ ∥ Σ[ γ ∶ S ]
(IsOrd γ × ⟨ γ ∈ˢ C.πX ⟩ × ⟨ x ∈ˢ Lset γ ⟩) ∥₁
covered x x∈πX = rec₁ squash₁ go (C.πX-member x x∈πX)
where
逆にたどるのは、崩壊自身の要素の記述である。像の要素は、単に、包のある要素の崩壊である。
go : Σ[ y ∶ S ] (⟨ y ∈ˢ M ⟩ × (C.π y ≡ x))
→ ∥ Σ[ γ ∶ S ]
(IsOrd γ × ⟨ γ ∈ˢ C.πX ⟩ × ⟨ x ∈ˢ Lset γ ⟩) ∥₁
go (y , y∈M , e) = map₁
(λ { (γ , oγ , γ∈πX , h) →
覆いは、崩壊の値の等しさに沿って運ばれる。持ち上がった主張はすぐに使われる。ベータのすべての順序数は、ベータの中のより大きな順序数の中にある。これが凝縮の議論の古典的な極限段階の一歩である。
γ , oγ , γ∈πX , subst (λ w → ⟨ w ∈ˢ Lset γ ⟩) e h })
(cover y y∈M)
β-succ : (δ : S) → ⟨ δ ∈ˢ β ⟩
→ ∥ Σ[ γ ∶ S ] (IsOrd γ × ⟨ δ ∈ˢ γ ⟩ × ⟨ γ ∈ˢ β ⟩) ∥₁
β-succ δ δ∈β = map₁ go (covered δ (β∈πX δ δ∈β))
delta の順序数性はベータから読まれ、変換は覆いの結論を所属の形で言い直す。delta を含む層は、その指数をベータの中に選べるのである。
where
oδ : IsOrd δ
oδ = β-ord δ δ∈β
go : Σ[ γ ∶ S ] (IsOrd γ × ⟨ γ ∈ˢ C.πX ⟩ × ⟨ δ ∈ˢ Lset γ ⟩)
→ Σ[ γ ∶ S ] (IsOrd γ × ⟨ δ ∈ˢ γ ⟩ × ⟨ γ ∈ˢ β ⟩)
δ と γ はともに順序数なので、δ ∈ Lset γ から δ ∈ γ が従う。また γ は πX に属する順序数なので、γ ∈ β である。そして逆の包含が述べられる。崩壊のすべての要素は、ベータにおける層に属する。
go (γ , oγ , γ∈πX , δ∈Lγ) =
γ , oγ , ord∈Lset→∈ γ oγ δ oδ δ∈Lγ , ord∈β γ γ∈πX oγ
πX⊆Lβ : (x : S) → ⟨ x ∈ˢ C.πX ⟩ → ⟨ x ∈ˢ Lset β ⟩
πX⊆Lβ x x∈πX = rec₁ ((x ∈ˢ Lset β) .snd) go (covered x x∈πX)
where
逆の包含が成り立つのは、ベータにおける層がすべてのより小さい層を含むからである。段階の構成の単調性が、覆いの層をベータの中へ運ぶ。
go : Σ[ γ ∶ S ] (IsOrd γ × ⟨ γ ∈ˢ C.πX ⟩ × ⟨ x ∈ˢ Lset γ ⟩)
→ ⟨ x ∈ˢ Lset β ⟩
go (γ , oγ , γ∈πX , x∈Lγ) =
Lset-mono {α = β} {β = γ} (ord∈β γ γ∈πX oγ) x∈Lγ
Lβ⊆πX : (x : S) → ⟨ x ∈ˢ Lset β ⟩ → ⟨ x ∈ˢ C.πX ⟩
順方向の包含は、ベータの層の要素を段階の構成で分解し、極限の一歩がベータの中のより大きな順序数を供給する。
Lβ⊆πX x x∈Lβ = rec₁ ((x ∈ˢ C.πX) .snd) go (Lset-out β x x∈Lβ)
where
go : Σ[ δ ∶ S ] (⟨ δ ∈ˢ β ⟩ × ⟨ x ∈ˢ 𝒟ₒ (Lset δ) ⟩)
→ ⟨ x ∈ˢ C.πX ⟩
go (δ , δ∈β , x∈𝒟ₒδ) = rec₁ ((x ∈ˢ C.πX) .snd) liftStage (β-succ δ δ∈β)
持ち上げの段階が述べられる。ベータの中で delta を含む順序数から、崩壊の中での x の所属を産み出す。
where
liftStage : Σ[ γ ∶ S ] (IsOrd γ × ⟨ δ ∈ˢ γ ⟩ × ⟨ γ ∈ˢ β ⟩)
→ ⟨ x ∈ˢ C.πX ⟩
liftStage (γ , oγ , δ∈γ , γ∈β) =
C.πX-trans {x = Lset γ} {y = x}
持ち上げは、二つの閉包を合成する。x は gamma より下の delta で定義されるので gamma の層に属し、さらに第一の仮定によって、崩壊の像は gamma における層を含む。二つの包含は、宇宙の外延性のもとで出会う。
(Lset-in γ δ x δ∈γ x∈𝒟ₒδ)
(levelIn γ oγ (β∈πX γ γ∈β))
ext : C.πX ≡ Lset β
ext = extensionality C.πX (Lset β) (sub , sup)
where
外延性の議論の前半は、各要素を橋を通して段階の読みへ運び、逆の包含を適用し、橋を通って戻す。
sub : (x : S) → ⟨ x ∈ₛ C.πX ⟩ → ⟨ x ∈ₛ Lset β ⟩
sub x x∈ₛπX = ∈∈ₛ {a = x} {b = Lset β} .fst
(πX⊆Lβ x (∈∈ₛ {a = x} {b = C.πX} .snd x∈ₛπX))
sup : (x : S) → ⟨ x ∈ₛ Lset β ⟩ → ⟨ x ∈ₛ C.πX ⟩
sup x x∈ₛLβ = ∈∈ₛ {a = x} {b = C.πX} .fst
後半は順方向の包含について同じことを行い、二つの半分が、崩壊の像をベータにおける層と同一視する。
(Lβ⊆πX x (∈∈ₛ {a = x} {b = Lset β} .snd x∈ₛLβ))
これで凝縮の主張が得られる。崩壊像は順序数 β を添字とする段階に等しくなる。応用では、段階 Lset α と一つの点 x の合併を始集合とし、α ∈ lam、x ⊆ Lset α、x ∈ Lset lam を仮定する。
condenses : Σ[ γ ∶ S ] (IsOrd γ × (C.πX ≡ Lset γ))
condenses = β , β-isOrd , ext
module UnionKit (α lam x : S) (ordα : IsOrd α) (ordλ : IsOrd lam)
(α∈λ : ⟨ α ∈ˢ lam ⟩) (x⊆Lα : (z : S) → ⟨ z ∈ˢ x ⟩ → ⟨ z ∈ˢ Lset α ⟩)
(x∈Lλ : ⟨ x ∈ˢ Lset lam ⟩) (α∉ω : ⟨ α ∈ˢ ω ⟩ → ⊥₀) where
始集合は Lset α と単集合 {x} の合併である。単集合の特徴づけから x ∈ {x} が得られる。
X : S
X = Lset α ∪ ⁅ x ⁆s
x∈sgl : ⟨ x ∈ₛ ⁅ x ⁆s ⟩
x∈sgl = SetPackage.classification (SingletonPackage x) x .snd refl
余分な点は、和の右側を通して始集合に属する。
x∈X : ⟨ x ∈ˢ X ⟩
x∈X = cup-inr (Lset α) ⁅ x ⁆s x (∈∈ₛ {a = x} {b = ⁅ x ⁆s} .snd x∈sgl)
段階のすべての要素は、左側を通して始集合に属する。
Lα∈X : (z : S) → ⟨ z ∈ˢ Lset α ⟩ → ⟨ z ∈ˢ X ⟩
Lα∈X = cup-inl (Lset α) ⁅ x ⁆s
単集合の特徴づけにより、{x} の各要素は x に等しくなる。
sgl≡ : (z : S) → ⟨ z ∈ˢ ⁅ x ⁆s ⟩ → z ≡ x
sgl≡ = sgl-out x
したがって、始集合への所属は二つの場合に分かれる。その点は Lset α に属するか、単集合 {x} に属する。
X-mem : (z : S) → ⟨ z ∈ˢ X ⟩
→ ⟨ (z ∈ˢ Lset α) ⊔ (z ∈ˢ ⁅ x ⁆s) ⟩
X-mem = cup-out (Lset α) ⁅ x ⁆s
生成集は周囲の段階に含まれる。段階の側の要素は、指数の包含に沿って、段階の構成の単調性によって運ばれる。
X⊆Lλ : (z : S) → ⟨ z ∈ˢ X ⟩ → ⟨ z ∈ˢ Lset lam ⟩
X⊆Lλ z z∈X = rec₁ ((z ∈ˢ Lset lam) .snd) go (X-mem z z∈X)
where
go : (⟨ z ∈ˢ Lset α ⟩ ⊎ ⟨ z ∈ˢ ⁅ x ⁆s ⟩) → ⟨ z ∈ˢ Lset lam ⟩
go (inl z∈Lα) = Lset-mono {α = lam} {β = α} α∈λ z∈Lα
単元の側の要素は余分な点に帰着し、その段階への所属は仮定であった。
go (inr z∈sgl) = subst (λ u → ⟨ u ∈ˢ Lset lam ⟩) (sym (sgl≡ z z∈sgl)) x∈Lλ
生成集は推移的である。段階の側の要素の要素は、層の推移性によって段階の中にあり、左の包含がそれを生成集の中に置く。
Xtr : isTransV X
Xtr {x = a} {y = b} b∈a a∈X = rec₁ ((b ∈ˢ X) .snd) go (X-mem a a∈X)
where
go : (⟨ a ∈ˢ Lset α ⟩ ⊎ ⟨ a ∈ˢ ⁅ x ⁆s ⟩) → ⟨ b ∈ˢ X ⟩
go (inl a∈Lα) = Lα∈X b (layer-trans (Lset-layer α) b∈a a∈Lα)
単集合側では中間の集合は x である。仮定 x ⊆ Lset α により、その各要素は合併の左側に入る。
go (inr a∈sgl) = Lα∈X b (x⊆Lα b
(subst (λ u → ⟨ b ∈ˢ u ⟩) (sgl≡ a a∈sgl) b∈a))
one∈α : ⟨ sucV ∅ ∈ˢ α ⟩
one∈α = ⊎-rec
(λ α∈ω → ⊥₀-rec (α∉ω α∈ω))
無限とは ω に属さないことであり、順序数の三分法が場合を分ける。ω に属するなら仮定と矛盾し、ω と等しいなら数項一が所属の証人となり、ω が α より下なら α の推移性によって数項一がその中に入る。
(⊎-rec (λ α≡ω → subst (λ w → ⟨ sucV ∅ ∈ˢ w ⟩) (sym α≡ω) (#∈ω 1))
(λ ω∈α → ordα .fst (#∈ω 1) ω∈α))
(ord-tri α ordα ω ω-ord)
空集合は最初の後続の段階に現れる。基底の層の符号化が、後続の段階の記述に沿って運ばれるからである。
∅∈Lset1 : ⟨ ∅ ∈ˢ Lset (sucV ∅) ⟩
∅∈Lset1 = subst (λ w → ⟨ ∅ ∈ˢ w ⟩) (sym (Lset-suc ∅)) (∅∈𝒟ₒ ∅)
単調性が、空集合をまず Lset α へ、さらに Lset lam へ持ち上げる。
∅∈Lλ : ⟨ ∅ ∈ˢ Lset lam ⟩
∅∈Lλ = Lset-mono {α = lam} {β = α} α∈λ
(Lset-mono {α = α} {β = sucV ∅} one∈α ∅∈Lset1)
ランクによる特徴づけにより、空集合が指数 lam 自身に属することが従う。残るのは包の外延性であり、これはその崩壊を単射にするために必要な最後の条件である。
∅∈λ : ⟨ ∅ ∈ˢ lam ⟩
∅∈λ = subst (λ w → ⟨ w ∈ˢ lam ⟩) (rank-fix ∅ ∅-ord)
(rank-Lset lam ordλ ∅ ∅∈Lλ)
module HullExt (α : S) (ordα : IsOrd α)
(X : S) (X⊆L : (x : S) → ⟨ x ∈ˢ X ⟩ → ⟨ x ∈ˢ Lset α ⟩)
(∅∈α : ⟨ ∅ ∈ˢ α ⟩) where
空集合が指数に属するという仮定により、Lset α における Skolem 包は、その項代数に必要な既定値をもつ。
M を、Lset α の内部で X から生成される Skolem 包とする。段階への包含は初等的である。M に制限した所属関係の外延性を示すため、包の中の論理式と段階での解釈を比較する。
module ASt = AtStage α ordα using ( module AbsL; module AtM; module Hull; SL )
module H = ASt.Hull X X⊆L ∅∈α using ( module T; Hull⊆L )
module A = ASt.AtM H.T.Hull H.Hull⊆L using ( SM; inL; module SemM )
module E = HullElemDown α ordα X X⊆L ∅∈α using ( elem )
module Mse = A.SemM.At A.SM id using ( _⊨_ )
包が名付けられ、二つの集合の対称差が所属の真値の水準で述べられる。ある点が一方に属し、他方には属さないと証明できる、という形である。
M : S
M = H.T.Hull
Different : S → S → S → Type (ℓ-suc ℓ)
Different x y z = (z ∈ᵗ x × (z ∈ᵗ y → ⊥₀))
⊎ (z ∈ᵗ y × (z ∈ᵗ x → ⊥₀))
古典的に、等しくない集合は対称差の中に点をもつ。切り詰められた存在は、排中律によって判定される。
different : (x y : S) → (x ≡ y → ⊥₀) → ∥ Σ[ z ∶ S ] Different x y z ∥₁
different x y nxy = go (lem P)
where
P : hProp (ℓ-suc ℓ)
P = ∥ Σ[ z ∶ S ] Different x y z ∥₁ , squash₁
もし二つの集合を区別する点がなければ、すべての所属命題が両方向で一致し、宇宙の外延性によって両者は等しくなり、仮定に矛盾する。
go : Dec ⟨ P ⟩ → ⟨ P ⟩
go (yes p) = p
go (no np) = ⊥₀-rec (nxy (extensionalV (λ z → ⇔toPath (fwd z) (bwd z))))
where
fwd : (z : S) → z ∈ᵗ x → z ∈ᵗ y
一致の両方向は排中律で判定され、失敗した方向はそれぞれの点を対称差に加える。
fwd z zx = decRec (λ zy → zy)
(λ nzy → ⊥₀-rec (np ∣ z , inl (zx , nzy) ∣₁))
(FOL.Semantics.decideMembership 𝒮ᵥ lem z y)
bwd : (z : S) → z ∈ᵗ y → z ∈ᵗ x
bwd z zy = decRec (λ zx → zx)
(λ nzx → ⊥₀-rec (np ∣ z , inr (zy , nzx) ∣₁))
(FOL.Semantics.decideMembership 𝒮ᵥ lem z x)
差の公式は選言 (z ∈ x ∧ z ∉ y) ∨ (z ∈ y ∧ z ∉ x) であり、二つの定数欄に二つの包の要素を入れる。
φ : A.SM → A.SM → Formula A.SM 1
φ x y = ((var zero ∈̇ con x) ∧̇ (¬̇ (var zero ∈̇ con y)))
∨̇ ((var zero ∈̇ con y) ∧̇ (¬̇ (var zero ∈̇ con x)))
outer : (u v : S) (u∈M : u ∈ᵗ M) (v∈M : v ∈ᵗ M)
→ (z : S) → Different u v z
存在論理式の充足は切り詰められているので、区別する点も切り詰めの中で返す。対称差のどちらの分岐でも、同じ点が段階における論理式の対応する選言肢を証明する。
→ ∥ Σ[ a ∶ ASt.SL ]
⟨ (a ∷ []) ASt.AbsL.⊨ᵐ (mapFo A.inL (φ (u , u∈M) (v , v∈M))) ⟩ ∥₁
outer u v u∈M v∈M z d = ∣ a , ∣ objectDifferent d ∣₁ ∣₁
where
objectDifferent = sumMap
どちらの分岐でも、周囲での所属が肯定側の連言項を与え、不所属の証明を公式意味論が要求する否定へ持ち上げる。段階の推移性により、区別する点もその台に入る。
(λ (zu , nzv) → zu , λ zv → lift (nzv zv))
(λ (zv , nzu) → zv , λ zu → lift (nzu zu))
z∈L : ⟨ z ∈ˢ Lset α ⟩
z∈L = ⊎-rec
(λ (zx , _) → layer-trans (Lset-layer α) zx (H.Hull⊆L u u∈M))
区別する点をその段階への所属と組にすると、段階の台における証人が得られる。包の外延性を示すため、まず包の各要素について、x に属するなら y にも属すると仮定する。
(λ (zv , _) → layer-trans (Lset-layer α) zv (H.Hull⊆L v v∈M)) d
a : ASt.SL
a = z , z∈L
refute : (x y : S) (x∈M : x ∈ᵗ M) (y∈M : y ∈ᵗ M)
→ (ag1 : (z : S) → z ∈ᵗ M → ⟨ z ∈ˢ x ⟩ → ⟨ z ∈ˢ y ⟩)
逆に、包の各要素について、y に属するなら x にも属すると仮定する。それでも x と y が等しくないなら、対称差の点から矛盾が導かれる。
→ (ag2 : (z : S) → z ∈ᵗ M → ⟨ z ∈ˢ y ⟩ → ⟨ z ∈ˢ x ⟩)
→ (x ≡ y → ⊥₀) → ⊥₀
refute x y x∈M y∈M ag1 ag2 nxy = rec₁ isProp⊥ diff (different x y nxy)
where
xS : A.SM
二つの包の要素は、部分構造の台の要素として読まれ、差の論理式に代入する準備ができる。
xS = x , x∈M
yS : A.SM
yS = y , y∈M
反証は、差の点を消去する。初等性が、差の点を証人とする存在の論理式の段階での充足を、包の中での同じ存在の充足へ変える。
diff : Σ[ z ∶ S ] Different x y z → ⊥₀
diff (z , d) = rec₁ isProp⊥ inside h
where
h : ⟨ [] Mse.⊨ (∃̇ (φ xS yS)) ⟩
h = subst ⟨_⟩ (sym (E.elem 0 (∃̇ (φ xS yS)) []))
初等性により、差の論理式を満たす包の中の証人が得られる。その切り詰められた選言を消去すると、二つの非対称な所属命題のどちらが成り立つかが得られる。
(outer x y x∈M y∈M z d)
inside : Σ[ b ∶ A.SM ] ⟨ (b ∷ []) Mse.⊨ φ xS yS ⟩ → ⊥₀
inside (b , q) = rec₁ isProp⊥ cases q
where
cases : (⟨ b .fst ∈ˢ x ⟩ × (⟨ b .fst ∈ˢ y ⟩ → Lift ⊥₀))
どちらの選言の枝でも、証人は一方の包の要素ではあって他方ではないとされ、対応する一致の仮定がその否定と矛盾する。この矛盾こそ、包の外延性が求めるものである。
⊎ (⟨ b .fst ∈ˢ y ⟩ × (⟨ b .fst ∈ˢ x ⟩ → Lift ⊥₀))
→ ⊥₀
cases (inl (bx , nby)) = lower (nby (ag1 (b .fst) (b .snd) bx))
cases (inr (by , nbx)) = lower (nbx (ag2 (b .fst) (b .snd) by))
包の外延性は古典的な背理法で証明する。集合の宇宙は h-集合なので x ≡ y は命題であり、排中律から等しい場合と等しくない場合に分かれる。x ≢ y なら、refute は包の中に x と y の一方だけに属する要素を与え、二つの所属一致の仮定に矛盾する。したがって x ≡ y である。
hullExt : isExt M
hullExt x y x∈M y∈M ag1 ag2 =
decRec (λ p → p) (λ np → ⊥₀-rec (bad np))
(FOL.Semantics.decideEquality 𝒮ᵥ lem x y)
where
bad が矛盾する分岐を除き、包の外延性が完成する。
bad : (x ≡ y → ⊥₀) → ⊥₀
bad = refute x y x∈M y∈M ag1 ag2
崩壊を通して有界論理式を移す
崩壊と周囲の宇宙を比較するため、ここで推移的集合 U を固定する。定数を含まない Δ₀ 論理式を U の要素で評価すると、U 上の制限構造と周囲の構造で同じ真理値をもつ。
module Unpack (U : S) (Utr : isTrans U) where
制限された台 SM の要素は、集合とそれが U に属する証拠との組である。各組を第一成分へ射影すると対応する周囲の環境が得られ、有界絶対性 abs₀ が射影の前後の充足を比較する。
module Ab = FOL.Absoluteness.Single 𝒮ᵥ (λ x → x ∈ˢ U) Utr using (SM; abs₀; _⊨ᵐ_)
定数を含まない Δ₀ 論理式 φ について、read はまず embed φ を制限された台の上の論理式として扱う。有界絶対性が制限された読みと周囲の読みを比較し、embed-⊨ が埋め込みに伴う改名を除き、空の定数領域からの関数の一意性が残る定数解釈を同定する。
read : {n : ℕ} {φ : Formula (⊥* {ℓ-suc ℓ}) n} → Δ₀ φ → (δ : Vec Ab.SM n)
→ (δ Ab.⊨ᵐ embed φ) ≡ (map (λ p → p .fst) δ ⊨ₚ φ)
read {n} {φ} dφ δ =
Ab.abs₀ (mapΔ₀ ⊥*-rec dφ) δ
∙ embed-⊨ 𝒮ᵥ {K = Ab.SM} (λ p → p .fst) φ (map (λ p → p .fst) δ)
最後のパスでは関数外延性を使う。定数領域が空なので、二つの定数解釈は各点で一致し、したがって等しい。次に Lset lam の内部で包を作るため、後続に閉じた順序数 lam と始集合 X ⊆ Lset lam を固定する。
∙ cong (λ ι → let module I = SemV.At (⊥* {ℓ-suc ℓ}) ι in map (λ p → p .fst) δ I.⊨ φ)
(funExt (λ b → ⊥*-rec b))
module Frame (lam : S) (ordλ : IsOrd lam)
(succλ : (d : S) → ⟨ d ∈ˢ lam ⟩ → ⟨ sucV d ∈ˢ lam ⟩)
(X : S) (X⊆Lλ : (z : S) → ⟨ z ∈ˢ X ⟩ → ⟨ z ∈ˢ Lset lam ⟩)
(∅∈λ : ⟨ ∅ ∈ˢ lam ⟩) where
さらに ∅ ∈ lam を仮定する。これは包の構成が用いる基底段階の仮定である。
M を Lset lam の内部で X から生成される包とする。以下では、段階への包含、それに対する初等性、そして上で証明した外延性を用いる。
module HS = HullStage lam ordλ succλ X X⊆Lλ ∅∈λ using (module ASt; module C; module Condense; module H; M)
module ASt = HS.ASt using (module AbsL; module AtM; Ltr; SL)
module A = ASt.AtM HS.M HS.H.Hull⊆L using (Elementary; SM; module SemM; inL)
module HE = HullExt lam ordλ X X⊆Lλ ∅∈λ using (hullExt)
したがって M は外延的である。これは M をその推移的な Mostowski 崩壊と同一視するために必要な仮定である。
Mext : isExt HS.M
Mext = HE.hullExt
移送の議論は、包含 M → Lset lam の初等性を明示的に受け取る。これと M の外延性から、以下で使う二つの比較、すなわち包から段階への比較と、包からその崩壊への比較が得られる。
module Carry (elem : A.Elementary) where
ここでは三つの構造、包 M、段階 Lset lam、推移的な崩壊像 πX を比較する。崩壊同型が第一と第三を結び、有界絶対性が二つの推移的集合をそれぞれ周囲の宇宙に結びつける。
module CIso = CollapseIso HS.M Mext using (module I; iso-fwd; iso-bwd)
module TL = Unpack (Lset lam) ASt.Ltr using (read)
module Tπ = Unpack HS.C.πX HS.C.πX-trans using (module Ab; read)
所属は崩壊によって直接保存される。所属の同型の順方向が、原子的な所属に必要な押し出しにちょうど当たる。
member-push : (x y : S) → ⟨ x ∈ˢ HS.M ⟩ → ⟨ y ∈ˢ HS.M ⟩
→ ⟨ y ∈ˢ x ⟩ → ⟨ HS.C.π y ∈ˢ HS.C.π x ⟩
member-push = CIso.iso-fwd
Lset lam は推移的なので、定数を含まない各 Δ₀ 論理式はそこで制限された読みと周囲の読みが一致する。atL はこの段階における read である。
atL : {n : ℕ} {φ : Formula (⊥* {ℓ-suc ℓ}) n} → Δ₀ φ → (δ : Vec ASt.SL n)
→ (δ ASt.AbsL.⊨ᵐ embed φ) ≡ (map (λ p → p .fst) δ ⊨ₚ φ)
atL dφ δ = TL.read dφ δ
崩壊像 πX も推移的なので、定数を含まない Δ₀ 論理式について同じ内外の一致が成り立つ。
atπ : {n : ℕ} {φ : Formula (⊥* {ℓ-suc ℓ}) n} → Δ₀ φ → (δ : Vec Tπ.Ab.SM n)
→ (δ Tπ.Ab.⊨ᵐ embed φ) ≡ (map (λ p → p .fst) δ ⊨ₚ φ)
atπ dφ δ = Tπ.read dφ δ
包自身の台のもとの読みは、初等性を通って分解される。埋め込まれた論理式はまず内部で読まれ、その論理式が定数を運ばないため改名は固定され、結果は段階の読みへ運ばれる。
atM : {n : ℕ} {φ : Formula (⊥* {ℓ-suc ℓ}) n} → Δ₀ φ → (δ : Vec A.SM n)
→ (δ CIso.I.⊨ᵐ embed φ) ≡ (map (λ p → p .fst) δ ⊨ₚ φ)
atM {n} {φ} dφ δ =
elem n (embed φ) δ
∙ cong (λ ψ → map A.inL δ ASt.AbsL.⊨ᵐ ψ) (embed-map A.inL φ)
段階での絶対性の後に残るのは環境の比較だけである。包の要素を Lset lam に含めても基礎にある集合は変わらないので、包含してから射影した周囲の集合のベクトルは、元の環境を直接射影したものに等しい。
∙ atL dφ (map A.inL δ)
∙ cong (λ γ → γ ⊨ₚ φ) (map-inL-fst δ)
where
map-inL-fst : {m : ℕ} (γ : Vec A.SM m)
→ map (λ p → p .fst) (map A.inL γ) ≡ map (λ p → p .fst) γ
この等式は空の環境では直ちに成り立ち、環境の先頭に一つの成分を加えても保たれる。したがって、定数を含まない Δ₀ 論理式について、包の要素からなる環境での周囲の真理は、それらの崩壊値からなる環境での周囲の真理を導く。
map-inL-fst [] = refl
map-inL-fst (q ∷ γ) = cong (q .fst ∷_) (map-inL-fst γ)
push : {n : ℕ} {φ : Formula (⊥* {ℓ-suc ℓ}) n} → Δ₀ φ → (δ : Vec A.SM n)
→ ⟨ map (λ p → p .fst) δ ⊨ₚ φ ⟩
→ ⟨ map (λ p → p .fst) (map CIso.I.g δ) ⊨ₚ φ ⟩
包の環境での周囲の真理から出発し、まず atM を逆向きに使って包の内部の真理を得る。iso-inv がそれを崩壊像へ移し、embed-map が空虚な定数の改名を除き、最後に atπ を順向きに使って崩壊値での周囲の真理へ戻す。
push {n} {φ} dφ δ h =
subst ⟨_⟩ (atπ dφ (map CIso.I.g δ))
(subst (λ ψ → ⟨ map CIso.I.g δ CIso.I.⊨ᵖᵐ ψ ⟩)
(embed-map CIso.I.g φ)
(CIso.I.iso-inv n (embed φ) δ (subst ⟨_⟩ (sym (atM dφ δ)) h)))
pull では、崩壊値での周囲の真理を atπ に沿って逆向きに崩壊像の内部へ移す。embed-map で改名された形を戻し、iso-inv-bwd で包の内部の真理へ戻った後、atM を順向きに使って元の包の環境での周囲の真理を回復する。
pull : {n : ℕ} {φ : Formula (⊥* {ℓ-suc ℓ}) n} → Δ₀ φ → (δ : Vec A.SM n)
→ ⟨ map (λ p → p .fst) (map CIso.I.g δ) ⊨ₚ φ ⟩
→ ⟨ map (λ p → p .fst) δ ⊨ₚ φ ⟩
pull {n} {φ} dφ δ h =
subst ⟨_⟩ (atM dφ δ)
push と pull を合わせると、定数を含まない任意の Δ₀ 論理式と、包の要素からなる任意の有限環境について、各成分をその崩壊値に置き換えても周囲での充足は変わらない。別の補題 member-push は、所属について対応する保存を直接与える。
(CIso.I.iso-inv-bwd n (embed φ) δ
(subst (λ ψ → ⟨ map CIso.I.g δ CIso.I.⊨ᵖᵐ ψ ⟩)
(sym (embed-map CIso.I.g φ))
(subst ⟨_⟩ (sym (atπ dφ (map CIso.I.g δ))) h)))