可以直接阅读本章，也可以通过交互式目录和依赖图选择其他路线。

交互式目录 · 依赖图

固定宇宙层级 ℓ。保留这个层级参数，使构造可以在所需的各个大小处实例化，而不必把不同的宇宙视为同一个。

module L.Coding.Quantification {ℓ : Level} where

本章提供码化公式共用的有穷槽位工具：为深层嵌套的槽位命名，把有穷公式族折叠成合取与析取，并定义拆出码化有序对分量的有界公式及隐藏容器见证的读式。

码化语法需要反复量化一个配对的分量。本章以码化词汇与配对表达式为基础，构造这些量词共用的槽位运算、有界公式与语义读式。塔规格最先使用这些读式，随后码域、满足子句与码化图诸章继续复用。它们都能按分量陈述数学内容，无须重复有界语法所需的容器见证。

module E = CodingExpressions.PairExpression
open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_ )
open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( ⁅_,_⁆; ⁅_⁆s; module InfinitySet )
open InfinitySet {ℓ} using ( sucV )

open hPropView 𝒮ʟ using ( S )

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

槽位索引与基本读式

移位运算与具名内部槽位组织深层嵌套的绑定，而有序对与后继读式把相应原子公式读回为集合等式。

英文原文

Slot arithmetic. sh k pushes an outer slot past k binders; the names i0 .. i19 are the innermost slots at any arity.

i0 : ∀ {j} → Fin (suc j)
i0 = zero
i1 : ∀ {j} → Fin (2 + j)
i1 = suc i0
i2 : ∀ {j} → Fin (3 + j)
i2 = suc i1
i3 : ∀ {j} → Fin (4 + j)
i3 = suc i2

pr-out : ∀ {m} (q u v : Fin m) (γ : Vec S m) → ⟨ γ ⊨ prAtL q u v ⟩
       → (lookup q γ) .fst ≡ pr ((lookup u γ) .fst) ((lookup v γ) .fst)
pr-out q u v γ h = subst ⟨_⟩ (prAtL-adequate q u v γ) h

pr-in : ∀ {m} (q u v : Fin m) (γ : Vec S m)
      → (lookup q γ) .fst ≡ pr ((lookup u γ) .fst) ((lookup v γ) .fst)
      → ⟨ γ ⊨ prAtL q u v ⟩
pr-in q u v γ e = subst ⟨_⟩ (sym (prAtL-adequate q u v γ)) e

down : (x : S) (y : V ℓ) → ⟨ y ∈ x .fst ⟩ → S
down x y h = y , isL-trans {x = x .fst} {y = y} h (x .snd)
英文原文

The components of a pair held as an element of L, as elements of L.

fstS sndS : (x : S) (u v : V ℓ) → x .fst ≡ pr u v → S
fstS x u v e = down (down x ⁅ u , v ⁆ (subst (λ z → ⟨ ⁅ u , v ⁆ ∈ z ⟩) (sym e) (∈pair-introR {u = ⁅ u ⁆s} {v = ⁅ u , v ⁆} refl))) u (∈pair-introL {u = u} {v = v} refl)
sndS x u v e = down (down x ⁅ u , v ⁆ (subst (λ z → ⟨ ⁅ u , v ⁆ ∈ z ⟩) (sym e) (∈pair-introR {u = ⁅ u ⁆s} {v = ⁅ u , v ⁆} refl))) v (∈pair-introR {u = u} {v = v} refl)

sh : ∀ {m} (k : ℕ) → Fin m → Fin (k + m)
sh 0 i = i
sh (suc k) i = suc (sh k i)

