Skolem 包を構成して崩壊させる

本章は、構成可能段階の中の始集合の Skolem 包を作り、包が段階の中で初等的であることを示し、所属を保つ全単射によって推移的集合へ崩壊させ、充足関係と有界論理式が崩壊を越えてどう移るかを整理します。重要なのは、包そのものはコードで与えられた像にすぎず、推移性は Mostowski 崩壊の後に初めて得られる、という点です。

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

本章は古典論理に依拠し、仮定はここで入ります。包の構成は問いの充足可能性を判定し、外延性の証明は両方向で所属を判定し、初等性の移送は二重否定を除去します。これらの段階はどれも排中律を消費します。

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

モジュールは宇宙レベル ℓ を固定し、本書の常の形式に従って古典的な仮定を明示的に受け取ります。ℓ-suc ℓ での排中律が引数として渡され、大域的に仮定されることはなく、本章の各定理はどのレベルの実例を使うかを正確に記録します。

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

対象言語は本書の一階の言語です。論理式は項から等号と所属で作られ、命題の結合子、非有界と有界の量化子の下で閉じています。述語 Δ₀ は、すべての量化子が有界である論理式を選び出します。

open import FOL.ZFStructure using ( ZFStructure; module hPropStructure; _↾_ )
open import FOL.Syntax using
  ( Formula; Term; con; var; _∈̇_; _≐_; _∧̇_; _∨̇_; _⇒̇_; ¬̇_; ⊥̇
  ; ∃̇_; ∀̇_; ∀̇∈; ∃̇∈ )
open import FOL.LevyHierarchy using

述語 Δ₀ は論理式の構造に沿う帰納的な証拠です。その構成子は原子式・結合子・有界量化子を覆いますが、非有界量化子に対応する構成子はありません。この証拠が後の絶対性の議論を支え、countFo と constantsFo は定数の各出現を記録します。

  ( Δ₀; δ-∈; δ-≐; δ-∧; δ-∨; δ-⇒; δ-⊥; δ-∀∈; δ-∃∈ )
import FOL.Absoluteness
import FOL.Manipulation.ConstantOccurrences
import FOL.Semantics
open import FOL.Manipulation.ConstantOccurrences using ( countFo; constantsFo )

パラメータ抽象は定数の出現を追加の環境変数で置き換え、定数写像と定数改名は意味を保って定数アルファベットを変えます。renameTm は文脈写像に沿って変数の位置を改名し、これにより以下で suc による弱化が得られます。周囲の階層は外延性とともに開かれます。同じ要素をもつ集合は等しい、という性質です。

open import FOL.Manipulation.ParameterAbstraction using ( absFo; ⊨-abs )
open import FOL.Manipulation.ConstantMapping using ( mapFo; mapTm; mapFo-comp; embed )
open import FOL.Manipulation.Relabelling using ( embed-⊨; mapΔ₀; ⊨-map )
open import FOL.Manipulation.Renaming using ( renameTm )
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ; extensionalV )

提示は、埋め込みをもつ小さな型で集合の要素を索引づけ、その繊維が提示された要素を名指します。崩壊は任意の台 X から推移的な像を構成し、崩壊写像を X 上で単射にするために制限された所属関係の外延性を用います。Δ₀ の小ささは、有界に定義できるクラスを集合へ分離します。空集合は各定義可能性後続に属し、Lset-suc は後続添字の段階を直前の段階の定義可能冪集合と同一視します。

open import V.Presentation {ℓ} using ( member; fiber )
open import V.Collapse {ℓ} using ( module Collapse; isExt; isTrans )
open import V.Smallness {ℓ} using ( separateFromSmall; module Δ₀Small )
open import L.Axioms.Basic {ℓ} using ( ∅∈𝒟ₒ; Lset-suc )
open import L.Constructible {ℓ}

構成可能な段階 Lset α は推移的であり、その構成は指数について単調なので、より大きな指数はより大きな段階を与えます。包の議論で繰り返し使う順序数の事実は、順序数の要素が順序数であること、ω が順序数であること、数項が ω に属すること、空集合が順序数であることです。

  using ( 𝒮ʟ; isTransV; IsOrd; Lset; Lset-in; Lset-out; Lset-mono; 𝒟ₒ
        ; layer-trans; Lset-layer )
