BedrockThe closure is closed
对码的递归是相对于一个索引集陈述的，而索引集必须携带其每个成员的诸子码，否则诸子句什么也约束不了。对象语言把这一点说出来了；本章说的是「一条公式的闭包满足对象语言所说的那件事」，而那正是第一个实例要交付的假设。
证明短，因为它所需的两半本就是为了在此处会合而造的。闭包的元素是某条公式的键，而它自带一个坐落于内的闭包；一个给定构造子形状的键有已知的诸子键，而是哪几个由那个形状的标签算出。故八条子句里的每一条都是同样四步：把元素拆开、读出它的标签、问那个标签索取什么，再把该公式自己的闭包早已含有的东西交回去。
{-# OPTIONS --cubical --safe --guardedness #-} open import Base.Prelude open import Base.Truth module L.Coding.Closed {ℓ : Level} where open import FOL.ZFStructure using ( module hPropStructure ) open import FOL.Syntax using ( Term; Formula; _∈̇_; _≐_; _∧̇_; _∨̇_; _⇒̇_; ¬̇_; ⊤̇; ⊥̇; ∃̇_; ∀̇_; ∀̇∈; ∃̇∈ ) import FOL.Absoluteness open import V.Hierarchy {ℓ} using ( 𝒮ᵥ ) open import V.Coding {ℓ} using ( pr ) open import L.Constructible {ℓ} using ( 𝒮ʟ; isL; isL-trans ) open import L.Coding.Model {ℓ} using ( closedAt; binShapeAt; unShapeAt ; bothSameAt; oneSameAt; oneSuccAt; succSndAt ; binSameClosed-in; unSameClosed-in; unSuccClosed-in; binSuccClosed-in ; binSameClosed-out; unSameClosed-out; unSuccClosed-out ; binSuccClosed-out; numL ) open import L.Coding.InL {ℓ} using ( closure; closureL; closure-inv; byTag; Concl; key; keyL ; codeL; codeTmL; sgl-out; cup-out ) open import Cubical.Foundations.HLevels using ( isProp× ) import Cubical.HITs.PropositionalTruncation as PT open PT using ( ∥_∥₁ ) open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_ ) open import Cubical.HITs.CumulativeHierarchy.Constructions using ( ⁅_⁆s; _∪_; module InfinitySet ) open import Cubical.Data.Sum using ( inl; inr ) open import FOL.Manipulation.Relabelling using ( mapTm; mapFo ) open import V.Coding {ℓ} using ( module VCode ) open InfinitySet using ( #_; sucV ) open TruthAlgebra (hPropAlgebra (ℓ-suc ℓ)) open hPropStructure 𝒮ʟ using ( S ) module AbsL = FOL.Absoluteness.Single 𝒮ᵥ isL isL-trans open AbsL using ( _^_ ) renaming ( _⊨ᵐ_ to _⊨_ )
作为模型元素的闭包
两章之前，闭包还是层级的一个集合，另带一份可构造性证书。此处它是模型的一个元素，而对象语言的公式正是相对于这样的东西求值的。
module _ {K : Type ℓ} (f : K → V ℓ) (h : (k : K) → ⟨ isL (f k) ⟩) where private Cl : ∀ {n} → Formula K n → V ℓ Cl = closure f h clo : ∀ {n} → Formula K n → S clo φ = closure f h φ , closureL f h φ
证明真正用到的东西
下面那些子句从不看一条公式。每一条都取该集合的一个成员，问它是哪个键，再交回该集合早已持有的诸键；故任何一条所消费的、关于闭包的唯一一件事，就是「成员可剥开」：它仅仅是某条公式的键，而那条公式自己的闭包坐落于该集合之内。那就是 Peel，也正是当那个集合是一个闭包时 closure-inv 所返回的东西。
把它单独陈述出来不是为了整洁。后面有一章从一个阶段里切出一个码集，须为它证同一条封闭性，而那个集合不是任何东西的闭包；它手上有的是「其诸成员即诸键」这条刻画，而 Peel 正是一条刻画所化成的东西。故八条子句只证一次，对任何可剥开的集合成立，而闭包是那两个实例中的头一个，不是主角。
Peel : V ℓ → Type (ℓ-suc ℓ) Peel C = (x : V ℓ) → ⟨ x ∈ C ⟩ → ∥ (Σ[ m ∈ ℕ ] Σ[ ψ ∈ Formula K m ] ((x ≡ key f h ψ) × ((z : V ℓ) → ⟨ z ∈ Cl ψ ⟩ → ⟨ z ∈ C ⟩))) ∥₁
八条子句
每一条都是它那个框架的引入规则施于一个函数，而那个函数每次都是同样四步。形状相同的两条子句之间唯一变的是标签，而形状决定用四个读式中的哪一个。
剥开所返回的那个截断当场消掉，这是允许的，因为要产出的是一条隶属、或一对隶属，而隶属是命题。
module _ (D : S) (peel : Peel (fst D)) where private C : V ℓ C = fst D viaKey : (k : ℕ) (c : S) (ar p : V ℓ) → ⟨ fst c ∈ C ⟩ → fst c ≡ pr ar (pr (# k) p) → (T : Type (ℓ-suc ℓ)) → isProp T → (Concl f h C k ar p → T) → T viaKey k c ar p c∈ sh T pT g = PT.rec pT (λ { (m , ψ , q , incl) → g (byTag f h C ψ k ar p incl (sym q ∙ sh)) }) (peel (fst c) c∈) same : ∀ {m} (γ : S ^ m) (k : ℕ) → ((ar a b : V ℓ) → Concl f h C k ar (pr a b) → ⟨ pr ar a ∈ C ⟩ × ⟨ pr ar b ∈ C ⟩) → ⟨ (D ∷ γ) ⊨ binShapeAt zero k (bothSameAt zero) ⟩ same γ k use = binSameClosed-in zero k (D ∷ γ) (λ c ar a b c∈ sh → viaKey k c (fst ar) (pr (fst a) (fst b)) c∈ sh _ (isProp× (snd (pr (fst ar) (fst a) ∈ C)) (snd (pr (fst ar) (fst b) ∈ C))) (use (fst ar) (fst a) (fst b))) one : ∀ {m} (γ : S ^ m) (k : ℕ) → ((ar a : V ℓ) → Concl f h C k ar a → ⟨ pr ar a ∈ C ⟩) → ⟨ (D ∷ γ) ⊨ unShapeAt zero k (oneSameAt zero) ⟩ one γ k use = unSameClosed-in zero k (D ∷ γ) (λ c ar a c∈ sh → viaKey k c (fst ar) (fst a) c∈ sh _ (snd (pr (fst ar) (fst a) ∈ C)) (use (fst ar) (fst a))) up : ∀ {m} (γ : S ^ m) (k : ℕ) → ((ar a : V ℓ) → Concl f h C k ar a → ⟨ pr (sucV ar) a ∈ C ⟩) → ⟨ (D ∷ γ) ⊨ unShapeAt zero k (oneSuccAt zero) ⟩ up γ k use = unSuccClosed-in zero k (D ∷ γ) (λ c ar a c∈ sh → viaKey k c (fst ar) (fst a) c∈ sh _ (snd (pr (sucV (fst ar)) (fst a) ∈ C)) (use (fst ar) (fst a))) sndUp : ∀ {m} (γ : S ^ m) (k : ℕ) → ((ar a b : V ℓ) → Concl f h C k ar (pr a b) → ⟨ pr (sucV ar) b ∈ C ⟩) → ⟨ (D ∷ γ) ⊨ binShapeAt zero k (succSndAt zero) ⟩ sndUp γ k use = binSuccClosed-in zero k (D ∷ γ) (λ c ar a b c∈ sh → viaKey k c (fst ar) (pr (fst a) (fst b)) c∈ sh _ (snd (pr (sucV (fst ar)) (fst b) ∈ C)) (use (fst ar) (fst a) (fst b)))
那个合取
四种形状的八个实例，而唯一变动的参数是标签。交给每一个的那段后继说出那个标签处的要求是什么，而使这八条成其为八条的正是那个参数，不是形状。
closureClosed 于是就是落在闭包处的那个实例，而它的剥开就是原样的 closure-inv：两条陈述是同一个类型，因为 Peel 本就是照着那条引理的结论读出来的。
closedOf : ∀ {m} (γ : S ^ m) → ⟨ (D ∷ γ) ⊨ closedAt zero ⟩ closedOf γ = same γ 2 (λ _ a b r → r a b refl) , ( same γ 3 (λ _ a b r → r a b refl) , ( same γ 4 (λ _ a b r → r a b refl) , ( one γ 5 (λ _ _ r → r) , ( up γ 8 (λ _ _ r → r) , ( up γ 9 (λ _ _ r → r) , ( sndUp γ 10 (λ _ a b r → r a b refl) , sndUp γ 11 (λ _ a b r → r a b refl) )))))) closureClosed : ∀ {n m} (φ : Formula K n) (γ : S ^ m) → ⟨ (clo φ ∷ γ) ⊨ closedAt zero ⟩ closureClosed φ γ = closedOf (clo φ) (closure-inv f h φ) γ
小结
closedOf 是「对诸子码作递归」关于其索引集所需的那条假设，对任何可剥开的集合交付；closureClosed 是那条陈述落在闭包处。两者里都没有任何关于满足关系的东西：八条子句只说一个给定形状的键会拖进哪些键，而一个可剥开的集合恰好持有那些。
它的代价值得记下，因为满足关系那个实例要付的是同样的形状。四个读式、八行实例化、每个读式一条引理；内容在早一章的 byTag 里，那里把十二个构造子与八项要求一次性对上，而不是对上十二乘八次。byTag 本就是对着任意目标集写的，这正是此处的一般性免费的原因：闭包从来不是主角，只是头一个被递进来的东西。
闭包是最小的封闭集
封闭是实例想要的一半；最小是另一半，而正是它使那个取值唯一，且除公式之外不必对任何东西作归纳。一个含有某公式之键的封闭集，按该构造子所对应的那条子句，含有其诸子公式的键；再由归纳，含有它们的闭包。
每种情形从那个合取里读出属于自己标签的那条子句，把结果交给归纳假设。没有子公式的那四种无可读：它们的闭包是单元集，而假设已经就是结论。
private Key : ∀ {n} → Formula K n → V ℓ Key = key f h cd : ∀ {n} → Formula K n → S cd φ = VCode.⌜ mapFo f φ ⌝ , codeL f h φ ct : ∀ {n} → Term K n → S ct t = VCode.⌜ mapTm f t ⌝ᵗ , codeTmL f h t kk : ∀ {n} → Formula K n → S kk φ = Key φ , keyL f h φ nn : ℕ → S nn n = # n , numL n atKey : ∀ {m} (ψ' : Formula K m) (z : S) → ⟨ Key ψ' ∈ fst z ⟩ → (w : V ℓ) → ⟨ w ∈ ⁅ Key ψ' ⁆s ⟩ → ⟨ w ∈ fst z ⟩ atKey ψ' z k∈ w hw = subst (λ v → ⟨ v ∈ fst z ⟩) (sym (sgl-out (Key ψ') w hw)) k∈ sub : ∀ {m m'} (ψ' : Formula K m) (a : Formula K m') (z : S) → ⟨ Key ψ' ∈ fst z ⟩ → ((w : V ℓ) → ⟨ w ∈ Cl a ⟩ → ⟨ w ∈ fst z ⟩) → (w : V ℓ) → ⟨ w ∈ (⁅ Key ψ' ⁆s ∪ Cl a) ⟩ → ⟨ w ∈ fst z ⟩ sub ψ' a z k∈ ra w hw = PT.rec (snd (w ∈ fst z)) (λ { (inl e) → atKey ψ' z k∈ w e ; (inr e) → ra w e }) (cup-out ⁅ Key ψ' ⁆s (Cl a) w hw) two : ∀ {m m'} (ψ' : Formula K m) (a b : Formula K m') (z : S) → ⟨ Key ψ' ∈ fst z ⟩ → ((w : V ℓ) → ⟨ w ∈ Cl a ⟩ → ⟨ w ∈ fst z ⟩) → ((w : V ℓ) → ⟨ w ∈ Cl b ⟩ → ⟨ w ∈ fst z ⟩) → (w : V ℓ) → ⟨ w ∈ (⁅ Key ψ' ⁆s ∪ (Cl a ∪ Cl b)) ⟩ → ⟨ w ∈ fst z ⟩ two ψ' a b z k∈ ra rb w hw = PT.rec (snd (w ∈ fst z)) (λ { (inl e) → atKey ψ' z k∈ w e ; (inr e) → PT.rec (snd (w ∈ fst z)) (λ { (inl ea) → ra w ea ; (inr eb) → rb w eb }) (cup-out (Cl a) (Cl b) w e) }) (cup-out ⁅ Key ψ' ⁆s (Cl a ∪ Cl b) w hw) closureLeast : ∀ {n m} (ψ : Formula K n) (z : S) (γ : S ^ m) → ⟨ Key ψ ∈ fst z ⟩ → ⟨ (z ∷ γ) ⊨ closedAt zero ⟩ → (w : V ℓ) → ⟨ w ∈ Cl ψ ⟩ → ⟨ w ∈ fst z ⟩ closureLeast ψ@(t ∈̇ u) z γ k∈ cl = atKey ψ z k∈ closureLeast ψ@(t ≐ u) z γ k∈ cl = atKey ψ z k∈ closureLeast ψ@⊤̇ z γ k∈ cl = atKey ψ z k∈ closureLeast ψ@⊥̇ z γ k∈ cl = atKey ψ z k∈ closureLeast {n} ψ@(a ∧̇ b) z γ k∈ cl = two ψ a b z k∈ (closureLeast a z γ (r .fst) cl) (closureLeast b z γ (r .snd) cl) where r = binSameClosed-out zero 2 (z ∷ γ) (cl .fst) (kk ψ) (nn n) (cd a) (cd b) k∈ refl closureLeast {n} ψ@(a ∨̇ b) z γ k∈ cl = two ψ a b z k∈ (closureLeast a z γ (r .fst) cl) (closureLeast b z γ (r .snd) cl) where r = binSameClosed-out zero 3 (z ∷ γ) (cl .snd .fst) (kk ψ) (nn n) (cd a) (cd b) k∈ refl closureLeast {n} ψ@(a ⇒̇ b) z γ k∈ cl = two ψ a b z k∈ (closureLeast a z γ (r .fst) cl) (closureLeast b z γ (r .snd) cl) where r = binSameClosed-out zero 4 (z ∷ γ) (cl .snd .snd .fst) (kk ψ) (nn n) (cd a) (cd b) k∈ refl closureLeast {n} ψ@(¬̇ a) z γ k∈ cl = sub ψ a z k∈ (closureLeast a z γ r cl) where r = unSameClosed-out zero 5 (z ∷ γ) (cl .snd .snd .snd .fst) (kk ψ) (nn n) (cd a) k∈ refl closureLeast {n} ψ@(∃̇ a) z γ k∈ cl = sub ψ a z k∈ (closureLeast a z γ r cl) where r = unSuccClosed-out zero 8 (z ∷ γ) (cl .snd .snd .snd .snd .fst) (kk ψ) (nn n) (cd a) k∈ refl closureLeast {n} ψ@(∀̇ a) z γ k∈ cl = sub ψ a z k∈ (closureLeast a z γ r cl) where r = unSuccClosed-out zero 9 (z ∷ γ) (cl .snd .snd .snd .snd .snd .fst) (kk ψ) (nn n) (cd a) k∈ refl closureLeast {n} ψ@(∀̇∈ t a) z γ k∈ cl = sub ψ a z k∈ (closureLeast a z γ r cl) where r = binSuccClosed-out zero 10 (z ∷ []) (cl .snd .snd .snd .snd .snd .snd .fst) (kk ψ) (nn n) (ct t) (cd a) k∈ refl closureLeast {n} ψ@(∃̇∈ t a) z γ k∈ cl = sub ψ a z k∈ (closureLeast a z γ r cl) where r = binSuccClosed-out zero 11 (z ∷ []) (cl .snd .snd .snd .snd .snd .snd .snd) (kk ψ) (nn n) (ct t) (cd a) k∈ refl