この章を読むか、対話型目次と依存グラフで別のルートを選べます。

対話型目次 · 依存グラフ

宇宙レベル ℓ を固定し、lem : LEM (ℓ-suc ℓ) を仮定する。この仮定は該当するレベルの各命題に判定を与え、以下の構成の明示的なパラメータとして保たれる。

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

一つの存在論理式と構成可能段階から取ったパラメータに対し、周囲の構成可能宇宙に証人があればそれを含む、より大きな順序数段階を構成する。証人を選ぶ操作を反復して順序数極限を取ると、その論理式への解答について閉じた段階が得られる。

英語原文

It can be done, and the argument is Montague's. Fix a matrix and an environment of parameters. If a witness exists at all, there is a least stage containing one, and that stage is a set-sized answer to a class-sized question. Range over all tuples of parameters drawn from one stage, bound the answers, and the result is a single stage that answers for every tuple from the stage below. Iterate that step through the natural numbers and take the union: the limit answers for its own parameters, because any finite tuple from the limit already lies in some finite layer, whose answers were bounded at the next.

英語原文

Two departures from the usual practice occur here. The choice of witness is where a well-ordering of L is normally invoked, and it is not needed: what the argument requires is a canonical ordinal, not a canonical element, and the ordinals are already well-ordered by membership. So the least stage that holds a witness is taken directly, by the descent of the stage chapter, without deciding which witness is there. And the parameters are a tuple from the start. Writing the one-parameter case first and generalizing later would mean writing the whole construction twice, since every step of it is indifferent to how many parameters there are; the only place the tuple matters is in locating it, where finitely many layers have to be merged into one.

open import Cubical.Data.Nat using ( +-comm )

open import Cubical.HITs.CumulativeHierarchy.Base using ( V; sett; _∈_ )
open import Cubical.HITs.CumulativeHierarchy.Properties
  using ( ∈∈ₛ; ∈-asFiber; ⟪_⟫; ⟪_⟫↪; ∈ₛ⟪_⟫↪_ )
open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( ∅; ⋃_ )

open hPropView 𝒮ʟ using ( S )

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

環境を一つの段階から取る

LsetEnv は段階の小さな提示からパラメータ環境を作り、Below σ ρ は環境の全成分が Lset σ に属することを表す。この条件は段階を大きくすると保存される。

英語原文

An environment lies below a stage when each of its entries does. Reading the tuple of indices back off such an environment is the inverse operation, and it returns the equation as well, since the construction will need to know that the environment it bounded is the one it was given. The equation is where constructibility being a proposition is used: two elements of the model agree as soon as their underlying sets do.

LsetElt : (σ : V ℓ) → IsOrd σ → ⟪ Lset σ ⟫ → S
LsetElt σ oσ m = ⟪ Lset σ ⟫↪ m
               , Lset→isL σ oσ (⟪ Lset σ ⟫↪ m)
                   (∈∈ₛ {a = ⟪ Lset σ ⟫↪ m} {b = Lset σ} .snd (∈ₛ⟪ Lset σ ⟫↪ m))

LsetEnv : (σ : V ℓ) (oσ : IsOrd σ) {k : ℕ} → Vec (⟪ Lset σ ⟫) k → Vec S k
LsetEnv σ oσ []       = []
LsetEnv σ oσ (m ∷ ms) = LsetElt σ oσ m ∷ LsetEnv σ oσ ms

Below : (σ : V ℓ) {k : ℕ} → Vec S k → Type (ℓ-suc ℓ)
Below σ []      = ⊤*
Below σ (p ∷ ρ) = ⟨ p .fst ∈ Lset σ ⟩ × Below σ ρ

Below-mono : {σ τ : V ℓ} → ⟨ σ ∈ τ ⟩ → {k : ℕ} {ρ : Vec S k}
           → Below σ ρ → Below τ ρ
Below-mono σ∈τ {ρ = []}    _         = tt*
Below-mono σ∈τ {ρ = p ∷ ρ} (h , hs) =
  Lset-mono σ∈τ h , Below-mono σ∈τ hs

indexEnv : (σ : V ℓ) (oσ : IsOrd σ) {k : ℕ} (ρ : Vec S k) → Below σ ρ
         → Σ[ ms ∶ Vec (⟪ Lset σ ⟫) k ] (LsetEnv σ oσ ms ≡ ρ)