open import L.Ordinal {ℓ} using ( mem-ord; ω-ord; #∈ω; ∅-ord )
open import L.Ordinal.Stages {ℓ} lem using ( ord∈Lset→∈; rank-Lset )
open import L.Ordinal.Linear {ℓ} lem using ( ord-tri )

整列順序には最小要素の選択子が伴います。述語を満たす要素の存在の切り詰められた主張から、述語を満たし整列順序で最小の要素を返します。段階の所属のランクによる特徴づけと、段階の台に制限した段階の順序がこの選択子に入力を供給し、和と単元を符号化する仕組みが、後で使う有限の始集合を作ります。

open import L.Rank {ℓ} using ( rank-fix )
open import L.WellOrder.Base {ℓ-suc ℓ} using ( SWO; leastOf )
open import L.Choice.StageOrders {ℓ} lem using ( orderAt )
open import L.Coding.CodeConstructibility {ℓ} using ( cup-out; cup-inl; cup-inr; sgl-out )

本章の環境は台の要素のベクトルであり、その演算は成分ごとに行われます。関数を環境へ写すこと、索引で参照すること、要素を一つ加えて延ばすこと、そして連結です。第二成分が命題である対は、要素を、決して区別しない証拠とともに記録します。

open import Cubical.Data.Nat using ( _+_ )
open import Cubical.Data.Vec using ( Vec; map; lookup; _∷_; []; _++_ )
open import Cubical.Data.Sigma using ( Σ≡Prop; _×_; _,_ )
open import Cubical.Data.Sum using ( _⊎_; inl; inr )
import Cubical.Data.Sum as Sum

空型は矛盾を表します。Empty.rec はその要素から任意の目標へ消去し、isProp⊥ は目標が矛盾であるとき命題的切り詰めの消去を可能にします。存在論理式の充足と提示された集合への所属は命題的切り詰めで表され、証人を選ばずに存在だけを保持します。

import Cubical.Data.Empty as Empty
open import Cubical.Data.Empty.Properties using ( isProp⊥ )
open import Cubical.Functions.Logic using ( ⇔toPath )
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∥_∥₁; ∣_∣₁; squash₁ )

累積階層は添字型と評価で集合を提示します。包では有限木型 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 hPropStructure 𝒮ᵥ

SemV は、以下で充足関係を具体化するときに使う固定長の周囲環境を与えます。定数が 𝒮ʟ を動く論理式では、出現回数によって定数を含まない場合を識別できます。そのとき erase は、充足を変えずに定数領域を空の型へ置き換えます。

module SemV = FOL.Semantics 𝒮ᵥ using ( _^_; module At )
open SemV using ( _^_ )
module CS = hPropStructure 𝒮ʟ using ( S )
module Cnt = FOL.Manipulation.ConstantOccurrences.ZeroOccurrences CS.S using ( erase; erase-inv )

空の定数領域では、Δ₀-small は各有界論理式の各環境での真理値が一段低い宇宙の命題と同値であることを示します。分出にはさらに separateFromSmall を適用する必要があります。そして項代数が始まります。構造、その台を周囲の宇宙へ写す写像、そして台の上の整列順序を引数とするのです。

module D0 = Δ₀Small {ℓc = ℓ-suc ℓ} {K = ⊥* {ℓ-suc ℓ}} (λ b → Empty.rec* b)
  using ( Δ₀-small )
module TermAlgebra (𝒮 : ZFStructure (ℓ-suc ℓ))
                   (toSet : ZFStructure.S 𝒮 → V ℓ)
                   (wo : SWO (ZFStructure.S 𝒮))

残りの引数は、既定の要素 junk と、K で索引づけられた基底の生成元の族です。K を始集合の提示と同一視するのは、後の包の実例です。既定の値は簿記のためのもので、後の構成がそれを調べることはありません。

                   (junk : ZFStructure.S 𝒮)
                   {K : Type ℓ} (emb : K → ZFStructure.S 𝒮) where