i4 : ∀ {j} → Fin (5 + j)
i4 = suc i3
i5 : ∀ {j} → Fin (6 + j)
i5 = suc i4
i6 : ∀ {j} → Fin (7 + j)
i6 = suc i5
i7 : ∀ {j} → Fin (8 + j)
i7 = suc i6
i8 : ∀ {j} → Fin (9 + j)
i8 = suc i7
i9 : ∀ {j} → Fin (10 + j)
i9 = suc i8
i10 : ∀ {j} → Fin (11 + j)
i10 = suc i9
i11 : ∀ {j} → Fin (12 + j)
i11 = suc i10
i12 : ∀ {j} → Fin (13 + j)
i12 = suc i11
i13 : ∀ {j} → Fin (14 + j)
i13 = suc i12
i14 : ∀ {j} → Fin (15 + j)
i14 = suc i13
i15 : ∀ {j} → Fin (16 + j)
i15 = suc i14
i16 : ∀ {j} → Fin (17 + j)
i16 = suc i15
i17 : ∀ {j} → Fin (18 + j)
i17 = suc i16
i18 : ∀ {j} → Fin (19 + j)
i18 = suc i17
i19 : ∀ {j} → Fin (20 + j)
i19 = suc i18

十个具名槽位与有穷联结词折叠

模式 f0 至 f9 命名构造子族使用的十个位置，而 bigOr 与 bigAnd 把任意非空有穷公式族折叠起来。相应读式选出一个析取项或恢复每个合取项，并不依赖任何特定编码方案。

pattern f0 = zero
pattern f1 = suc f0
pattern f2 = suc f1
pattern f3 = suc f2
pattern f4 = suc f3
pattern f5 = suc f4
pattern f6 = suc f5
pattern f7 = suc f6
pattern f8 = suc f7
pattern f9 = suc f8

bigOr bigAnd : ∀ {m} (n : ℕ) → (Fin (suc n) → Formula S m) → Formula S m
bigOr 0 φ = φ zero
bigOr (suc n) φ = φ zero ∨̇ bigOr n (λ k → φ (suc k))
bigAnd 0 φ = φ zero
bigAnd (suc n) φ = φ zero ∧̇ bigAnd n (λ k → φ (suc k))

module _ {m : ℕ} (γ : Vec S m) where

bigOr-in : (n : ℕ) (φ : Fin (suc n) → Formula S m) (k : Fin (suc n))
         → ⟨ γ ⊨ φ k ⟩ → ⟨ γ ⊨ bigOr n φ ⟩
bigOr-in 0 φ zero h = h
bigOr-in (suc n) φ zero h = ∣ inl h ∣₁
bigOr-in (suc n) φ (suc k) h = ∣ inr (bigOr-in n (λ j → φ (suc j)) k h) ∣₁

bigOr-out : (n : ℕ) (φ : Fin (suc n) → Formula S m) → ⟨ γ ⊨ bigOr n φ ⟩
          → ∥ Σ[ k ∶ Fin (suc n) ] ⟨ γ ⊨ φ k ⟩ ∥₁
bigOr-out 0 φ h = ∣ zero , h ∣₁
bigOr-out (suc n) φ = rec₁ squash₁
  (λ { (inl h) → ∣ zero , h ∣₁
     ; (inr h) → map₁ (λ { (k , hk) → suc k , hk }) (bigOr-out n (λ j → φ (suc j)) h) })

bigAnd-in : (n : ℕ) (φ : Fin (suc n) → Formula S m)
          → ((k : Fin (suc n)) → ⟨ γ ⊨ φ k ⟩) → ⟨ γ ⊨ bigAnd n φ ⟩
bigAnd-in 0 φ h = h zero
bigAnd-in (suc n) φ h = h zero , bigAnd-in n (λ j → φ (suc j)) (λ k → h (suc k))

bigAnd-out : (n : ℕ) (φ : Fin (suc n) → Formula S m) → ⟨ γ ⊨ bigAnd n φ ⟩
           → (k : Fin (suc n)) → ⟨ γ ⊨ φ k ⟩
bigAnd-out 0 φ h zero = h
bigAnd-out (suc n) φ h zero = h .fst
bigAnd-out (suc n) φ h (suc k) = bigAnd-out n (λ j → φ (suc j)) (h .snd) k

有界原子与后继语义

有序对与后继原子取得 Δ₀ 见证，而 suc-out 与 suc-in 给出变元环境处的两个语义方向。

英文原文

The atoms and their certificates.

