構成可能なコードと部分式の木

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

本章では項のコード、論理式のコード、有限環境のグラフが L に属することを証明し、さらに各部分式上のデータを集める構成可能な木を作って、その要素を特徴づけます。

英語原文

A code is a hereditarily finite set built by pairing numerals, so it ought to be an element of L, and this chapter says so. The proof is one induction over the formula constructors with nothing in it, but the statement is what lets a later chapter treat a code as an ordinary element of the model rather than as a set of the hierarchy that happens to be lying around.

英語原文

It matters more than it looks. A recursion internalized in L takes its domain from a small family of elements of L, and the family here is the codes; a graph naming a code as a constant needs that code to be an element of the model, since the object language of the model has no other kind of constant. Both requirements are this one lemma.

英語原文

This chapter establishes constructibility of individual codes. The set of all codes over a constructible alphabet is constructed later as AllCodes in L.Coding.CodeSet; it supplies the internal syntax domain needed by the definable powerset construction.

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

open import Base.Prelude

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

open import FOL.ZFStructure using ( module hPropStructure )

open import FOL.Syntax
  using ( Term; con; var; Formula; _∈̇_; _≐_; _∧̇_; _∨̇_; _⇒̇_; ⊥̇
        ; ∃̇_; ∀̇_; ∀̇∈; ∃̇∈ )
open import FOL.Manipulation.ConstantMapping using ( mapTm; mapFo )
open import V.Coding {ℓ} using ( pr; pr-inj; module VCode )
open import L.Constructible {ℓ} using ( 𝒮ʟ; isL; IsOrd; Lset )
open import L.Coding.Model {ℓ} using ( prʟ; prʟ-fst )
open import L.Coding.Expressions {ℓ} using ( numL )
open import L.Axioms.Numerals {ℓ} using ( pairʟ; pairʟ-fst; unionʟ; unionʟ-fst )
open import L.Coding.Environment {ℓ} using ( env )
open import L.Axioms.Basic {ℓ} using ( finSet; module FinOf )