ここで隠すのは引数構造の修飾されていない Agda 名 _∈ˢ_ だけであり、充足関係 _⊨₀_ の原子的所属は引き続き 𝒮 によって解釈されます。台の名前を替えるのは、本章が周囲の台を指すときの曖昧さをなくすためです。

  open ZFStructure 𝒮 hiding ( _∈ˢ_ ) renaming ( S to S𝒮 )

項代数の充足は、自明に空な定数領域のもとで述べられます。評価される論理式は、定数記号を使わずに作られたものだけで、純粋な所属と等号の言語であり、充足は命題値です。この節の各問いと閉包の主張は、すべてこの読みを用います。

  private module Sem = FOL.Semantics 𝒮
  open Sem using () renaming ( _^_ to _^𝒮_ )
  module At0 = Sem.At (⊥* {ℓ}) Empty.rec* using ( _⊨_ )
  _⊨₀_ : {n : ℕ} → 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) ⊨₀ ψ ⟩ ∥₁

この切り詰められた存在が与えられれば、search は、引数 wo として渡された特定の狭義整列順序のもとで最小の充足要素を返します。最小とはその整列順序での最小のことであり、所属に関する極小でもランクの比較でもありません。

  search : (k : ℕ) (ψ : Formula (⊥* {ℓ}) (suc k)) (vs : Vec S𝒮 k)
         → Sat k ψ vs → S𝒮
  search k ψ vs w = leastOf wo {ℓ'' = ℓ-suc ℓ} lem (λ a → (a ∷ vs) ⊨₀ ψ) 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) = Sum.rec (search k ψ (vals cs)) (λ _ → junk)
                       (lem (Sat k ψ (vals cs) , squash₁))

この小さな補題は、命題の目標に要素があると分かったとき、古典的な判定がどのように使われるかを記録します。判定が左枝なら、命題性によりその要素は x と同一視され、消去結果は f x になります。右枝なら、その否定は x と矛盾するため、その場合は不可能です。

  sum-stuck : {X : Type (ℓ-suc ℓ)} (x : X) (px : isProp X)
            → (f : X → S𝒮) (g : (X → Empty.⊥) → S𝒮) (s : X ⊎ (X → Empty.⊥))
            → Sum.rec f g s ≡ f x
  sum-stuck x px f g (Sum.inl x') = sym (cong f (px x x'))
  sum-stuck x px f g (Sum.inr h)  = Empty.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)
                       (lem (Sat k ψ (vals cs) , squash₁))