Δ₀-prAtL : ∀ {m} (q u v : Fin m) → Δ₀ (prAtL q u v)
Δ₀-prAtL q u v = Δ₀-liftFo _ (Δ₀-prAt q u v)

Δ₀-sucAtL : ∀ {m} (i j : Fin m) → Δ₀ (sucAtL i j)
Δ₀-sucAtL i j = Δ₀-liftFo _ (Δ₀-sucAt i j)
英文原文

The successor reader, both ways, at a variable environment.

suc-out : ∀ {m} (i j : Fin m) (γ : Vec S m) → ⟨ γ ⊨ sucAtL i j ⟩
        → (lookup j γ) .fst ≡ sucV ((lookup i γ) .fst)
suc-out i j γ h = subst ⟨_⟩ (sucAtL-adequate i j γ) h

suc-in : ∀ {m} (i j : Fin m) (γ : Vec S m)
       → (lookup j γ) .fst ≡ sucV ((lookup i γ) .fst) → ⟨ γ ⊨ sucAtL i j ⟩
suc-in i j γ e = subst ⟨_⟩ (sym (sucAtL-adequate i j γ)) e

对有序对分量的有界量化

四个宏 sndEx、sndAll、bothEx 与 bothAll 通过内部容器绑定有序对分量；它们给出的存在与全称形式均保持为 Δ₀。

英文原文

The pair as a container. Both components of pr u v lie in the member ⁅ u , v ⁆ of it. This is what lets a Δ₀ formula bind the components of a pair it holds, with no ambient bound at all.

英文原文

The opaque pair container is supplied by L.Coding.Model and shared with its structural pair-expression reader.

英文原文

The destructors. Four macros bind the components of a pair held at a slot: the second component alone (the first is a slot already), or both, each under an existential or a universal. The body sits at v ∷ s ∷ γ, or at v ∷ u ∷ s ∷ γ, with s the container. Every reader is at a variable environment; the container is junk the reader supplies.

sndEx : ∀ {m} → Fin m → Fin m → Formula S (2 + m) → Formula S m
sndEx x u body =
  ∃̇∈ (var x) (∃̇∈ (var i0) (prAtL (sh 2 x) (sh 2 u) i0 ∧̇ body))

sndAll : ∀ {m} → Fin m → Fin m → Formula S (2 + m) → Formula S m
sndAll x u body =
  ∀̇∈ (var x) (∀̇∈ (var i0) (prAtL (sh 2 x) (sh 2 u) i0 ⇒̇ body))

bothEx : ∀ {m} → Fin m → Formula S (3 + m) → Formula S m
bothEx x body =
  ∃̇∈ (var x) (∃̇∈ (var i0) (∃̇∈ (var i1) (prAtL (sh 3 x) i1 i0 ∧̇ body)))

bothAll : ∀ {m} → Fin m → Formula S (3 + m) → Formula S m
bothAll x body =
  ∀̇∈ (var x) (∀̇∈ (var i0) (∀̇∈ (var i1) (prAtL (sh 3 x) i1 i0 ⇒̇ body)))

Δ₀-sndEx : ∀ {m} (x u : Fin m) (body : Formula S (2 + m)) → Δ₀ body → Δ₀ (sndEx x u body)
Δ₀-sndEx x u body d = δ-∃∈ (δ-∃∈ (δ-∧ (Δ₀-prAtL (sh 2 x) (sh 2 u) i0) d))

Δ₀-sndAll : ∀ {m} (x u : Fin m) (body : Formula S (2 + m)) → Δ₀ body → Δ₀ (sndAll x u body)
Δ₀-sndAll x u body d = δ-∀∈ (δ-∀∈ (δ-⇒ (Δ₀-prAtL (sh 2 x) (sh 2 u) i0) d))

Δ₀-bothAll : ∀ {m} (x : Fin m) (body : Formula S (3 + m)) → Δ₀ body → Δ₀ (bothAll x body)
Δ₀-bothAll x body d = δ-∀∈ (δ-∀∈ (δ-∀∈ (δ-⇒ (Δ₀-prAtL (sh 3 x) i1 i0) d)))

