BedrockThe closure is closed
A recursion over codes is stated against an index set, and the index set has to carry the subcodes of everything in it or the clauses constrain nothing. The object language says so; this chapter says that the closure of a formula satisfies what the object language says, which is the hypothesis the first instance will discharge.
The proof is short because the two halves it needs were built to meet here. An element of the closure is the key of a formula, and it brings a closure of its own that sits inside; a key of a given constructor shape has known subkeys, and which ones is computed from the shape's tag. So each of the eight clauses is the same four moves: take the element apart, read its tag, ask what that tag demands, and hand back what the formula's own closure already contains.
{-# 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 _⊨_ )
The closure, as an element of the model
Two chapters ago the closure was a set of the hierarchy carrying a constructibility certificate. Here it is one element of the model, which is what an object-language formula can be evaluated against.
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 φ
What the proof actually uses
The clauses below never look at a formula. Each of them takes a member of the set, asks which key it is, and hands back keys that the set already holds, so the only thing about the closure that any of them consumes is that a member peels: that it is merely the key of some formula whose own closure sits inside the set. That is Peel, and it is exactly what closure-inv returns when the set is a closure.
Stating it separately is not tidiness. A later chapter cuts a set of codes out of a stage and has to prove the same closedness for it, and that set is not a closure of anything; what it has instead is a characterization of its members as keys, and Peel is what a characterization turns into. So the eight clauses are proved once, for any set that peels, and the closure is the first of the two instances rather than the subject.
Peel : V ℓ → Type (ℓ-suc ℓ) Peel C = (x : V ℓ) → ⟨ x ∈ C ⟩ → ∥ (Σ[ m ∈ ℕ ] Σ[ ψ ∈ Formula K m ] ((x ≡ key f h ψ) × ((z : V ℓ) → ⟨ z ∈ Cl ψ ⟩ → ⟨ z ∈ C ⟩))) ∥₁
The eight clauses
Each is the introduction rule of its frame applied to one function, and that function is the same four moves every time. The tag is the only thing that changes between two clauses of the same shape, and the shape is what decides which of the four readers is used.
The truncation that peeling returns is eliminated straight away, which is allowed because what is being produced is a membership, or a pair of them, and membership is a proposition.
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)))
The conjunction
Eight instances of four shapes, and the tag is the only argument that moves. The continuation handed to each says what the demand at that tag is, and it is that argument, not the shape, that makes the eight eight.
closureClosed is then the instance at a closure, and its peeling is
closure-inv unchanged: the two statements are the same type, because
Peel was read off that lemma's conclusion.
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 φ) γ
Recap
closedOf is the hypothesis a recursion over subcodes needs about its index set, discharged for any set that peels; closureClosed is that statement at a closure. Nothing in either is about satisfaction: the eight clauses say only which keys a key of a given shape drags in, and a set that peels holds exactly those.
What it cost is worth recording, because the same shape is what the satisfaction instance will pay. Four readers, eight lines of instantiation, and one lemma per reader; the content is in byTag one chapter earlier, where the twelve constructors were matched against the eight demands once and for all rather than twelve times eight. byTag was already written against an arbitrary target set, which is why generality here is free: the closure was never the subject, only the first thing handed in.
The closure is the least closed set
Closed is half of what an instance wants; least is the other half, and it is what makes the value unique without an induction on anything but the formula. A closed set that contains a formula's key contains its subformulas' keys, by the clause the constructor answers to, and then by induction contains their closures.
Each case reads the clause for its own tag out of the conjunction and hands the result to the induction hypothesis. The four with no subformula have nothing to read: their closure is a singleton and the assumption is already the conclusion.
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