コードのベクトルの評価は、その上で評価を写すことと同じであり、簡単な再帰で示されます。これにより、後の主張は環境の再帰的な形と写した形の間を自由に行き来できます。

  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 = leastOf wo {ℓ'' = ℓ-suc ℓ} lem (λ a → (a ∷ vals cs) ⊨₀ ψ) 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) (δ : SA ^ n)
          → (δ ⊨ᴬ φ) ≡ (map g δ ⊨ᴮ mapFo g φ)
  Witness : (SA → SB) → Type (ℓ-suc ℓ)
  Witness g = (n : ℕ) (φ : Formula SA (suc n)) (δ : 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) (δ : SA ^ n)
         → (δ ⊨ᴬ (t ∈̇ u)) ≡ (map g δ ⊨ᴮ mapFo g (t ∈̇ u)))
    (at≐ : (n : ℕ) (t u : Term SA n) (δ : 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) (δ : 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) (δ : 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) (δ : 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) (δ : SA ^ n)
             → (fst x ∈ˢ fst (⟦ mapTm g (renameTm suc t) ⟧ᴮ (x ∷ map g δ)))
             ≡ (fst x ∈ˢ fst (⟦ mapTm g t ⟧ᴮ (map g δ)))
      memRen t x δ = cong (λ s → fst x ∈ˢ fst s) (renG t x δ)
      memPath : {n : ℕ} (t : Term SA n) (q : SA) (δ : SA ^ n)

有界量化子の副条件は、写像を越えて移ります。連鎖は、源の構造で弱めることから始まり、ずらした環境のもとで所属の原子的な仮定を適用します。

              → (fst q ∈ˢ fst (⟦ t ⟧ᴬ δ))
              ≡ (fst (g q) ∈ˢ fst (⟦ mapTm g t ⟧ᴮ (map g δ)))
      memPath {n} t q δ =
        cong (λ s → fst q ∈ˢ fst s) (sym (renA t q δ))
        ∙ at∈ (suc n) (var zero) (renameTm suc t) (q ∷ δ)

連鎖は、目標の構造での弱めで終わります。これで、どの有界の場合の副条件も、写像の両側で読めます。

        ∙ memRen t (g q) δ

古典的な段階は一度だけまとめられます。命題に対する二重否定の除去は排中律から従います。全称の場合の順方向では、目標側の反例を仮定し、それを否定された行列の存在証人として包み、Witness で内側へ引き戻して矛盾を導きます。最後に dne が必要な目標側の真理を与えます。

      dne : (P : hProp (ℓ-suc ℓ)) → (((⟨ P ⟩) → Empty.⊥) → Empty.⊥) → ⟨ P ⟩
      dne P h = Sum.rec (λ p → p)
        (λ (np : ⟨ P ⟩ → Empty.⊥) → Empty.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 = PT.rec (snd (map g δ ⊨ᴮ mapFo g (∃̇ ψ)))
        (λ { (q , hq) → ∣ g q , subst ⟨_⟩ (agree (suc n) ψ (q ∷ δ)) hq ∣₁ })
      bwd : ⟨ map g δ ⊨ᴮ mapFo g (∃̇ ψ) ⟩ → ⟨ δ ⊨ᴬ (∃̇ ψ) ⟩
      bwd h = PT.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 で否定された行列を充足します。その否定に証人の原理を施すと、像が否定を充足する内側の点が返り、その点での一致が、すべての内側の点が行列を充足するという仮定と矛盾します。

        PT.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) → ⟨ fst q ∈ˢ fst (⟦ t ⟧ᴬ δ) ⟩ → ⟨ (q ∷ δ) ⊨ᴬ ψ ⟩)
          → (x : SB) → ⟨ fst x ∈ˢ fst (⟦ mapTm g t ⟧ᴮ (map g δ)) ⟩
          → ⟨ (x ∷ map g δ) ⊨ᴮ mapFo g ψ ⟩
      fwd h x hx =
        dne ((x ∷ map g δ) ⊨ᴮ mapFo g ψ) λ nx →

証人の原理を補助の論理式に施すと、内側の点 q が返ります。その像は上界に属しますが、行列を反証します。像の上界への所属は、弱めと memPath を通して運び戻され、一致が行列の内側での充足を像へ持ち上げて、失敗と矛盾します。

        PT.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) → ⟨ fst x ∈ˢ fst (⟦ mapTm g t ⟧ᴮ (map g δ)) ⟩
                   → ⟨ (x ∷ map g δ) ⊨ᴮ mapFo g ψ ⟩)
          → (q : SA) → ⟨ fst q ∈ˢ fst (⟦ t ⟧ᴬ δ) ⟩ → ⟨ (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 ] (⟨ fst q ∈ˢ fst (⟦ t ⟧ᴬ δ) ⟩ × ⟨ (q ∷ δ) ⊨ᴬ ψ ⟩) ∥₁
          → ∥ Σ[ x ∈ SB ] (⟨ fst x ∈ˢ fst (⟦ mapTm g t ⟧ᴮ (map g δ)) ⟩
                        × ⟨ (x ∷ map g δ) ⊨ᴮ mapFo g ψ ⟩) ∥₁
      fwd = PT.map (λ { (q , hq , hψ) →

二つの成分は別々に運ばれます。副条件は memPath で、行列は一致によって運ばれます。逆方向はその逆を述べ、外側の証人の対が内側の対を与えます。

        g q , (subst ⟨_⟩ (memPath t q δ) hq ,
               subst ⟨_⟩ (agree (suc n) ψ (q ∷ δ)) hψ) })
      bwd : ∥ Σ[ x ∈ SB ] (⟨ fst x ∈ˢ fst (⟦ mapTm g t ⟧ᴮ (map g δ)) ⟩
                        × ⟨ (x ∷ map g δ) ⊨ᴮ mapFo g ψ ⟩) ∥₁
          → ∥ Σ[ q ∈ SA ] (⟨ fst q ∈ˢ fst (⟦ t ⟧ᴬ δ) ⟩ × ⟨ (q ∷ δ) ⊨ᴬ ψ ⟩) ∥₁