module _ {m : ℕ} (x u : Fin m) (body : Formula S (2 + m)) (γ : Vec S m) where

private
  X = (lookup x γ) .fst
  U = (lookup u γ) .fst

读取分量量词

存在式的 out 引理从满足关系返回分量数据的命题截断，只记录合适分量的仅仅存在性；全称式读引理则接收明确的分量。相应的 in 引理从明确的数据重建满足关系，并应用有序对的单射性得到相应的取值等式。

英文原文

Out: the witness's second component is pinned by pair injectivity.

sndEx-out : ⟨ γ ⊨ sndEx x u body ⟩
          → ∥ Σ[ v ∶ S ] Σ[ s ∶ S ] ((X ≡ pr U (v .fst)) × ⟨ (v ∷ s ∷ γ) ⊨ body ⟩) ∥₁
sndEx-out = rec₁ squash₁ (λ { (s , (s∈ , h)) → map₁
  (λ { (v , (v∈ , (e , hb))) → v , s , (pr-out (sh 2 x) (sh 2 u) i0 (v ∷ s ∷ γ) e , hb) })
  h })

sndEx-in : (v s : S) → ⟨ s .fst ∈ X ⟩ → ⟨ v .fst ∈ s .fst ⟩ → X ≡ pr U (v .fst)
         → ⟨ (v ∷ s ∷ γ) ⊨ body ⟩ → ⟨ γ ⊨ sndEx x u body ⟩
sndEx-in v s s∈ v∈ e hb = ∣ s , (s∈ , ∣ v , (v∈ , (pr-in (sh 2 x) (sh 2 u) i0 (v ∷ s ∷ γ) e , hb)) ∣₁) ∣₁

sndAll-out : ⟨ γ ⊨ sndAll x u body ⟩
           → (v s : S) → ⟨ s .fst ∈ X ⟩ → ⟨ v .fst ∈ s .fst ⟩ → X ≡ pr U (v .fst)
           → ⟨ (v ∷ s ∷ γ) ⊨ body ⟩
sndAll-out h v s s∈ v∈ e = h s s∈ v v∈ (pr-in (sh 2 x) (sh 2 u) i0 (v ∷ s ∷ γ) e)

sndAll-in : ((v s : S) → ⟨ s .fst ∈ X ⟩ → ⟨ v .fst ∈ s .fst ⟩ → X ≡ pr U (v .fst)
             → ⟨ (v ∷ s ∷ γ) ⊨ body ⟩)
          → ⟨ γ ⊨ sndAll x u body ⟩
sndAll-in k s s∈ v v∈ e = k v s s∈ v∈ (pr-out (sh 2 x) (sh 2 u) i0 (v ∷ s ∷ γ) e)

module _ {m : ℕ} (x : Fin m) (body : Formula S (3 + m)) (γ : Vec S m) where

private
  X = (lookup x γ) .fst

bothEx-out : ⟨ γ ⊨ bothEx x body ⟩
           → ∥ Σ[ u ∶ S ] Σ[ v ∶ S ] Σ[ s ∶ S ]
               ((X ≡ pr (u .fst) (v .fst)) × ⟨ (v ∷ u ∷ s ∷ γ) ⊨ body ⟩) ∥₁