indexEnv σ oσ []      _        = [] , refl
indexEnv σ oσ (p ∷ ρ) (h , hs) = (m ∷ rest .fst) , cong₂ _∷_ eltEq (rest .snd)
  where
  fib = ∈-asFiber {a = p .fst} {b = Lset σ} h
  m   = fib .fst
  eltEq : LsetElt σ oσ m ≡ p
  eltEq = Σ≡Prop (λ x → ⟨ isL x ⟩isProp) (fib .snd)
  rest = indexEnv σ oσ ρ hs

解答を含む段階

存在論理式が真なら、その証人は構成可能なので最小の段階を持つ。選択した証人とその段階を一つの順序数上界へ集めることで、与えられた環境への解答を含む段階を得る。

英語原文

Totality then wants a value even when no witness exists, and the excluded middle supplies the case distinction. As in the stage chapter, the distinction is made by an explicit auxiliary rather than by a with, because the load-bearing lemma below has to name the very same decision value and match on it.

Sat : {k : ℕ} (ψ : Formula S (suc k)) (ρ : Vec S k) → S → hProp (ℓ-suc ℓ)
Sat ψ ρ q = (q ∷ ρ) ⊨ ψ

SatEx : {k : ℕ} (ψ : Formula S (suc k)) (ρ : Vec S k) → hProp (ℓ-suc ℓ)
SatEx ψ ρ = ∃[ q ∶ S ] Sat ψ ρ q

satExDecision : {k : ℕ} (ψ : Formula S (suc k)) (ρ : Vec S k)
              → Dec ⟨ SatEx ψ ρ ⟩
satExDecision ψ ρ = FOL.Semantics.decideSatisfaction 𝒮ʟ id lem ρ (∃̇ ψ)

Wit : {k : ℕ} (ψ : Formula S (suc k)) (ρ : Vec S k) → V ℓ → hProp (ℓ-suc ℓ)
Wit ψ ρ σ = ∃[ q ∶ S ] ((q .fst ∈ Lset σ) ⊓ Sat ψ ρ q)

witnessed : {k : ℕ} (ψ : Formula S (suc k)) (ρ : Vec S k) → ⟨ SatEx ψ ρ ⟩
          → ∥ (Σ[ α ∶ V ℓ ] (IsOrd α × ⟨ Wit ψ ρ α ⟩)) ∥₁
witnessed ψ ρ = rec₁ squash₁
  (λ { (q , satq) → map₁
      (λ { (α , (oα , q∈Lα)) → α , (oα , ∣ q , (q∈Lα , satq) ∣₁) })
      (q .snd) })

pick : {k : ℕ} (ψ : Formula S (suc k)) (ρ : Vec S k) → ⟨ SatEx ψ ρ ⟩
     → LeastOrd (Wit ψ ρ)
pick ψ ρ sat = leastOrd (Wit ψ ρ) (witnessed ψ ρ sat)

decideStage : {k : ℕ} (ψ : Formula S (suc k)) (ρ : Vec S k)
            → Dec ⟨ SatEx ψ ρ ⟩ → V ℓ
decideStage ψ ρ (yes sat) = pick ψ ρ sat .fst
decideStage ψ ρ (no _)    = ∅

pickStage : {k : ℕ} (ψ : Formula S (suc k)) (ρ : Vec S k) → V ℓ
pickStage ψ ρ = decideStage ψ ρ (satExDecision ψ ρ)

decideStage-ord : {k : ℕ} (ψ : Formula S (suc k)) (ρ : Vec S k)
                  (d : Dec ⟨ SatEx ψ ρ ⟩)
                → IsOrd (decideStage ψ ρ d)
decideStage-ord ψ ρ (yes sat) = pick ψ ρ sat .snd .fst
decideStage-ord ψ ρ (no _)    = ∅-ord

pickStage-ord : {k : ℕ} (ψ : Formula S (suc k)) (ρ : Vec S k)
              → IsOrd (pickStage ψ ρ)
pickStage-ord ψ ρ = decideStage-ord ψ ρ (satExDecision ψ ρ)
英語原文