逆方向は、補助の形で読んだ外側の対に証人の原理を走らせ、内側の点とその像の対を得ます。成分は、弱めと memPath、そして一致によって運び戻されます。

      bwd h = PT.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 δ (PT.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 = fst c , M⊆L (fst c) (snd c)

初等性は、この包含のもとで充足が変わらないことを、台のすべての論理式と環境に対して述べます。これは命題の間のパスであり、二つの原子式についての合同性と証人の原理がこの形で合成されます。

    Elementary : Type (ℓ-suc (ℓ-suc ℓ))
    Elementary = (n : ℕ) (φ : Formula SM n) (δ : SM ^ n)
               → (δ ⊨ᵐ φ) ≡ (map inL δ AbsL.⊨ᵐ (mapFo inL φ))

Tarski-Vaught の判定条件は、初等性の証人の形です。段階がある環境の像のもとで存在の論理式を充足するなら、台のある要素の像がそこで行列を充足します。充足が命題値なので、単に存在すれば足ります。

    TarskiVaught : Type (ℓ-suc ℓ)
    TarskiVaught = (n : ℕ) (φ : Formula SM (suc n)) (δ : SM ^ n)
                 → ⟨ map inL δ AbsL.⊨ᵐ (mapFo inL (∃̇ φ)) ⟩
                 → ∥ Σ[ q ∈ SM ] ⟨ (inL q ∷ map inL δ) AbsL.⊨ᵐ (mapFo inL φ) ⟩ ∥₁

各点での包含は環境の参照と可換です。これは項の一致に必要な変数の場合です。

    private
      lookup-inL : {n : ℕ} (i : Fin n) (δ : 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) (δ : SM ^ n)
               → fst (⟦ t ⟧ᵐ δ) ≡ fst (AbsL.⟦ mapTm inL t ⟧ᵐ (map inL δ))
      tm-agree n (con c) δ = refl
      tm-agree n (var i) δ = sym (cong 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 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 = PT.rec (snd (x ∈ˢ Lset α)) go x∈H
      where
      go : Σ[ c ∈ Code ] (fst (val c) ≡ x) → ⟨ x ∈ˢ Lset α ⟩
      go (c , q) = subst (λ z → ⟨ z ∈ˢ Lset α ⟩) q (snd (val c))

所属は、切り詰められた存在としてしか読み戻せません。包の要素はあるコードの値ですが、コードは選ばれません。異なるコードが同じ値に評価しうるので、これが提示の正直な形です。

    hull-member : (x : S) → ⟨ x ∈ˢ Hull ⟩
                → ∥ Σ[ c ∈ Code ] (fst (val c) ≡ x) ∥₁
    hull-member x x∈H = x∈H

逆方向には切り詰めは要りません。提示自身の導入規則により、どのコードの値も要素です。

    val-in-Hull : (c : Code) → ⟨ fst (val c) ∈ˢ 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 ⟩)

閉性の条件 p∈ に加えて、写像 p には四つの仮定を置きます。iso-fwd は所属を保存し、iso-bwd は所属を反映し、最後の二つの引数は M 上の単射性と終域 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 は M 上で単射であり、PM へ単に全射です。保存と反映と合わせて、これらはまさに二つの構造の間の所属の同型のデータです。

          → p x ≡ p y → x ≡ y)
  (surj : (z : S) (z∈ : ⟨ z ∈ˢ PM ⟩)
        → ∥ Σ[ y ∈ S ] (⟨ y ∈ˢ M ⟩ × (p y ≡ z)) ∥₁)
  where

源の台は、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 (fst m) , p∈ (fst m) (snd m)

始域の意味論は、M に制限した構造で項と論理式を解釈します。

  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∈) = PT.map (λ { (y , y∈ , e) →
    (y , y∈) , Σ≡Prop (λ w → (w ∈ˢ PM) .snd) e }) (surj z z∈)

