Constant bounding

A formula is bounded by a predicate when every constant occurrence satisfies that predicate. These structural certificates support weakening along predicate implication and allow a partially defined constant map to relabel exactly the formulas on which it is defined.

This chapter is that certificate. BoundedFo P φ records, occurrence by occurrence, that every constant appearing in φ satisfies P. It is defined by the same case analysis as the formula it inspects, so it splits automatically under pattern matching, and no proof ever has to reason about a list of the constants of a formula. Being pure syntax, the chapter mentions neither hierarchies nor stages, and introduces no extra cost.

The companion is monotonicity. A certificate for a narrower predicate is one for a wider predicate, which is how certificates written against different stages are brought to a common stage before being used together.

Why should a formula come with a certificate about its constants? Consider a map on constants that is only partially defined: it sends a constant c to a new constant exactly when c satisfies some predicate P. Such a map cannot act on an arbitrary formula, because the formula might mention a constant outside its domain. But if we are handed, for each constant occurrence in the formula, a proof that this occurrence lies in the domain, then the map can act everywhere the formula needs it to. The question this chapter answers is: what is the right shape for that per-occurrence evidence, and what does it buy us?

{-# OPTIONS --cubical --safe --guardedness #-}

open import Base.Prelude

module FOL.Manipulation.ConstantBounding where

open import FOL.Syntax
  using ( Term; con; var; Formula; _∈̇_; _≐_; _∧̇_; _∨̇_; _⇒̇_; ⊥̇

The answer is a definition that follows the shape of the syntax itself. A term is either a constant, which must come with a proof of P, or a variable, which mentions no constant and so imposes no condition; a formula is built from these, and its certificate is assembled from the certificates of its parts. Because the certificate mirrors the constructor structure of Term K n and Formula K n, matching against it delivers exactly the domain proof at each constant occurrence. Two later uses shape the design: the monotonicity section transports certificates along an implication of predicates, and the relabelling section feeds them to the partial map; the Δ₀ constructors are imported so the relabelled formula can keep its Lévy-hierarchy witness, and the unit type supplies the trivial certificate carried by anything with no constants.

        ; ∃̇_; ∀̇_; ∀̇∈; ∃̇∈ )
open import FOL.LevyHierarchy
  using ( Δ₀; δ-∈; δ-≐; δ-∧; δ-∨; δ-⇒; δ-⊥; δ-∀∈; δ-∃∈ )
open import FOL.Manipulation.ConstantMapping using ( mapTm; mapFo )

open import Cubical.Data.Unit using ( Unit )

The certificate

BoundedTm P and BoundedFo P mirror the syntax: constants carry proofs of P, variables carry trivial data, and compound formulas pair the certificates of their parts. Pattern matching therefore exposes precisely the evidence needed at each constant occurrence.

Start with terms, where the condition is simplest. Take a predicate P on constants and a term such as c ∈̇ var i built from a constant c and a variable. The certificate BoundedTm P t is defined by recursion on t: for con c it is P c itself, the domain proof at that occurrence, while for var i it is Lift Unit, the unit type raised to the level of P c so that both cases have type Type ℓp. A variable asks for nothing; its trivial certificate simply fills the slot.

BoundedTm : ∀ {ℓk ℓp} {K : Type ℓk} (P : K → Type ℓp) {n} → Term K n → Type ℓp
BoundedTm P (con c) = P c
BoundedTm P (var i) = Lift Unit

BoundedFo : ∀ {ℓk ℓp} {K : Type ℓk} (P : K → Type ℓp) {n} → Formula K n → Type ℓp
BoundedFo P (t ∈̇ u)  = BoundedTm P t × BoundedTm P u

The recursion pattern is uniform: whenever a constructor has term or formula arguments, its certificate is the product of theirs; whenever a constructor mentions no constant, its certificate is trivial. For example, in (c ∈̇ d) ∧̇ ∃̇ (var 0 ≐ c) with two occurrences of the constant c, the certificate is a fourfold pairing that ends in two copies of the proof P c: one per occurrence, in the position where the occurrence sits. In contrast, ⊥̇ and bare variables carry nothing but Lift Unit. So the certificate follows occurrences, not the constant symbols abstractly: the same constant occurring twice contributes two proofs.

BoundedFo P (t ≐ u)  = BoundedTm P t × BoundedTm P u
BoundedFo P (φ ∧̇ ψ)  = BoundedFo P φ × BoundedFo P ψ
BoundedFo P (φ ∨̇ ψ)  = BoundedFo P φ × BoundedFo P ψ
BoundedFo P (φ ⇒̇ ψ)  = BoundedFo P φ × BoundedFo P ψ
BoundedFo P ⊥̇        = Lift Unit

Quantifiers bind variables and therefore leave constants untouched, so the unbounded forms pass their body's certificate through unchanged. A bounded quantifier, however, carries a bounding term that may mention constants: for ∀̇∈ t φ the certificate pairs the term certificate for t with the formula certificate for φ, exactly as our example formula ∃̇ (var 0 ≐ c) shows, where the outer body's certificate is just the certificate of var 0 ≐ c. These clauses exhaust the constructors of Formula K n, and each clause is read off the shape of the formula rather than computed by searching it.

BoundedFo P (∃̇ φ)    = BoundedFo P φ
BoundedFo P (∀̇ φ)    = BoundedFo P φ
BoundedFo P (∀̇∈ t φ) = BoundedTm P t × BoundedFo P φ
BoundedFo P (∃̇∈ t φ) = BoundedTm P t × BoundedFo P φ

Monotonicity

If P implies Q, every P-bounded term or formula is also Q-bounded. The proof follows the certificate structure and later lets bounds established at smaller stages be reused at larger stages.

Certificates are only useful if they can be moved between predicates. Think of a predicate as restricting which constants are allowed: widening P to Q along a pointwise implication P⊆Q cannot invalidate any certificate, since every occurrence accepted by P is still accepted by Q. For a single constant this is one application: P⊆Q c turns the proof P c into Q c. BoundedTm-mono extends this to whole terms by recursion: the constant case performs that single application, and the variable case passes through, since Lift Unit is inhabited regardless of the predicate.

module _ {ℓk ℓp ℓq} {K : Type ℓk} {P : K → Type ℓp} {Q : K → Type ℓq}
         (P⊆Q : (c : K) → P c → Q c) where

  BoundedTm-mono : ∀ {n} (t : Term K n) → BoundedTm P t → BoundedTm Q t
  BoundedTm-mono (con c) p = P⊆Q c p
  BoundedTm-mono (var i) _ = _

The same argument lifts to formulas through their certificates' products. For our example (c ∈̇ d) ∧̇ ∃̇ (var 0 ≐ c), a P-certificate is four proofs against P; applying BoundedTm-mono to each term slot and the recursion to each subformula turns them into four proofs against Q, and the formula's shape never changes.

  BoundedFo-mono : ∀ {n} (φ : Formula K n) → BoundedFo P φ → BoundedFo Q φ
  BoundedFo-mono (t ∈̇ u)  (ht , hu) = BoundedTm-mono t ht , BoundedTm-mono u hu
  BoundedFo-mono (t ≐ u)  (ht , hu) = BoundedTm-mono t ht , BoundedTm-mono u hu
  BoundedFo-mono (φ ∧̇ ψ)  (hφ , hψ) = BoundedFo-mono φ hφ , BoundedFo-mono ψ hψ
  BoundedFo-mono (φ ∨̇ ψ)  (hφ , hψ) = BoundedFo-mono φ hφ , BoundedFo-mono ψ hψ

Nothing about this conversion is special to any connective: the atomic and propositional cases each split the certificate into its two factors, convert the factors, and re-pair them, while ⊥̇ needs only the trivial inhabitant. Conjunction, disjunction and implication are three spellings of one step.

  BoundedFo-mono (φ ⇒̇ ψ)  (hφ , hψ) = BoundedFo-mono φ hφ , BoundedFo-mono ψ hψ
  BoundedFo-mono ⊥̇        _         = _
  BoundedFo-mono (∃̇ φ)    hφ        = BoundedFo-mono φ hφ

The quantifier cases finish the induction. Under ∃̇ or ∀̇ the body is converted recursively; under a bounded quantifier the bounding term's certificate is converted too, since the term may hold constants of its own. The result: widening the predicate widens every certificate, which is what lets bounds proved at one stage be quoted at another.

  BoundedFo-mono (∀̇ φ)    hφ        = BoundedFo-mono φ hφ
  BoundedFo-mono (∀̇∈ t φ) (ht , hφ) = BoundedTm-mono t ht , BoundedFo-mono φ hφ
  BoundedFo-mono (∃̇∈ t φ) (ht , hφ) = BoundedTm-mono t ht , BoundedFo-mono φ hφ

Relabelling, partially

A partial map can relabel a bounded formula because its certificate supplies the domain proof at every constant occurrence. The resulting formula agrees after both source and target are mapped into a common type, and its Lévy witness is preserved.

The interface is stated in the generality its user needs. Two domains, a common world they both map into, a predicate on the source, a partial map defined under it, and the equation saying the partial map agrees with the two projections. In the intended instance the source is the model's carrier, the target is a stage's member type, the world is the hierarchy, and the equation is the fact that a member of a stage, viewed as a set, is the set it was.

Now the certificate meets its consumer. A partial constant map is given by a domain predicate P on a source set K of constants and an assignment down defined only on P. To relabel a whole formula we also need a target set K' of constants and a world W into which both K and K' map. The mathematical condition on this data is a commuting triangle: each source constant c with p : P c lands, via down and then the target's map, on the same world element as c itself reaches by the source's map. When such a triangle is supplied, the relabelling it induces can be checked to agree with the original after both are read in W.

module Relabel
  {ℓk ℓk' ℓv ℓp : Level}
  {K  : Type ℓk}
  {K' : Type ℓk'}
  {W  : Type ℓv}

The triangle appears here as the parameter down-correct: for every c and p : P c, the path up (down c p) ≡ proj c. This is the only correctness obligation on the data; everything else about the relabelling will follow from it occurrence by occurrence. Note that down needs the proof p as an argument: the certificate is what makes the partial map applicable, supplying its domain condition exactly where the formula mentions a constant.

  (proj : K → W)
  (up   : K' → W)
  (P    : K → Type ℓp)
  (down : (c : K) → P c → K')
  (down-correct : (c : K) (p : P c) → up (down c p) ≡ proj c)

Relabelling a term now just threads the certificate through. liftTm takes t together with h : BoundedTm P t; matching h at the constant node hands over precisely the proof p : P c that down c requires, so the node becomes con (down c p). At a variable, h is trivial and the node passes through. The partial map has become total, but only on terms that present their domain proofs.

  where

  liftTm : ∀ {n} (t : Term K n) → BoundedTm P t → Term K' n
  liftTm (con c) p = con (down c p)
  liftTm (var i) _ = var i

  liftFo : ∀ {n} (φ : Formula K n) → BoundedFo P φ → Formula K' n

For a formula, liftFo applies liftTm at the term slots and recurses elsewhere. In our running example, the two occurrences of c are replaced by down c at its two proofs, d likewise, and the bound variable structure is untouched: relabelling only rewrites constants, never de Bruijn indices, so the free-variable count stays n.

  liftFo (t ∈̇ u)  (ht , hu) = liftTm t ht ∈̇ liftTm u hu
  liftFo (t ≐ u)  (ht , hu) = liftTm t ht ≐ liftTm u hu
  liftFo (φ ∧̇ ψ)  (hφ , hψ) = liftFo φ hφ ∧̇ liftFo ψ hψ
  liftFo (φ ∨̇ ψ)  (hφ , hψ) = liftFo φ hφ ∨̇ liftFo ψ hψ
  liftFo (φ ⇒̇ ψ)  (hφ , hψ) = liftFo φ hφ ⇒̇ liftFo ψ hψ

The bounded quantifiers repeat the same two-part shape, relabelling their bounding term and recursing into their body, while ⊥̇ and the unbounded quantifiers contribute no constants to relabel. So liftFo φ h is always defined for a certified formula, and the agreement theorem of the next section says precisely in what sense it is the same formula as φ.

  liftFo ⊥̇        _         = ⊥̇
  liftFo (∃̇ φ)    hφ        = ∃̇ liftFo φ hφ
  liftFo (∀̇ φ)    hφ        = ∀̇ liftFo φ hφ
  liftFo (∀̇∈ t φ) (ht , hφ) = ∀̇∈ (liftTm t ht) (liftFo φ hφ)
  liftFo (∃̇∈ t φ) (ht , hφ) = ∃̇∈ (liftTm t ht) (liftFo φ hφ)

Correctness says the relabelling changed nothing that matters: pushing the result into the common world W along up gives the same formula as pushing the original along proj. That is the equation at which the two branches of an absoluteness argument meet, and it holds occurrence by occurrence for exactly the reason the interface down-correct demanded. The Δ₀ witness survives as well: the certificate records quantifier structure only, so it transfers unchanged under a relabelling of constants.

Two facts close the story of the triangle. First, relabelling the lifted term into the common constant domain W along up yields the same term as relabelling the original along proj; second, relabelling preserves the Δ₀ certificate, since it changes constants but no quantifier structure. The base case is a term. For the constant con c, the certificate provides p : P c, and the desired path is just the triangle's edge down-correct c p placed under cong con. For var i both sides compute to mapTm _ (var i) applied to the same variable, so the path is refl.

  liftTm-correct : ∀ {n} (t : Term K n) (h : BoundedTm P t)
                 → mapTm up (liftTm t h) ≡ mapTm proj t
  liftTm-correct (con c) p = cong con (down-correct c p)
  liftTm-correct (var i) _ = refl

  liftFo-correct : ∀ {n} (φ : Formula K n) (h : BoundedFo P φ)

The formula-level statement compares the two composites mapFo up ∘ liftFo and mapFo proj applied to φ. An atomic formula such as t ∈̇ u already shows the mechanism: the goal splits into the two term goals for t and u, which the base case supplies, and cong₂ _∈̇_ places them under the membership symbol.

                 → mapFo up (liftFo φ h) ≡ mapFo proj φ
  liftFo-correct (t ∈̇ u) (ht , hu) =
    cong₂ _∈̇_ (liftTm-correct t ht) (liftTm-correct u hu)
  liftFo-correct (t ≐ u) (ht , hu) =
    cong₂ _≐_ (liftTm-correct t ht) (liftTm-correct u hu)

Compound formulas add nothing new: each binary connective case applies cong₂ to the symbol and the two recursive paths from the subformulas. The induction simply follows the certificate's own pairing structure, which is why the certificate was designed to mirror the syntax.

  liftFo-correct (φ ∧̇ ψ) (hφ , hψ) =
    cong₂ _∧̇_ (liftFo-correct φ hφ) (liftFo-correct ψ hψ)
  liftFo-correct (φ ∨̇ ψ) (hφ , hψ) =
    cong₂ _∨̇_ (liftFo-correct φ hφ) (liftFo-correct ψ hψ)
  liftFo-correct (φ ⇒̇ ψ) (hφ , hψ) =

Constant-free forms are even easier. ⊥̇ maps to itself on both routes, giving refl; the unbounded quantifier cases each wrap one recursive path in cong on the quantifier symbol, since a prefix introduces no constants.

    cong₂ _⇒̇_ (liftFo-correct φ hφ) (liftFo-correct ψ hψ)
  liftFo-correct ⊥̇ _ = refl
  liftFo-correct (∃̇ φ) hφ = cong ∃̇_ (liftFo-correct φ hφ)
  liftFo-correct (∀̇ φ) hφ = cong ∀̇_ (liftFo-correct φ hφ)
  liftFo-correct (∀̇∈ t φ) (ht , hφ) =

A bounded quantifier combines the two kinds of case: its term path and its body path are joined by cong₂ under the quantifier constructor, completing the induction. The declaration Δ₀-liftFo then turns to the second promised fact. Its statement is a transfer: given a boundedness certificate h for φ and a Δ₀ witness for φ, it returns a Δ₀ witness for liftFo φ h. The base case is the atomic witness δ-∈, which carries no data and survives untouched.

    cong₂ ∀̇∈ (liftTm-correct t ht) (liftFo-correct φ hφ)
  liftFo-correct (∃̇∈ t φ) (ht , hφ) =
    cong₂ ∃̇∈ (liftTm-correct t ht) (liftFo-correct φ hφ)

  Δ₀-liftFo : ∀ {n} {φ : Formula K n} (h : BoundedFo P φ) → Δ₀ φ → Δ₀ (liftFo φ h)
  Δ₀-liftFo (ht , hu) δ-∈       = δ-∈

The recursion runs over the Δ₀ witness, not the formula; the certificate is split only to reach the sub-certificates paired with each sub-witness. Connectives rebuild their constructor from the transferred sub-witnesses, and falsity returns δ-⊥ directly.

  Δ₀-liftFo (ht , hu) δ-≐       = δ-≐
  Δ₀-liftFo (hφ , hψ) (δ-∧ c d) = δ-∧ (Δ₀-liftFo hφ c) (Δ₀-liftFo hψ d)
  Δ₀-liftFo (hφ , hψ) (δ-∨ c d) = δ-∨ (Δ₀-liftFo hφ c) (Δ₀-liftFo hψ d)
  Δ₀-liftFo (hφ , hψ) (δ-⇒ c d) = δ-⇒ (Δ₀-liftFo hφ c) (Δ₀-liftFo hψ d)
  Δ₀-liftFo _         δ-⊥       = δ-⊥

The bounded quantifier witnesses finish the recursion: each wraps one transferred sub-witness in δ-∀∈ or δ-∃∈. Since every Δ₀ constructor has been handled, the transfer is total, and a formula's Δ₀ status is untouched by relabelling its constants.

  Δ₀-liftFo (ht , hφ) (δ-∀∈ c)  = δ-∀∈ (Δ₀-liftFo hφ c)
  Δ₀-liftFo (ht , hφ) (δ-∃∈ c)  = δ-∃∈ (Δ₀-liftFo hφ c)

Recap

Constant-bounded syntax packages the evidence needed by a partial constant map. Monotonicity transports that evidence along a pointwise implication of predicates. The functions liftTm and liftFo, their agreement lemmas, and Δ₀-liftFo then carry out certified constant relabelling while preserving the displayed syntax-level properties.