open import Cubical.Data.FinData using ( toℕ )
open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_; setIsSet )
open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( ⁅_⁆s; ⁅_,_⁆; ⋃_; _∪_; module InfinitySet )
open import Cubical.Data.Sum using ( _⊎_; inl; inr )
open import Cubical.Data.Unit using ( Unit*; tt* )
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∣_∣₁; ∥_∥₁; squash₁ )
open import V.Model {ℓ} using ( pair-singleton; pair-spec; union-spec )
open InfinitySet using ( #_; sucV )

open hPropStructure 𝒮ʟ using ( S )

構成可能な対とタグ

prL は符号化された対を作る操作について構成可能性が閉じていることを示し、tagL はそれを数項のタグに特殊化します。この二補題がすべての構文構成子の外形を扱います。

英語原文

A numeral is constructible for the same reason, but the result was already used a chapter earlier, so its proof is given there. A pair is constructible because the model has pairing, and the same equation reads it back. A tag is a pair with a numeral on the left, so it is both.

英語原文

Both are the same two steps: build the thing inside the model, then transport its membership along the equation saying that reading it out gives the thing.

prL : {a b : V ℓ} → ⟨ isL a ⟩ → ⟨ isL b ⟩ → ⟨ isL (pr a b) ⟩
prL {a} {b} pa pb =
  subst (λ w → ⟨ isL w ⟩) (prʟ-fst (a , pa) (b , pb))
    (prʟ (a , pa) (b , pb) .snd)

tagL : (k : ℕ) {x : V ℓ} → ⟨ isL x ⟩ → ⟨ isL (VCode.mkTag k x) ⟩
tagL k px = prL (numL k) px

項と論理式のコードに関する帰納法

各定数が構成可能集合を表すと仮定し、codeTmL と codeL は構造帰納法により、写像後のすべての項と論理式のコードが構成可能であることを示します。

英語原文

Terms first. A term is a variable or a constant, and the two are the two tags that terms carry: a numeral for the variable's index, and the constant's own set for a constant. So a code is constructible provided the constants it names are, and the induction takes that as its hypothesis rather than assuming there are none.

英語原文

That generality takes one extra clause and covers the parameters. A formula whose constants are members of a stage codes to a set of L exactly as a parameter-free one does, which is what lets the recursion below range over the formulas the constructible hierarchy is actually built from. The parameter-free case is the instance at the empty type.

英語原文

Then the formulas: ten clauses with no real content. Each constructor's code is a tag on either a pair of sub-codes, a single sub-code, or a numeral, and the three blocks above cover all three shapes. The induction is over the parameter-free formula rather than its embedding, which requires no extra argument because embedding is a relabelling and commutes with every constructor definitionally.

module _ {K : Type ℓ} (f : K → V ℓ) (h : (k : K) → ⟨ isL (f k) ⟩) where

  codeTmL : ∀ {n} (t : Term K n) → ⟨ isL VCode.⌜ mapTm f t ⌝ᵗ ⟩
  codeTmL (con c) = tagL 0 (h c)
  codeTmL (var i) = tagL 1 (numL _)

  codeL : ∀ {n} (φ : Formula K n) → ⟨ isL VCode.⌜ mapFo f φ ⌝ ⟩
  codeL (t ∈̇ u)  = tagL 0  (prL (codeTmL t) (codeTmL u))
  codeL (t ≐ u)  = tagL 1  (prL (codeTmL t) (codeTmL u))
  codeL (φ ∧̇ ψ)  = tagL 2  (prL (codeL φ) (codeL ψ))
  codeL (φ ∨̇ ψ)  = tagL 3  (prL (codeL φ) (codeL ψ))
  codeL (φ ⇒̇ ψ)  = tagL 4  (prL (codeL φ) (codeL ψ))
  codeL ⊥̇        = tagL 5 (numL 0)
  codeL (∃̇ φ)    = tagL 6 (codeL φ)
  codeL (∀̇ φ)    = tagL 7 (codeL φ)
  codeL (∀̇∈ t φ) = tagL 8 (prL (codeTmL t) (codeL φ))
  codeL (∃̇∈ t φ) = tagL 9 (prL (codeTmL t) (codeL φ))

環境グラフの構成可能性

envIsFinSet は環境グラフを符号化された対の有限集合と同一視し、envL はそれらの対を含む共通の順序数段階を用いてグラフを L に入れます。

英語原文

An environment is a finite set: the keys are the numerals below its length and the entries are pairs. It is, in fact, the finite set of the pairs, on the nose, because both are the same image of the same lifted index type. Saying so is one line, and it is the line that lets the finite-family lemma apply to environments without any further argument.

英語原文

The consequence is that an environment over a stage is an element of L immediately: its entries are pairs of a numeral with a member of the stage, and both are in the stage after one step. No recursion on the length, and no replacement.

envIsFinSet : ∀ {n} (g : Fin n → V ℓ)
            → env g ≡ finSet n (λ i → pr (# (toℕ i)) (g i))
envIsFinSet g = refl

envL : (σ : V ℓ) (oσ : IsOrd σ) {n : ℕ} (g : Fin n → V ℓ)
     → ((i : Fin n) → ⟨ pr (# (toℕ i)) (g i) ∈ Lset σ ⟩)
     → ⟨ isL (env g) ⟩
envL σ oσ {n} g h =
  subst (λ w → ⟨ isL w ⟩) (sym (envIsFinSet g))
    (FinOf.finSetL σ oσ n (λ i → pr (# (toℕ i)) (g i)) h)

和集合と一元集合

一元集合と二項和集合の構成を、階層の台となる集合と L の要素の双方について実装し、導入・除去補題によってその要素条件を明らかにします。

英語原文

Two more shapes, and the model supplies both directly. A singleton is the pair of a thing with itself, and a binary union is the union of the pair, so each is the model's own operation read through the underlying set.

英語原文

Each shape comes twice over. Once on the underlying set, with the two lemmas that read a member of a singleton or of a binary union back, and once on the model's own sets, where a proof of constructibility accompanies each step and the same lemmas are restated through the equation that reads the underlying set out. The recursion below runs on the second, so a set it builds is an element of L by construction and not by a second induction.

sgl-out : (a x : V ℓ) → ⟨ x ∈ ⁅ a ⁆s ⟩ → x ≡ a
sgl-out a x h = PT.rec (setIsSet x a) (λ { (inl e) → e ; (inr e) → e })
  (subst ⟨_⟩ (pair-spec a a x)
    (subst (λ w → ⟨ x ∈ w ⟩) (sym (pair-singleton a)) h))

sgl-in : (a x : V ℓ) → x ≡ a → ⟨ x ∈ ⁅ a ⁆s ⟩
sgl-in a x e = subst (λ w → ⟨ x ∈ w ⟩) (pair-singleton a)
  (subst ⟨_⟩ (sym (pair-spec a a x)) ∣ inl e ∣₁)

cup-out : (A B x : V ℓ) → ⟨ x ∈ (A ∪ B) ⟩ → ∥ (⟨ x ∈ A ⟩ ⊎ ⟨ x ∈ B ⟩) ∥₁
cup-out A B x h = PT.rec squash₁
  (λ { (v , v∈ , x∈v) → PT.map
         (λ { (inl e) → inl (subst (λ w → ⟨ x ∈ w ⟩) e x∈v)
            ; (inr e) → inr (subst (λ w → ⟨ x ∈ w ⟩) e x∈v) })
         (subst ⟨_⟩ (pair-spec A B v) v∈) })
  (subst ⟨_⟩ (union-spec ⁅ A , B ⁆ x) h)

cup-inl : (A B x : V ℓ) → ⟨ x ∈ A ⟩ → ⟨ x ∈ (A ∪ B) ⟩
cup-inl A B x h = subst ⟨_⟩ (sym (union-spec ⁅ A , B ⁆ x))
  ∣ A , subst ⟨_⟩ (sym (pair-spec A B A)) ∣ inl refl ∣₁ , h ∣₁

cup-inr : (A B x : V ℓ) → ⟨ x ∈ B ⟩ → ⟨ x ∈ (A ∪ B) ⟩
cup-inr A B x h = subst ⟨_⟩ (sym (union-spec ⁅ A , B ⁆ x))
  ∣ B , subst ⟨_⟩ (sym (pair-spec A B B)) ∣ inr refl ∣₁ , h ∣₁

sglʟ : S → S
sglʟ a = pairʟ a a

sglʟ-fst : (a : S) → fst (sglʟ a) ≡ ⁅ fst a ⁆s
sglʟ-fst a = pairʟ-fst a a ∙ pair-singleton (fst a)

cupʟ : S → S → S
cupʟ a b = unionʟ (pairʟ a b)

cupʟ-fst : (a b : S) → fst (cupʟ a b) ≡ (fst a ∪ fst b)
cupʟ-fst a b = unionʟ-fst (pairʟ a b) ∙ cong (⋃_) (pairʟ-fst a b)

sglʟ-in : (a : S) (x : V ℓ) → x ≡ fst a → ⟨ x ∈ fst (sglʟ a) ⟩
sglʟ-in a x e = subst (λ w → ⟨ x ∈ w ⟩) (sym (sglʟ-fst a)) (sgl-in (fst a) x e)

sglʟ-out : (a : S) (x : V ℓ) → ⟨ x ∈ fst (sglʟ a) ⟩ → x ≡ fst a
sglʟ-out a x h = sgl-out (fst a) x (subst (λ w → ⟨ x ∈ w ⟩) (sglʟ-fst a) h)

cupʟ-inl : (a b : S) (x : V ℓ) → ⟨ x ∈ fst a ⟩ → ⟨ x ∈ fst (cupʟ a b) ⟩
cupʟ-inl a b x h = subst (λ w → ⟨ x ∈ w ⟩) (sym (cupʟ-fst a b))
  (cup-inl (fst a) (fst b) x h)

cupʟ-inr : (a b : S) (x : V ℓ) → ⟨ x ∈ fst b ⟩ → ⟨ x ∈ fst (cupʟ a b) ⟩
cupʟ-inr a b x h = subst (λ w → ⟨ x ∈ w ⟩) (sym (cupʟ-fst a b))
  (cup-inr (fst a) (fst b) x h)

cupʟ-out : (a b : S) (x : V ℓ) → ⟨ x ∈ fst (cupʟ a b) ⟩
         → ∥ (⟨ x ∈ fst a ⟩ ⊎ ⟨ x ∈ fst b ⟩) ∥₁
cupʟ-out a b x h = cup-out (fst a) (fst b) x
  (subst (λ w → ⟨ x ∈ w ⟩) (cupʟ-fst a b) h)

部分式上の再帰

tree f φ は φ の各部分式 χ に対する値 f χ を合併します。tree-inv は任意の要素を、それを供給した部分式によって記述し、Parts は順方向の包含を記録します。

英語原文

One recursion over the ten constructors, with what it collects left as its parameter. It gathers one thing per subformula: give it the key and it gives the subformula closure of the next section, give it an entry and it gives the satisfaction table of a later chapter. Both want the same inversion, so the inversion is proved here once and instantiated twice.

英語原文

Of says what a member of such a set is: one of the things gathered, gathered at some subformula whose own set sits inside the one it came from. tree-inv proves it, and Parts carries the memberships the other direction needs, one for each shape a clause of the recursion produces.

module _ {ℓ' : Level} {K : Type ℓ'} where

  tree : (∀ {m} → Formula K m → S) → ∀ {n} → Formula K n → S
  tree f φ@(t ∈̇ u)  = sglʟ (f φ)
  tree f φ@(t ≐ u)  = sglʟ (f φ)
  tree f φ@⊥̇        = sglʟ (f φ)
  tree f φ@(a ∧̇ b)  = cupʟ (sglʟ (f φ)) (cupʟ (tree f a) (tree f b))
  tree f φ@(a ∨̇ b)  = cupʟ (sglʟ (f φ)) (cupʟ (tree f a) (tree f b))
  tree f φ@(a ⇒̇ b)  = cupʟ (sglʟ (f φ)) (cupʟ (tree f a) (tree f b))
  tree f φ@(∃̇ a)    = cupʟ (sglʟ (f φ)) (tree f a)
  tree f φ@(∀̇ a)    = cupʟ (sglʟ (f φ)) (tree f a)
  tree f φ@(∀̇∈ t a) = cupʟ (sglʟ (f φ)) (tree f a)
  tree f φ@(∃̇∈ t a) = cupʟ (sglʟ (f φ)) (tree f a)

  Of : (f g : ∀ {m} → Formula K m → S) {n : ℕ} → Formula K n → V ℓ
     → Type (ℓ-max (ℓ-suc ℓ) ℓ')
  Of f g φ x = ∥ (Σ[ m ∈ ℕ ] Σ[ χ ∈ Formula K m ]
                   ((x ≡ fst (f χ))
                    × ((z : V ℓ) → ⟨ z ∈ fst (tree g χ) ⟩
                       → ⟨ z ∈ fst (tree g φ) ⟩))) ∥₁

  private
    module _ (f g : ∀ {m} → Formula K m → S) where
      one : ∀ {n} (φ : Formula K n) (x : V ℓ)
          → ⟨ x ∈ fst (sglʟ (f φ)) ⟩ → Of f g φ x
      one {n} φ x h = ∣ n , φ , sglʟ-out (f φ) x h , (λ _ hz → hz) ∣₁

      wider : ∀ {n m} (φ : Formula K n) (χ : Formula K m) {x : V ℓ}
            → ((z : V ℓ) → ⟨ z ∈ fst (tree g χ) ⟩ → ⟨ z ∈ fst (tree g φ) ⟩)
            → Of f g χ x → Of f g φ x
      wider _ _ s = PT.map
        (λ { (m , ψ , e , t) → m , ψ , e , (λ z hz → s z (t z hz)) })

      un : ∀ {n m} (φ : Formula K n) (a : Formula K m)
         → ((z : V ℓ) → ⟨ z ∈ fst (cupʟ (sglʟ (g φ)) (tree g a)) ⟩
            → ⟨ z ∈ fst (tree g φ) ⟩)
         → ((x : V ℓ) → ⟨ x ∈ fst (tree f a) ⟩ → Of f g a x)
         → (x : V ℓ) → ⟨ x ∈ fst (cupʟ (sglʟ (f φ)) (tree f a)) ⟩ → Of f g φ x
      un φ a into ra x h = PT.rec squash₁
        (λ { (inl e) → one φ x e
           ; (inr e) → wider φ a
               (λ z hz → into z (cupʟ-inr (sglʟ (g φ)) (tree g a) z hz))
               (ra x e) })
        (cupʟ-out (sglʟ (f φ)) (tree f a) x h)

      bin : ∀ {n m} (φ : Formula K n) (a b : Formula K m)
          → ((z : V ℓ)
             → ⟨ z ∈ fst (cupʟ (sglʟ (g φ)) (cupʟ (tree g a) (tree g b))) ⟩
             → ⟨ z ∈ fst (tree g φ) ⟩)
          → ((x : V ℓ) → ⟨ x ∈ fst (tree f a) ⟩ → Of f g a x)
          → ((x : V ℓ) → ⟨ x ∈ fst (tree f b) ⟩ → Of f g b x)
          → (x : V ℓ)
          → ⟨ x ∈ fst (cupʟ (sglʟ (f φ)) (cupʟ (tree f a) (tree f b))) ⟩
          → Of f g φ x
      bin φ a b into ra rb x h = PT.rec squash₁
        (λ { (inl e) → one φ x e
           ; (inr e) → PT.rec squash₁
               (λ { (inl ea) → wider φ a (λ z hz → into z
                      (cupʟ-inr (sglʟ (g φ)) (cupʟ (tree g a) (tree g b)) z
                        (cupʟ-inl (tree g a) (tree g b) z hz)))
                      (ra x ea)
                  ; (inr eb) → wider φ b (λ z hz → into z
                      (cupʟ-inr (sglʟ (g φ)) (cupʟ (tree g a) (tree g b)) z
                        (cupʟ-inr (tree g a) (tree g b) z hz)))
                      (rb x eb) })
               (cupʟ-out (tree f a) (tree f b) x e) })
        (cupʟ-out (sglʟ (f φ)) (cupʟ (tree f a) (tree f b)) x h)

  module Parts (f : ∀ {m} → Formula K m → S) where
    self : ∀ {n} (φ : Formula K n) → ⟨ fst (f φ) ∈ fst (tree f φ) ⟩
    self φ@(t ∈̇ u)  = sglʟ-in (f φ) _ refl
    self φ@(t ≐ u)  = sglʟ-in (f φ) _ refl
    self φ@⊥̇        = sglʟ-in (f φ) _ refl
    self φ@(a ∧̇ b)  = cupʟ-inl _ _ _ (sglʟ-in (f φ) _ refl)
    self φ@(a ∨̇ b)  = cupʟ-inl _ _ _ (sglʟ-in (f φ) _ refl)
    self φ@(a ⇒̇ b)  = cupʟ-inl _ _ _ (sglʟ-in (f φ) _ refl)
    self φ@(∃̇ a)    = cupʟ-inl _ _ _ (sglʟ-in (f φ) _ refl)
    self φ@(∀̇ a)    = cupʟ-inl _ _ _ (sglʟ-in (f φ) _ refl)
    self φ@(∀̇∈ t a) = cupʟ-inl _ _ _ (sglʟ-in (f φ) _ refl)
    self φ@(∃̇∈ t a) = cupʟ-inl _ _ _ (sglʟ-in (f φ) _ refl)

    left : ∀ {n m} (χ : Formula K n) (a b : Formula K m) (z : V ℓ)
         → ⟨ z ∈ fst (tree f a) ⟩
         → ⟨ z ∈ fst (cupʟ (sglʟ (f χ)) (cupʟ (tree f a) (tree f b))) ⟩
    left χ a b z h = cupʟ-inr (sglʟ (f χ)) (cupʟ (tree f a) (tree f b)) z
                       (cupʟ-inl (tree f a) (tree f b) z h)

    right : ∀ {n m} (χ : Formula K n) (a b : Formula K m) (z : V ℓ)
          → ⟨ z ∈ fst (tree f b) ⟩
          → ⟨ z ∈ fst (cupʟ (sglʟ (f χ)) (cupʟ (tree f a) (tree f b))) ⟩
    right χ a b z h = cupʟ-inr (sglʟ (f χ)) (cupʟ (tree f a) (tree f b)) z
                        (cupʟ-inr (tree f a) (tree f b) z h)

    only : ∀ {n m} (χ : Formula K n) (a : Formula K m) (z : V ℓ)
         → ⟨ z ∈ fst (tree f a) ⟩
         → ⟨ z ∈ fst (cupʟ (sglʟ (f χ)) (tree f a)) ⟩
    only χ a z h = cupʟ-inr (sglʟ (f χ)) (tree f a) z h

  tree-inv : (f g : ∀ {m} → Formula K m → S)
           → ∀ {n} (φ : Formula K n) (x : V ℓ)
           → ⟨ x ∈ fst (tree f φ) ⟩ → Of f g φ x
  tree-inv f g φ@(t ∈̇ u) = one f g φ
  tree-inv f g φ@(t ≐ u) = one f g φ
  tree-inv f g φ@⊥̇       = one f g φ
  tree-inv f g φ@(a ∧̇ b) = bin f g φ a b (λ _ hz → hz)
                             (tree-inv f g a) (tree-inv f g b)
  tree-inv f g φ@(a ∨̇ b) = bin f g φ a b (λ _ hz → hz)
                             (tree-inv f g a) (tree-inv f g b)
  tree-inv f g φ@(a ⇒̇ b) = bin f g φ a b (λ _ hz → hz)
                             (tree-inv f g a) (tree-inv f g b)
  tree-inv f g φ@(∃̇ a)    = un f g φ a (λ _ hz → hz) (tree-inv f g a)
  tree-inv f g φ@(∀̇ a)    = un f g φ a (λ _ hz → hz) (tree-inv f g a)
  tree-inv f g φ@(∀̇∈ t a) = un f g φ a (λ _ hz → hz) (tree-inv f g a)
  tree-inv f g φ@(∃̇∈ t a) = un f g φ a (λ _ hz → hz) (tree-inv f g a)

部分式閉包

一般の木を論理式の鍵に特殊化して closure φ を得ます。これは φ の鍵と全部分式の鍵を含む構成可能集合であり、各構成子について明示的な要素写像を備えます。

英語原文

A recursion on codes is stated against a slot: a set of codes closed under immediate subcodes, holding the one the recursion is asked about. The smallest such slot is the set of codes of a formula's own subformulas, and it is the recursion above taken at the key.

英語原文

Each entry carries its arity, because the recursion's own key does; a binder's subformula therefore enters at the successor. This is the only place where a change of arity appears explicitly, and it appears there because the arity is exactly what the frames bind.

英語原文

Constructibility is not a second proof. The recursion above runs on the model's own sets, so the certificate comes out of it together with the set.

module _ {K : Type ℓ} (f : K → V ℓ) (h : (k : K) → ⟨ isL (f k) ⟩) where

  key : ∀ {n} → Formula K n → V ℓ
  key {n} φ = pr (# n) VCode.⌜ mapFo f φ ⌝

  keyL : ∀ {n} (φ : Formula K n) → ⟨ isL (key φ) ⟩
  keyL φ = prL (numL _) (codeL f h φ)

  private
    keyS : ∀ {m} → Formula K m → S
    keyS φ = key φ , keyL φ

  closure : ∀ {n} → Formula K n → V ℓ
  closure φ = fst (tree keyS φ)

  closureL : ∀ {n} (φ : Formula K n) → ⟨ isL (closure φ) ⟩
  closureL φ = snd (tree keyS φ)

まとめ

以上により、構文コード、環境、部分式で添字づけられた集まりが L に入ります。残る補題は閉包の要素を具体的な部分式の鍵へ戻し、後の有界再帰に備えます。

英語原文

codeL says every code is an element of L, and numL, prL and tagL are the three shapes it is built from. With it a code may be named as a constant of the model's object language, and a family of codes may be the domain of an internalized recursion.

英語原文

envL then puts an environment in L with no recursion on its length and no use of replacement, because an environment is on the nose the finite set of its entries. closure is the smallest slot a recursion on a code can be stated against, and closureL reads its certificate off the recursion that built it rather than proving it a second time.

英語原文

The set of all codes is still not an element of L, and is still not needed.

閉包の要素を読み戻す

closure-inv は一般の木の反転を適用し、closure φ の各要素が、閉包から φ の閉包への包含をもつある部分式の鍵であることを示します。

英語原文

A recursion over codes has to know what the elements of its domain are, and "whatever the union of these singletons happens to contain" is not an answer. The lemma below is the answer: every element of a closure is the key of a formula, and that formula's own closure sits inside the one it came from. The second half is what an induction consumes, since it is how the induction knows its hypothesis is available where it wants to apply it.

英語原文

It and the membership of a key in its own closure are the recursion above read at the key, so neither is an induction here.

  Inv : ∀ {n} → Formula K n → V ℓ → Type (ℓ-suc ℓ)
  Inv φ x = Of keyS keyS φ x

  closure-inv : ∀ {n} (φ : Formula K n) (x : V ℓ)
              → ⟨ x ∈ closure φ ⟩ → Inv φ x
  closure-inv φ x hx = tree-inv keyS keyS φ x hx

  key∈closure : ∀ {n} (φ : Formula K n) → ⟨ key φ ∈ closure φ ⟩
  key∈closure φ = Parts.self keyS φ

論理式の鍵から論理式を復元する

ある集合が論理式の鍵に等しいと分かっているとき、最後の補題はその証拠を明示的な論理式へ移し、その閉包から元の閉包への包含も保ちます。

英語原文

The demand a closedness predicate makes is indexed by a constructor tag, and the formula it is made of is indexed by a constructor. Matching the two is the only real work in the first instance, and doing it clause by clause would be ten formulas times seven demands. It is not, because the demand can be computed from the tag: one type family over the tag, one function over the formula, and the equation between tags that the key's injectivity yields carries the second to the first.

英語原文

Below the tag, a key is an arity paired with a code, and both layers are pinned by pairing's injectivity. What comes out is that an arity-preserving constructor demands its components at the arity read, an arity-raising one demands them at the successor, and a constructor with no subformula demands nothing.

  module _ (C : V ℓ) where
    BothSame : V ℓ → V ℓ → Type (ℓ-suc ℓ)
    BothSame ar p = (u v : V ℓ) → p ≡ pr u v
                  → ⟨ pr ar u ∈ C ⟩ × ⟨ pr ar v ∈ C ⟩

    SecondSucc : V ℓ → V ℓ → Type (ℓ-suc ℓ)
    SecondSucc ar p = (u v : V ℓ) → p ≡ pr u v → ⟨ pr (sucV ar) v ∈ C ⟩

    Concl : ℕ → V ℓ → V ℓ → Type (ℓ-suc ℓ)
    Concl 2  ar p = BothSame ar p
    Concl 3  ar p = BothSame ar p
    Concl 4  ar p = BothSame ar p
    Concl 6 ar p = ⟨ pr (sucV ar) p ∈ C ⟩
    Concl 7 ar p = ⟨ pr (sucV ar) p ∈ C ⟩
    Concl 8 ar p = SecondSucc ar p
    Concl 9 ar p = SecondSucc ar p
    Concl _  _  _ = Unit*

    private
      Below : ∀ {n} → Formula K n → Type (ℓ-suc ℓ)
      Below φ = (z : V ℓ) → ⟨ z ∈ closure φ ⟩ → ⟨ z ∈ C ⟩

      inC : ∀ {n m} (φ : Formula K n) (a : Formula K m)
          → Below φ → ⟨ key a ∈ closure φ ⟩ → {w : V ℓ} → key a ≡ w → ⟨ w ∈ C ⟩
      inC φ a below mem q = subst (λ w → ⟨ w ∈ C ⟩) q (below (key a) mem)

      atTag : ∀ {m k : ℕ} {ar p : V ℓ} (j : ℕ) (q : V ℓ)
            → pr (# m) (VCode.mkTag j q) ≡ pr ar (pr (# k) p)
            → (j ≡ k) × ((# m ≡ ar) × (q ≡ p))
      atTag j q e = VCode.mkTag-inj (pr-inj e .snd) .fst
                  , (pr-inj e .fst , VCode.mkTag-inj (pr-inj e .snd) .snd)

      bothOf : ∀ {n m'} (φ' : Formula K n) (a b : Formula K m')
             → Below φ' → ⟨ key a ∈ closure φ' ⟩ → ⟨ key b ∈ closure φ' ⟩
             → (ar p : V ℓ) → # m' ≡ ar
             → pr VCode.⌜ mapFo f a ⌝ VCode.⌜ mapFo f b ⌝ ≡ p
             → BothSame ar p
      bothOf φ' a b below ma mb ar p qa qp u v qu =
          inC φ' a below ma (cong₂ pr qa (pr-inj (qp ∙ qu) .fst))
        , inC φ' b below mb (cong₂ pr qa (pr-inj (qp ∙ qu) .snd))

      oneOf : ∀ {n m'} (φ' : Formula K n) (a : Formula K m')
            → Below φ' → ⟨ key a ∈ closure φ' ⟩
            → (ar p : V ℓ) → # m' ≡ ar → VCode.⌜ mapFo f a ⌝ ≡ p
            → ⟨ pr ar p ∈ C ⟩
      oneOf φ' a below ma ar p qa qp = inC φ' a below ma (cong₂ pr qa qp)

      upOf : ∀ {n m'} (φ' : Formula K n) (a : Formula K (suc m'))
           → Below φ' → ⟨ key a ∈ closure φ' ⟩
           → (ar p : V ℓ) → # m' ≡ ar → VCode.⌜ mapFo f a ⌝ ≡ p
           → ⟨ pr (sucV ar) p ∈ C ⟩
      upOf φ' a below ma ar p qa qp =
        inC φ' a below ma (cong₂ pr (cong sucV qa) qp)

      sndUpOf : ∀ {n m'} (φ' : Formula K n) (t : Term K m')
                (a : Formula K (suc m'))
              → Below φ' → ⟨ key a ∈ closure φ' ⟩
              → (ar p : V ℓ) → # m' ≡ ar
              → pr VCode.⌜ mapTm f t ⌝ᵗ VCode.⌜ mapFo f a ⌝ ≡ p
              → SecondSucc ar p
      sndUpOf φ' t a below ma ar p qa qp u v qu =
        inC φ' a below ma (cong₂ pr (cong sucV qa) (pr-inj (qp ∙ qu) .snd))

      left : ∀ {n m'} (φ' : Formula K n) (a b : Formula K m')
           → ⟨ key a ∈ fst (cupʟ (sglʟ (keyS φ'))
                              (cupʟ (tree keyS a) (tree keyS b))) ⟩
      left φ' a b = Parts.left keyS φ' a b (key a) (key∈closure a)

      right : ∀ {n m'} (φ' : Formula K n) (a b : Formula K m')
            → ⟨ key b ∈ fst (cupʟ (sglʟ (keyS φ'))
                               (cupʟ (tree keyS a) (tree keyS b))) ⟩
      right φ' a b = Parts.right keyS φ' a b (key b) (key∈closure b)

      only : ∀ {n m'} (φ' : Formula K n) (a : Formula K m')
           → ⟨ key a ∈ fst (cupʟ (sglʟ (keyS φ')) (tree keyS a)) ⟩
      only φ' a = Parts.only keyS φ' a (key a) (key∈closure a)

    byTag : ∀ {m} (φ : Formula K m) (k : ℕ) (ar p : V ℓ)
          → Below φ → key φ ≡ pr ar (pr (# k) p) → Concl k ar p
    byTag (t ∈̇ u) k ar p below eq = subst (λ j → Concl j ar p)
      (atTag 0 (pr VCode.⌜ mapTm f t ⌝ᵗ VCode.⌜ mapTm f u ⌝ᵗ) eq .fst) tt*
    byTag (t ≐ u) k ar p below eq = subst (λ j → Concl j ar p)
      (atTag 1 (pr VCode.⌜ mapTm f t ⌝ᵗ VCode.⌜ mapTm f u ⌝ᵗ) eq .fst) tt*
    byTag ⊥̇ k ar p below eq = subst (λ j → Concl j ar p)
      (atTag 5 (# 0) eq .fst) tt*
    byTag φ@(a ∧̇ b) k ar p below eq =
      let r = atTag 2 (pr VCode.⌜ mapFo f a ⌝ VCode.⌜ mapFo f b ⌝) eq in
      subst (λ j → Concl j ar p) (r .fst)
        (bothOf φ a b below (left φ a b) (right φ a b) ar p
          (r .snd .fst) (r .snd .snd))
    byTag φ@(a ∨̇ b) k ar p below eq =
      let r = atTag 3 (pr VCode.⌜ mapFo f a ⌝ VCode.⌜ mapFo f b ⌝) eq in
      subst (λ j → Concl j ar p) (r .fst)
        (bothOf φ a b below (left φ a b) (right φ a b) ar p
          (r .snd .fst) (r .snd .snd))
    byTag φ@(a ⇒̇ b) k ar p below eq =
      let r = atTag 4 (pr VCode.⌜ mapFo f a ⌝ VCode.⌜ mapFo f b ⌝) eq in
      subst (λ j → Concl j ar p) (r .fst)
        (bothOf φ a b below (left φ a b) (right φ a b) ar p
          (r .snd .fst) (r .snd .snd))
    byTag φ@(∃̇ a) k ar p below eq =
      let r = atTag 6 VCode.⌜ mapFo f a ⌝ eq in
      subst (λ j → Concl j ar p) (r .fst)
        (upOf φ a below (only φ a) ar p (r .snd .fst) (r .snd .snd))
    byTag φ@(∀̇ a) k ar p below eq =
      let r = atTag 7 VCode.⌜ mapFo f a ⌝ eq in
      subst (λ j → Concl j ar p) (r .fst)
        (upOf φ a below (only φ a) ar p (r .snd .fst) (r .snd .snd))
    byTag φ@(∀̇∈ t a) k ar p below eq =
      let r = atTag 8 (pr VCode.⌜ mapTm f t ⌝ᵗ VCode.⌜ mapFo f a ⌝) eq in
      subst (λ j → Concl j ar p) (r .fst)
        (sndUpOf φ t a below (only φ a) ar p (r .snd .fst) (r .snd .snd))
    byTag φ@(∃̇∈ t a) k ar p below eq =
      let r = atTag 9 (pr VCode.⌜ mapTm f t ⌝ᵗ VCode.⌜ mapFo f a ⌝) eq in
      subst (λ j → Concl j ar p) (r .fst)
        (sndUpOf φ t a below (only φ a) ar p (r .snd .fst) (r .snd .snd))