一般の充足関係の移送定理を、M と PM への所属述語に適用できます。所属の保存と反映が、その所属原子式の場合を与えます。

  module Tr = SatTransfer (λ x → x ∈ˢ M) (λ x → x ∈ˢ PM)

写像 p は環境に各索引ごとに施されるので、参照は一度に一つずつ簡約できます。

  private
    lookup-g : {n : ℕ} (i : Fin n) (δ : SM ^ n)
             → p (fst (lookup i δ)) ≡ fst (lookup i (map g δ))
    lookup-g zero (m ∷ δ) = refl
    lookup-g (suc i) (m ∷ δ) = lookup-g i δ

項は写像 p のもとで一致します。M の項の値に p を施すことは、写された項を写された環境で評価することと等しくなります。定数は固定的で、変数は参照に従います。所属の原子式がここで述べられます。

    tm-agree : {n : ℕ} (t : Term SM n) (δ : SM ^ n)
             → p (fst (⟦ t ⟧ᵐ δ)) ≡ fst (⟦ mapTm g t ⟧ᵖᵐ (map g δ))
    tm-agree (con m) δ = refl
    tm-agree (var i) δ = lookup-g i δ
    at∈ : (n : ℕ) (t u : Term SM n) (δ : SM ^ n)

原子項の所属は両方向に移ります。順方向は、内側の所属を項の等式に沿って運び、所属を保存する iso-fwd に渡します。

        → (δ ⊨ᵐ (t ∈̇ u)) ≡ (map g δ ⊨ᵖᵐ mapFo g (t ∈̇ u))
    at∈ n t u δ = ⇔toPath
      (λ h → subst (λ z → ⟨ fst (⟦ mapTm g t ⟧ᵖᵐ (map g δ)) ∈ˢ z ⟩) (tm-agree u δ)
        (subst (λ z → ⟨ z ∈ˢ p (fst (⟦ u ⟧ᵐ δ)) ⟩) (tm-agree t δ)
          (iso-fwd (fst (⟦ u ⟧ᵐ δ)) (fst (⟦ t ⟧ᵐ δ)) (snd (⟦ u ⟧ᵐ δ))

順方向の輸送は、p を施した後の所属に着地します。逆方向は、同型を通してその所属を反映し、項の等式に沿って内側の所属を復元します。

            (snd (⟦ t ⟧ᵐ δ)) h)))
      (λ h → iso-bwd (fst (⟦ u ⟧ᵐ δ)) (fst (⟦ t ⟧ᵐ δ)) (snd (⟦ u ⟧ᵐ δ))
        (snd (⟦ t ⟧ᵐ δ))
        (subst (λ z → ⟨ p (fst (⟦ t ⟧ᵐ δ)) ∈ˢ z ⟩) (sym (tm-agree u δ))
          (subst (λ z → ⟨ z ∈ˢ fst (⟦ mapTm g u ⟧ᵖᵐ (map g δ)) ⟩)

逆方向が所属の節を閉じます。項の等式に導かれた同型を通した反映が、内側の所属をちょうど返します。等号の原子式と証人の原理は、残りの仮定が扱います。

            (sym (tm-agree t δ)) h)))

アトムの項の等号は、等式の両辺に崩壊を施すことで移ります。順方向は、M における値の等式を取り、cong で p を施し、項の同約によって両辺を写された項へ運びます。

    at≐ : (n : ℕ) (t u : Term SM n) (δ : SM ^ n)
        → (δ ⊨ᵐ (t ≐ u)) ≡ (map g δ ⊨ᵖᵐ mapFo g (t ≐ u))
    at≐ n t u δ = ⇔toPath
      (λ h → subst (λ z → z ≡ fst (⟦ mapTm g u ⟧ᵖᵐ (map g δ))) (tm-agree t δ)
        (subst (λ z → p (fst (⟦ t ⟧ᵐ δ)) ≡ z) (tm-agree u δ) (cong p h)))

