---
title: "Closure under subformulas"
module: L.Coding.SubformulaClosure
lang: en
site: "Bedrock"
description: "Closure under subformulas"
stage: "Internal coding: expressions and domains"
reading_order: 47
canonical: https://bedrock.institute/en/L.Coding.SubformulaClosure.html
html: L.Coding.SubformulaClosure.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/Coding/SubformulaClosure.lagda.md
prerequisites: [Base.Prelude, FOL.ZFStructure, FOL.Syntax, FOL.Absoluteness, V.Hierarchy, V.Coding, L.Constructible, L.Coding.Closure, L.Coding.CodeConstructibility]
routes: [internal-satisfaction]
translations: [https://bedrock.institute/zh/L.Coding.SubformulaClosure.md, https://bedrock.institute/ja/L.Coding.SubformulaClosure.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# 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.

```agda
{-# 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.

```agda
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.

```agda
  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.

```agda
  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.

```agda
    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)
      , ( up γ 6 (λ _ _ r → r)
      , ( up γ 7 (λ _ _ r → r)
      , ( sndUp γ 8 (λ _ a b r → r a b refl)
      , sndUp γ 9 (λ _ 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.