---
title: "構成可能なコードと部分式の木"
module: L.Coding.CodeConstructibility
lang: ja
site: "Bedrock"
description: "構成可能なコードと部分式の木"
stage: "内部の符号化：式と定義域"
reading_order: 46
canonical: https://bedrock.institute/ja/L.Coding.CodeConstructibility.html
html: L.Coding.CodeConstructibility.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/Coding/CodeConstructibility.lagda.md
prerequisites: [Base.Prelude, FOL.ZFStructure, FOL.Syntax, FOL.Manipulation.ConstantMapping, V.Coding, L.Constructible, L.Coding.Model, L.Coding.Expressions, L.Axioms.Numerals, L.Coding.Environment, L.Axioms.Basic, V.Model]
routes: [internal-satisfaction, hulls-and-counting]
translations: [https://bedrock.institute/en/L.Coding.CodeConstructibility.md, https://bedrock.institute/zh/L.Coding.CodeConstructibility.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# 構成可能なコードと部分式の木
本章では項のコード、論理式のコード、有限環境のグラフが `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.
```agda
{-# 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.
```agda
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.
```agda
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.
```agda
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.
```agda
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.
```agda
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.
```agda
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.
```agda
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.
```agda
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))
```