bothEx-out = rec₁ squash₁ (λ { (s , (s∈ , h)) → rec₁ squash₁
  (λ { (u , (u∈ , h')) → map₁
    (λ { (v , (v∈ , (e , hb))) → u , v , s , (pr-out (sh 3 x) i1 i0 (v ∷ u ∷ s ∷ γ) e , hb) })
    h' })
  h })

bothEx-in : (u v s : S) → ⟨ s .fst ∈ X ⟩ → ⟨ u .fst ∈ s .fst ⟩ → ⟨ v .fst ∈ s .fst ⟩
          → X ≡ pr (u .fst) (v .fst) → ⟨ (v ∷ u ∷ s ∷ γ) ⊨ body ⟩ → ⟨ γ ⊨ bothEx x body ⟩
bothEx-in u v s s∈ u∈ v∈ e hb =
  ∣ s , (s∈ , ∣ u , (u∈ , ∣ v , (v∈ , (pr-in (sh 3 x) i1 i0 (v ∷ u ∷ s ∷ γ) e , hb)) ∣₁) ∣₁) ∣₁

bothAll-out : ⟨ γ ⊨ bothAll x body ⟩
            → (u v s : S) → ⟨ s .fst ∈ X ⟩ → ⟨ u .fst ∈ s .fst ⟩ → ⟨ v .fst ∈ s .fst ⟩
            → X ≡ pr (u .fst) (v .fst) → ⟨ (v ∷ u ∷ s ∷ γ) ⊨ body ⟩
bothAll-out h u v s s∈ u∈ v∈ e = h s s∈ u u∈ v v∈ (pr-in (sh 3 x) i1 i0 (v ∷ u ∷ s ∷ γ) e)

bothAll-in : ((u v s : S) → ⟨ s .fst ∈ X ⟩ → ⟨ u .fst ∈ s .fst ⟩ → ⟨ v .fst ∈ s .fst ⟩
              → X ≡ pr (u .fst) (v .fst) → ⟨ (v ∷ u ∷ s ∷ γ) ⊨ body ⟩)
           → ⟨ γ ⊨ bothAll x body ⟩
bothAll-in k s s∈ u u∈ v v∈ e = k u v s s∈ u∈ v∈ (pr-out (sh 3 x) i1 i0 (v ∷ u ∷ s ∷ γ) e)

供应容器见证

fillSnd、fillBoth、useSnd 与 useBoth 从有序对等式自动构造内部容器，使调用方只须推理其分量。

英文原文

Supplying the junk: a pair at a slot, with its components as elements, fills any of the four.

module _ {m : ℕ} (x : Fin m) (γ : Vec S m) (u v : S)
         (e : (lookup x γ) .fst ≡ pr (u .fst) (v .fst)) where

private
  c = container (lookup x γ) u v e

fillSnd : (body : Formula S (2 + m)) → ⟨ (v ∷ c .fst ∷ γ) ⊨ body ⟩
        → (ui : Fin m) → (lookup ui γ) .fst ≡ u .fst → ⟨ γ ⊨ sndEx x ui body ⟩
fillSnd body hb ui qu = sndEx-in x ui body γ v (c .fst) (c .snd .fst) (c .snd .snd .snd)
  (e ∙ cong (λ w → pr w (v .fst)) (sym qu)) hb

fillBoth : (body : Formula S (3 + m)) → ⟨ (v ∷ u ∷ c .fst ∷ γ) ⊨ body ⟩
         → ⟨ γ ⊨ bothEx x body ⟩
fillBoth body hb = bothEx-in x body γ u v (c .fst) (c .snd .fst) (c .snd .snd .fst)
  (c .snd .snd .snd) e hb

useSnd : (body : Formula S (2 + m)) (ui : Fin m) → (lookup ui γ) .fst ≡ u .fst
       → ⟨ γ ⊨ sndAll x ui body ⟩ → ⟨ (v ∷ c .fst ∷ γ) ⊨ body ⟩
useSnd body ui qu h = sndAll-out x ui body γ h v (c .fst) (c .snd .fst) (c .snd .snd .snd)
  (e ∙ cong (λ w → pr w (v .fst)) (sym qu))

useBoth : (body : Formula S (3 + m)) → ⟨ γ ⊨ bothAll x body ⟩
        → ⟨ (v ∷ u ∷ c .fst ∷ γ) ⊨ body ⟩
useBoth body h = bothAll-out x body γ h u v (c .fst) (c .snd .fst) (c .snd .snd .fst)
  (c .snd .snd .snd) e

回顾

具名槽位与有穷联结词折叠组织反复出现的公式族。本章的有界配对公式揭示码化有序对的一个或两个分量，相应读式恢复这些分量的语义，而填充引理隐藏了在较大公式中复用这些读式时所需的容器见证。