逆方向は、単射性が活きる場所です。崩壊した両辺が等しいことから、p-inj がもとの値の等しさを取り戻します。二つの向きで、等号のアトムが命題の間のパスになります。

      (λ h → p-inj (fst (⟦ t ⟧ᵐ δ)) (fst (⟦ u ⟧ᵐ δ)) (snd (⟦ t ⟧ᵐ δ))
        (snd (⟦ u ⟧ᵐ δ))
        (subst (λ z → z ≡ p (fst (⟦ u ⟧ᵐ δ))) (sym (tm-agree t δ))
          (subst (λ z → fst (⟦ mapTm g t ⟧ᵖᵐ (map g δ)) ≡ z)
            (sym (tm-agree u δ)) h)))

証人の原理は全射から作られます。像の中の外側の証人 p' は、単に、M のある q の崩壊です。その同一視に沿って充足を運ぶと、内側の証人と、像の中での充足が得られます。

    wit : Tr.Witness g
    wit n ψ δ h = PT.rec squash₁
      (λ { (p' , hp) → PT.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) (δ : SM ^ n)
        → (δ ⊨ᵐ φ) ≡ (map g δ ⊨ᵖᵐ mapFo g φ)
  agree = Tr.Along.agree g at∈ at≐ wit

一致は、後で合成するために二つの片方向の形で記録されます。順方向には、内側の充足から、写された環境での写された論理式の充足が得られます。

  iso-inv : (n : ℕ) (φ : Formula SM n) (δ : SM ^ n)
          → ⟨ δ ⊨ᵐ φ ⟩ → ⟨ map g δ ⊨ᵖᵐ mapFo g φ ⟩
  iso-inv n φ δ = subst ⟨_⟩ (agree n φ δ)

逆方向は、外側の充足を内側の充足へ戻します。本章は次に、外延性をもつ集合 X の崩壊のもとでこの不変性を具体化し、所属の同型と単射性を伴って崩壊を開きます。

  iso-inv-bwd : (n : ℕ) (φ : Formula SM n) (δ : 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 = PT.map (λ { (c , e) → c , Σ≡Prop (λ z → (z ∈ˢ Lset α) .snd) e })
    (H.hull-member (fst q) (snd q))

コードは、一つの要素から有限の環境へ持ち上がります。空の環境は空のベクトルで符号化され、再帰の場合は、新しいコードを、すでに作られたコードの列に加えます。

  codeEnv : {n : ℕ} (δ : Vec A.SM n)
          → ∥ Σ[ ds ∈ Vec H.T.Code n ]
               (map H.T.val ds ≡ map A.inL δ) ∥₁
  codeEnv [] = ∣ [] , refl ∣₁
  codeEnv (q ∷ δ) = PT.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 = PT.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) = PT.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 = PT.map (λ { (b , hb) →
        b , subst ⟨_⟩ (sym (body-path b)) hb }) h

探索は、符号化された環境のもとで抽象された本体を満たす、包の中の最小の証人を返します。変換は、これをもとの論理式に対する Tarski-Vaught の対へ変える必要があります。

      finish : Σ[ a ∈ ASt.SL ]
                 ( ⟨ fst a ∈ˢ 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 = fst a , a∈H

証人の段階への包含は、証人そのものです。二つの台は、命題値の所属の証明だけが違い、それは反射性によって同一視されます。

        q≡a : A.inL q ≡ a
        q≡a = Σ≡Prop (λ z → (z ∈ˢ Lset α) .snd) 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 → Empty.rec* b) using ( _⊨_ )

パラメータなしの論理式の周囲の充足は、再利用のために名付けられます。重要な観察はこうです。パラメータなしの論理式は、改名しても変わらない。写し直す定数がないからです。

_⊨ₚ_ : {n : ℕ} → 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 Empty.rec* f φ
  ∙ cong (λ h → mapFo h φ) (funExt (λ b → Empty.rec* b))
opaque
  isOrdAt : Formula (⊥* {ℓ-suc ℓ}) 

順序数性は、一つの枠をもつ有界論理式によって、引数自身が推移的であり、そのすべての要素も推移的であることとして表されます。

  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 ℓ}) 

三つの枠をもつ論理式の最初の連言支は、引数の要素の要素が引数の要素であること、すなわち第二の枠で読まれる推移性を言います。

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 φ ≡ )
         → Δ₀ φ → Δ₀ (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