Closure under subformulas

A recursion over formula codes needs an index set containing the immediate subformula keys required by each constructor. This chapter proves the seven object-language closure conditions first for any set with the Peel property, then for the actual subformula closure of a formula.

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 seven 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

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

open import FOL.ZFStructure using ( module hPropStructure )
open import FOL.Syntax using ( 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.Closure {ℓ} using ( closedAt; binShapeAt; unShapeAt; bothSameAt; oneSameAt; oneSuccAt; succSndAt; binSameClosed-in; unSameClosed-in; unSuccClosed-in; binSuccClosed-in )
open import L.Coding.CodeConstructibility {ℓ}
  using ( closure; closureL; closure-inv; byTag; Concl; key )

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 ( module InfinitySet )
open InfinitySet using ( #_; sucV )

open hPropStructure 𝒮ʟ using ( S )

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

The closure as a model element

clo φ packages the externally constructed set closure f h φ with its constructibility proof, making it an element of L against which closedAt can be evaluated.

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 φ

Recovering subformula keys

Peel C says that every member of C is the key of a formula whose own closure is contained in C. This is exactly the information needed to recover the immediate subformula keys demanded by a constructor tag.

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 seven 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 seven closure conditions

The helpers same, one, up, and sndUp turn a peeled formula key into the subkeys required by binary, unary, arity-raising, and bounded-quantifier constructors. Their seven tag instances prove the seven closure conditions.

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)))

Combining the closure conditions

closedOf combines the seven tag instances into the conjunction closedAt for any model element whose underlying set satisfies Peel; closureClosed supplies closure-inv to obtain the result for clo φ.

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 γ  (λ _ a b r → r a b refl)
      , ( same γ  (λ _ a b r → r a b refl)
      , ( same γ  (λ _ a b r → r a b refl)
      , ( up γ  (λ _ _ r → r)
      , ( up γ  (λ _ _ r → r)
      , ( sndUp γ  (λ _ a b r → r a b refl)
      , sndUp γ  (λ _ 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 seven clauses say only which keys a key of a given shape brings 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, seven lines of instantiation, and one lemma per reader; the content is in byTag one chapter earlier, where the ten constructors were matched against the seven demands once and for all rather than ten times seven. 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.