And the property the whole construction rests on: if the environment is satisfiable at all, its answering stage really does hold a witness. The proof has to know which branch the decision took, and it cannot ask, because the decision is a value of the excluded middle and nothing computes it. So it does the standard thing: quantify over the branch, remember the equation that the branch is the decision, and transport along it. In the false branch the hypothesis refutes itself.

pickWitness : {k : ℕ} (ψ : Formula S (suc k)) (ρ : Vec S k) → ⟨ SatEx ψ ρ ⟩
            → ⟨ Wit ψ ρ (pickStage ψ ρ) ⟩
pickWitness ψ ρ sat = go (satExDecision ψ ρ) refl
  where
  go : (d : Dec ⟨ SatEx ψ ρ ⟩)
     → satExDecision ψ ρ ≡ d → ⟨ Wit ψ ρ (pickStage ψ ρ) ⟩
  go (yes s) e = subst (λ d → ⟨ Wit ψ ρ (decideStage ψ ρ d) ⟩) (sym e)
                   (pick ψ ρ s .snd .snd .fst)
  go (no ¬s) e = ⊥₀-rec (¬s sat)

梯子とその極限

解答を含む段階を取る操作を自然数に沿って反復し、その順序数上界を極限とする。各有限段階は次へ含まれるため、極限段階は一回の解答操作で外へ出ない。

英語原文

Stating the reach with the gap as an explicit summand, rather than through an order relation, is what makes two rungs mergeable by addition alone. That matters because merging rungs is the only thing a tuple of parameters costs, and it is worth not paying for arithmetic to do it.

英語原文

Separating the ladder from the tower is worth a moment's care, because the next chapter needs a ladder built differently: one whose single step closes all the matrices of a formula at once. Everything below is proved of the ladder, so that chapter builds its ladder and gets the argument, rather than running it again.

ClosedFor : (β : V ℓ) {k : ℕ} (ψ : Formula S (suc k)) → Type (ℓ-suc ℓ)
ClosedFor β {k} ψ = (ρ : Vec S k) → Below β ρ → ⟨ SatEx ψ ρ ⟩ → ⟨ Wit ψ ρ β ⟩

module Ladder (G : ℕ → V ℓ) (G-ord : (n : ℕ) → IsOrd (G n))
              (G-up : (n : ℕ) → ⟨ G n ∈ G (suc n) ⟩) where

reach : (n d : ℕ) → ⟨ G n ∈ G (suc (d + n)) ⟩
reach n 0    = G-up n
reach n (suc d) =
  G-ord (suc (suc (d + n))) .fst {x = G (suc (d + n))} {y = G n}
    (reach n d) (G-up (suc (d + n)))

fam : Lift {ℓ-zero} {ℓ} ℕ → V ℓ
fam i = G (lower i)

top : V ℓ
top = ⋃ (sett (Lift {ℓ-zero} {ℓ} ℕ) fam)

top-ord : IsOrd top
top-ord = setUnion-ord (Lift {ℓ-zero} {ℓ} ℕ) fam (λ i → G-ord (lower i))

G∈top : (n : ℕ) → ⟨ G n ∈ top ⟩
G∈top n = union-family-in (Lift {ℓ-zero} {ℓ} ℕ) fam (lift (suc n)) (G n) (G-up n)
英語原文

The closure argument needs its parameters on a rung, not merely under the limit. For one parameter, two inversions get it there: an ordinal in the limit belongs to one of the sets being unioned, hence to a rung; and a set in the stage of the limit belongs, by the tower's characterization, to the operator applied to the stage of some smaller ordinal, so locating that ordinal and going back in places the set in that rung's stage.

英語原文

For a tuple, the rungs found for the entries have to be merged, and the reach lemma merges two of them: from rungs n and m, both reach rung suc (n + m), one of them directly and the other after commuting the sum. Recursion on the tuple merges all of them, and monotonicity carries the earlier entries up.

δ∈top→fin : (δ : V ℓ) → ⟨ δ ∈ top ⟩ → ∥ (Σ[ N ∶ ℕ ] ⟨ δ ∈ G N ⟩) ∥₁
δ∈top→fin δ δ∈ = map₁ (λ { (i , h) → lower i , h })
  (union-family-out (Lift {ℓ-zero} {ℓ} ℕ) fam δ δ∈)

localize₁ : (e : V ℓ) → ⟨ e ∈ Lset top ⟩ → ∥ (Σ[ N ∶ ℕ ] ⟨ e ∈ Lset (G N) ⟩) ∥₁
localize₁ e e∈ = rec₁ squash₁
  (λ { (δ , (δ∈top , e∈𝒟ₒδ)) → map₁
      (λ { (N , δ∈GN) → N , Lset-in (G N) δ e δ∈GN e∈𝒟ₒδ })
      (δ∈top→fin δ δ∈top) })
  (Lset-out top e e∈)

localize : {j : ℕ} (ρ : Vec S j) → Below top ρ → ∥ (Σ[ N ∶ ℕ ] Below (G N) ρ) ∥₁
localize []      _        = ∣ zero , tt* ∣₁
localize (p ∷ ρ) (h , hs) = rec₁ squash₁
  (λ { (N , h') → map₁ (merge N h') (localize ρ hs) })
  (localize₁ (p .fst) h)
  where
  merge : (N : ℕ) → ⟨ p .fst ∈ Lset (G N) ⟩
        → Σ[ M ∶ ℕ ] Below (G M) ρ
        → Σ[ M ∶ ℕ ] Below (G M) (p ∷ ρ)
  merge N h' (M , hs') = suc (M + N)
    , ( Lset-mono (reach N M) h'
      , Below-mono (subst (λ n → ⟨ G M ∈ G (suc n) ⟩) (+-comm N M)
                      (reach M N)) hs' )

land : (q : S) (σ τ : V ℓ)
     → ⟨ q .fst ∈ Lset σ ⟩ → ⟨ σ ∈ τ ⟩ → ⟨ τ ∈ top ⟩ → ⟨ q .fst ∈ Lset top ⟩
land q σ τ fq∈σ σ∈τ τ∈top =
  Lset-mono {α = top} {β = τ} τ∈top (Lset-mono {α = τ} {β = σ} σ∈τ fq∈σ)

閉性

ClosedFor β ψ は、β より前の段階から取ったパラメータに対する ψ の証人を Lset β が含むことを表す。梯子の極限はこの条件を満たし、より大きな順序数へも移せる。

英語原文

Given it, the limit is closed for the matrix. Locate the environment on a rung and name it there: it is the image of some tuple of indices of that rung's stage, up to an equality that the reading lemma returns along with the tuple. Its answering stage is on the next rung, so whatever lives in the answering stage lives in that rung's stage, hence under the limit; two applications of monotonicity, and the equation transported back.

module _ {k : ℕ} (ψ : Formula S (suc k))
         (answers : (n : ℕ) (ms : Vec (⟪ Lset (G n) ⟫) k)
                  → ⟨ pickStage ψ (LsetEnv (G n) (G-ord n) ms) ∈ G (suc n) ⟩)
         where

closure : ClosedFor top ψ
closure ρ below sat = rec₁ squash₁ atRung (localize ρ below)
  where
  atRung : Σ[ N ∶ ℕ ] Below (G N) ρ → ⟨ Wit ψ ρ top ⟩
  atRung (N , belowN) = map₁ found (pickWitness ψ ρₘ satₘ)
    where
    idx = indexEnv (G N) (G-ord N) ρ belowN
    ρₘ : Vec S k
    ρₘ = LsetEnv (G N) (G-ord N) (idx .fst)
    e : ρₘ ≡ ρ
    e = idx .snd
    satₘ : ⟨ SatEx ψ ρₘ ⟩
    satₘ = subst (λ r → ⟨ SatEx ψ r ⟩) (sym e) sat
    found : Σ[ q ∶ S ] (⟨ q .fst ∈ Lset (pickStage ψ ρₘ) ⟩ × ⟨ Sat ψ ρₘ q ⟩)
          → Σ[ q ∶ S ] (⟨ q .fst ∈ Lset top ⟩ × ⟨ Sat ψ ρ q ⟩)
    found (q , (fq∈pick , satq)) = q
      , ( land q (pickStage ψ ρₘ) (G (suc N))
            fq∈pick (answers N (idx .fst)) (G∈top (suc N))
        , subst (λ r → ⟨ Sat ψ r q ⟩) e satq )
英語原文

This gives the theorem that later chapters use. For an environment under the limit, the class model satisfies the existential exactly when a witness lies in the limit's stage. Forwards is closure; backwards is forgetting where the witness lives.

英語原文

The forward direction needs no translation step, because the two sides are the same proposition already: the semantics of an existential quantifier is the truncated sum over the carrier, and that is what SatEx was defined to be. So the theorem is closure with its statement rewritten, and moving between syntax and the meta-level requires no further work.

reflect-bwd : (ρ : Vec S k) → ⟨ Wit ψ ρ top ⟩ → ⟨ ρ ⊨ (∃̇ ψ) ⟩
reflect-bwd ρ = map₁ (λ { (q , (_ , satq)) → q , satq })

reflect : (ρ : Vec S k) → Below top ρ → (ρ ⊨ (∃̇ ψ)) ≡ Wit ψ ρ top
reflect ρ below = ⇔toPath (closure ρ below) (reflect-bwd ρ)

一つの母式に対する段階

一つの存在母式と出発段階に対し、順序数の段階を一つ進め、出発段階を含み、その母式へのすべての必要な解答について閉じた新しい段階を返す。

英語原文

The step is sealed. Unfolded, it is a bound built from a bound built from the excluded middle, and the closure argument matches on rungs repeatedly; a transparent definition would push that whole tower into every conversion check. The three properties open the seal once each, and the last of them is the one place transitivity is used, so the chain from the answer through the bound into the step is closed inside the seal and the caller sees only its conclusion.

module Single {k : ℕ} (ψ : Formula S (suc k)) where

Fbnd : (σ : V ℓ) (oσ : IsOrd σ)
     → Σ[ β ∶ V ℓ ] (IsOrd β × ((ms : Vec (⟪ Lset σ ⟫) k)
                               → ⟨ pickStage ψ (LsetEnv σ oσ ms) ∈ β ⟩))
Fbnd σ oσ = boundingOrd (Vec (⟪ Lset σ ⟫) k)
              (λ ms → pickStage ψ (LsetEnv σ oσ ms))
              (λ ms → pickStage-ord ψ (LsetEnv σ oσ ms))

opaque
  Fstep : (σ : V ℓ) → IsOrd σ → V ℓ
  Fstep σ oσ = bound2 (Fbnd σ oσ .fst) σ (Fbnd σ oσ .snd .fst) oσ .fst

opaque
  unfolding Fstep

  Fstep-ord : (σ : V ℓ) (oσ : IsOrd σ) → IsOrd (Fstep σ oσ)
  Fstep-ord σ oσ = bound2 (Fbnd σ oσ .fst) σ (Fbnd σ oσ .snd .fst) oσ .snd .fst

  pickLand : (σ : V ℓ) (oσ : IsOrd σ) (ms : Vec (⟪ Lset σ ⟫) k)
           → ⟨ pickStage ψ (LsetEnv σ oσ ms) ∈ Fstep σ oσ ⟩
  pickLand σ oσ ms =
    Fstep-ord σ oσ .fst {x = Fbnd σ oσ .fst}
                        {y = pickStage ψ (LsetEnv σ oσ ms)}
      (Fbnd σ oσ .snd .snd ms)
      (bound2 (Fbnd σ oσ .fst) σ (Fbnd σ oσ .snd .fst) oσ .snd .snd .fst)

まとめ

一つの存在論理式について、パラメータを含む段階から始め、証人の段階を反復して順序数極限を取る。得られた段階は元の段階を含み、その論理式の存在証人について反映する。

英語原文

The construction used the excluded middle twice, once to decide satisfiability and once inside the descent, and used the axiom of choice not at all. That is the point of taking the least stage rather than the least witness: the ordinals come well-ordered, and nothing here has to ask for a well-ordering of L.

英語原文

What this chapter achieves is one quantifier, with any number of parameters. An arbitrary formula may contain many quantifiers, hence many matrices, and no limit taken for a single matrix covers them all; the next chapter builds a ladder whose step closes all of them at once, and thereby obtains everything above directly, without redoing any of the individual arguments.