Parameter abstraction

A formula with constants can be converted into a parameter-free formula by replacing each constant occurrence with a fresh variable and recording the constants in a vector. Supplying that vector through the environment preserves satisfaction, which makes formulas with parameters available to later coding arguments.

This chapter builds the replacement itself. The occurrence count from FOL.Manipulation.ConstantOccurrences fixes how many new variables are needed, and a placement decides which variable slot each occurrence receives. The substitution runs in a single structural pass, and the adequacy theorem at the end identifies satisfaction before and after, which is what later coding of formulas will rely on.

Chapter introductions of formulas often need constants: to say that a set $a$ is definable from parameters, one writes a formula mentioning $a$ by name. For coding arguments, however, it is convenient to work with parameter-free formulas only. Parameter abstraction is the translation that makes this possible: replace each constant occurrence by a fresh variable, and record the constants in a vector that the environment will supply.

The replacement works occurrence by occurrence, not constant by constant. If the constant $c$ appears twice, it is recorded twice and receives two variables. Recording occurrences this way means the translation never has to decide whether two names are equal, so the alphabet K needs no decidable equality; the positional count from the chapter on constant occurrences does all the bookkeeping.

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

module FOL.Manipulation.ParameterAbstraction where

open import Base.Prelude
open import FOL.ZFStructure using ( ZFStructure )

Concretely, the translation consumes two pieces of data prepared in "Constants by occurrence": the number of constant occurrences, which fixes how many fresh variables are needed, and the recorded vector of constants, which fixes what those variables will stand for once interpreted. The replacement itself is described by a placement, a function deciding which variable slot each occurrence receives.

The whole construction is one structural pass over the formula. Its adequacy theorem, proved at the end of the chapter, identifies satisfaction of the original formula under a constant interpretation with satisfaction of the abstraction under the extended environment, and this identification is what later coding arguments rely on.

open import FOL.Syntax using
  ( Term; con; var
  ; Formula; _∈̇_; _≐_; _∧̇_; _∨̇_; _⇒̇_; ⊥̇; ∃̇_; ∀̇_; ∀̇∈; ∃̇∈ )
import FOL.Semantics
open import FOL.Manipulation.ConstantOccurrences using

Since every constant occurrence becomes a variable, the translated formula contains no constants at all: it lives over an alphabet with no inhabitants. The code uses the empty type ⊥* as that alphabet. No interpretation of it is ever demanded, because there is nothing to interpret; the type only has to exist so the translated syntax has a well-formed carrier.

  ( countTm; countFo; constantsTm; constantsFo; padRight; padLeft
  ; lookup-padRight; lookup-padLeft; lookup-map )
open import Cubical.Data.Nat using ( _+_ )
open import Cubical.Data.Vec using ( _++_; map )
import Cubical.Data.Empty as Empty

The abstraction

A placement assigns each constant occurrence a variable in a larger context. placeFo performs this replacement structurally, and absFo chooses the consecutive block after the original free variables, whose length is the occurrence count.

The traversal is stated for an arbitrary placement θ, and that generality is forced by the recursion: the placements used at a subformula are produced inside the traversal, so the induction hypothesis must be about all of them. Keeping θ abstract also keeps the proof of adequacy modular. This section builds the two traversals, over terms first and then formulas.

The general form of the replacement is a traversal that takes, besides the formula, a placement θ : Fin (countTm t) → Fin (n + k): it reads the occurrence slots of t in the order the counting chapter enumerates them, and for each one names a variable slot among the n + k available, of which n are the original free variables and k are the fresh parameter slots. The output is a term over the empty alphabet ⊥*, since no constant survives.

placeTm : ∀ {ℓz ℓc} {K : Type ℓc} {n k} (t : Term K n)
        → (Fin (countTm t) → Fin (n + k)) → Term (⊥* {ℓz}) (n + k)
placeTm         (con c) θ = var (θ zero)
placeTm {k = k} (var i) θ = var (padRight k i)

placeFo : ∀ {ℓz ℓc} {K : Type ℓc} {n k} (φ : Formula K n)

The term cases show the two moves. A constant con c has one occurrence, namely slot zero, and the placement says which variable replaces it: var (θ zero). A variable var i contributes no occurrence, so the placement is unused, but the context has grown from n to n + k and the old index must be re-embedded: padRight k sends i to the same slot among the first n, which by the pad law keeps its value in a concatenated environment.

        → (Fin (countFo φ) → Fin (n + k)) → Formula (⊥* {ℓz}) (n + k)
placeFo (t ∈̇ u)  θ = placeTm t (λ i → θ (padRight (countTm u) i))
                   ∈̇ placeTm u (λ j → θ (padLeft (countTm t) j))
placeFo (t ≐ u)  θ = placeTm t (λ i → θ (padRight (countTm u) i))
                   ≐ placeTm u (λ j → θ (padLeft (countTm t) j))

At a binary node the occurrence list splits, and the placement arithmetic appears. Consider the atom t ∈̇ u where t = con c and u = con d: the occurrence list is c ∷ d ∷ [], with c at index 0 and d at index 1. The left term must therefore read the placement through padRight, skipping past the countTm u slots that belong to u, while the right term reads it through padLeft, stepping over the countTm t slots that belong to t. Each subterm then sees a placement on its own occurrence slots, and the two translated subterms recombine with the original connective.

placeFo (φ ∧̇ ψ)  θ = placeFo φ (λ i → θ (padRight (countFo ψ) i))
                   ∧̇ placeFo ψ (λ j → θ (padLeft (countFo φ) j))
placeFo (φ ∨̇ ψ)  θ = placeFo φ (λ i → θ (padRight (countFo ψ) i))
                   ∨̇ placeFo ψ (λ j → θ (padLeft (countFo φ) j))
placeFo (φ ⇒̇ ψ)  θ = placeFo φ (λ i → θ (padRight (countFo ψ) i))

The formula traversal generalizes this example by structural recursion. Every two-part constructor, atom or propositional, splits its occurrence list in exactly this way: the first factor's occurrences precede the second's, so the left traversal composes θ with padRight past the right count and the right traversal with padLeft past the left count. Falsity ⊥̇ has no occurrences at all and translates to itself. No clause needs a second pass or a renaming lemma: composing the placements before recursing keeps the whole translation to one structural traversal.

                   ⇒̇ placeFo ψ (λ j → θ (padLeft (countFo φ) j))
placeFo ⊥̇        θ = ⊥̇
placeFo (∃̇ φ)    θ = ∃̇ placeFo φ (λ j → suc (θ j))
placeFo (∀̇ φ)    θ = ∀̇ placeFo φ (λ j → suc (θ j))
placeFo (∀̇∈ t φ) θ = ∀̇∈ (placeTm t (λ i → θ (padRight (countFo φ) i)))

Under a binder the context grows by one, and this is the second recurring move. In ∃̇∈ t φ, the bound variable is consed onto the left of the environment when the semantics evaluates the body, so every parameter slot shifts up by one: the body is traversed under the placement suc ∘ θ, adjusted further by padLeft past the term's occurrence, while the term itself is placed at the front by padRight past the body's occurrences. The unbounded quantifiers ∃̇ and ∀̇ carry only the shift, and with these clauses the traversal covers all ten formula constructors.

                        (placeFo φ (λ j → suc (θ (padLeft (countTm t) j))))
placeFo (∃̇∈ t φ) θ = ∃̇∈ (placeTm t (λ i → θ (padRight (countFo φ) i)))
                        (placeFo φ (λ j → suc (θ (padLeft (countTm t) j))))

The instance is the one the rest of the book will use: take the budget to be exactly the occurrence count and the placement to be the block that follows the variables. This is the required abstraction, and its type states the chapter's main result: a formula over K with n free variables becomes a parameter-free formula with n + countFo φ of them.

padLeft n is exactly the placement that sends occurrence j to slot n + j, so each recorded constant receives the first free slot after the original variables, in the order constantsFo φ lists them. Nothing else needs to be chosen.

The definition is a single call: absFo φ = placeFo φ (padLeft n). All the index arithmetic was already folded into the traversal, so the abstraction itself carries no cases of its own. Because the budget equals the count, the placement is a bijection between occurrence slots and parameter slots in effect, though the code never needs to say so.

absFo : ∀ {ℓz ℓc} {K : Type ℓc} {n} (φ : Formula K n) → Formula (⊥* {ℓz}) (n + countFo φ)
absFo {n = n} φ = placeFo φ (padLeft n)

Adequacy

Adequacy compares the original formula under a constant interpretation with its abstraction under an extended variable environment. When each placed variable contains the interpretation of its recorded constant, term denotation and formula satisfaction agree by structural induction.

The comparison is stated inside a structure 𝒮 with carrier S, under one interpretation ι : K → S of the original constants. Two semantic readings are set up side by side: _⊨_ and ⟦_⟧ for formulas and terms over K under ι, and their renamed copies _⊨₀_, ⟦_⟧₀ for the abstraction's constant domain ⊥*. The parameter-free side needs no genuine interpretation, since ⊥* is empty, but the semantics module requires the data, and Empty.rec* supplies it vacuously.

Adequacy is the statement that the abstraction does not change meaning. It compares two evaluations of the same formula: the original syntax over K with its constants interpreted by a map ι : K → S, against the translated syntax over the empty alphabet evaluated in the concatenated environment γ ++ σ, where γ holds the values of the original free variables and σ holds the interpretations of the recorded constants. Here S is the carrier of a proposition-valued structure 𝒮, and S ^ n is the type of environments of length n.

module _ {ℓ} (𝒮 : ZFStructure ℓ) where

  open ZFStructure 𝒮

  private module Sem = FOL.Semantics 𝒮
  open Sem using ( _^_ )

The comparison rests on a single hypothesis connecting the two sides: for every occurrence, the variable the placement named holds the interpretation of the constant recorded there, that is, lookup (θ j) (γ ++ σ) ≡ ι (lookup j (constantsFo φ)). All that follows is structural induction on the syntax with this hypothesis maintained. Since the translated syntax lives over the empty alphabet, its reading _⊨₀_ and ⟦_⟧₀ needs no genuine constant interpretation, though the semantics module requires one as data; the elimination of the empty type supplies it vacuously.

  module _ {ℓz ℓc} {K : Type ℓc} (ι : K → S) where

    open Sem.At K ι using ( _⊨_; ⟦_⟧ )
    open Sem.At (⊥* {ℓz}) Empty.rec* using ()
      renaming ( _⊨_ to _⊨₀_ ; ⟦_⟧ to ⟦_⟧₀ )

The statement is generic in the placement, and it has to be, because the recursion's placements are built at the recursive calls. It is stated at a variable environment γ and a variable parameter environment σ, constrained by one hypothesis: at every occurrence, the slot the placement names holds the interpretation of the constant the collection recorded there. That hypothesis is the whole content of "the constants are supplied in the environment", and stating it as a hypothesis rather than substituting a concrete environment is what keeps every clause from normalizing a vector.

Splitting the hypothesis is the only bookkeeping the two-part constructors need, and each half is one composition with a pad law.

The induction's invariant is the hypothesis h about the full occurrence vector, and the only new work is splitting it when a binary constructor divides that vector into a left part p and a right part q. Suppose h says that in γ ++ σ, slot θ j holds the interpretation of the j-th entry of p ++ q. The left operand needs this only for indices j below length p, and reading such an index through padRight past q recovers exactly the entry of p: lookup-padRight is that law. Composing it with h and then applying ι gives the left premise of the recursive call.

    private
      leftHalf : ∀ {n k a b} (θ : Fin (a + b) → Fin (n + k))
                 (γ : S ^ n) (σ : S ^ k) (p : Vec K a) (q : Vec K b)
               → (∀ j → lookup (θ j) (γ ++ σ) ≡ ι (lookup j (p ++ q)))
               → (∀ i → lookup (θ (padRight b i)) (γ ++ σ) ≡ ι (lookup i p))

The right half is the mirror image: indices of q are read through padLeft, which steps over exactly the a slots of p, and lookup-padLeft identifies the entry found in the concatenation with the entry of q. Note that a is an explicit argument of rightHalf while it was implicit in leftHalf: the placement's domain Fin (a + b) does not by itself determine a, whereas padLeft must be told precisely how many slots to step over.

      leftHalf θ γ σ p q h i = h (padRight _ i) ∙ cong ι (lookup-padRight p q i)

      rightHalf : ∀ {n k} a {b} (θ : Fin (a + b) → Fin (n + k))
                  (γ : S ^ n) (σ : S ^ k) (p : Vec K a) (q : Vec K b)
                → (∀ j → lookup (θ j) (γ ++ σ) ≡ ι (lookup j (p ++ q)))
                → (∀ j → lookup (θ (padLeft a j)) (γ ++ σ) ≡ ι (lookup j q))

With leftHalf and rightHalf in place, the splitting invariant is established once and for all. Every binary clause of the induction below restricts the joint hypothesis through one of these two lemmas, and no clause ever looks inside the concatenated environment again.

      rightHalf a θ γ σ p q h j = h (padLeft a j) ∙ cong ι (lookup-padLeft a p q j)

Terms first, two cases and both immediate. A constant's value is what the hypothesis says the slot holds; a variable's value is untouched, and the pad law finds it again in the extended environment.

The induction starts at terms, where the invariant already does all the work. The claim is that the value of t in γ under the interpretation ι equals the value of the translated term in γ ++ σ over the empty alphabet, whenever h fills the placed slots correctly. For a constant con c the translation is var (θ zero), whose value in γ ++ σ is lookup (θ zero) (γ ++ σ); the hypothesis h zero identifies it with ι c, which is exactly the claim, up to the direction in which the equation is stated.

    ⟦⟧-place : ∀ {n k} (t : Term K n) (θ : Fin (countTm t) → Fin (n + k))
               (γ : S ^ n) (σ : S ^ k)
             → (∀ j → lookup (θ j) (γ ++ σ) ≡ ι (lookup j (constantsTm t)))
             → ⟦ t ⟧ γ ≡ ⟦ placeTm t θ ⟧₀ (γ ++ σ)
    ⟦⟧-place (con c) θ γ σ h = sym (h zero)

For a variable var i nothing was replaced, only re-indexed: the translation moved it to padRight k i, the same slot in the wider context, and the pad law shows that looking it up in γ ++ σ recovers the original value. With the constant and variable cases settled, every remaining constructor is either a two-part node handled by the splitting invariant or a binder, and the formula-level induction follows the same pattern.

    ⟦⟧-place (var i) θ γ σ h = sym (lookup-padRight γ σ i)

Then the twelve cases of the induction, ten formula cases here and the two term cases just discharged. Every primitive propositional clause is a congruence, because the semantics assigns its constructor exactly the corresponding logical operation and there is no translation layer to cross. The four binding clauses push a value onto the environment and appeal to the induction hypothesis at the extended one, and the hypothesis about the parameter slots travels unchanged: consing on the left and shifting the placement by suc cancel each other by computation, so the binders need no lemma of their own. The two bounded clauses split, term on the left and body on the right, exactly as their constructors do.

The formula-level statement ⊨-place has the same shape as the term lemma, with satisfaction in place of denotation: under the hypothesis h about the placed slots, (γ ⊨ φ) equals ((γ ++ σ) ⊨₀ placeFo φ θ). The representative atom is membership t ∈̇ u: satisfaction of an atom is a congruence of the two term values along the structure's membership, so the clause applies the term lemma to each operand, at the placements the traversal actually used.

    ⊨-place : ∀ {n k} (φ : Formula K n) (θ : Fin (countFo φ) → Fin (n + k))
              (γ : S ^ n) (σ : S ^ k)
            → (∀ j → lookup (θ j) (γ ++ σ) ≡ ι (lookup j (constantsFo φ)))
            → (γ ⊨ φ) ≡ ((γ ++ σ) ⊨₀ placeFo φ θ)
    ⊨-place (t ∈̇ u) θ γ σ h = cong₂ _∈ˢ_

The per-operand hypothesis is precisely what the splitting invariant supplies: the joint hypothesis h for constantsTm t ++ constantsTm u, restricted on the left by padRight and on the right by padLeft. The equality atom t ≐ u is handled identically, with the structure's equality ≈ˢ in place of membership, and the two propositional connectives that follow need only the formula-level induction in place of the term lemma.

      (⟦⟧-place t (λ i → θ (padRight (countTm u) i)) γ σ
        (leftHalf θ γ σ (constantsTm t) (constantsTm u) h))
      (⟦⟧-place u (λ j → θ (padLeft (countTm t) j)) γ σ
        (rightHalf (countTm t) θ γ σ (constantsTm t) (constantsTm u) h))
    ⊨-place (t ≐ u) θ γ σ h = cong₂ _≈ˢ_

Conjunction is the first purely propositional clause. The semantics defines satisfaction of φ ∧̇ ψ by applying propositional conjunction _⊓_ to the two satisfaction values, so the clause is cong₂ _⊓_ under the two induction hypotheses, with h split between constantsFo φ and constantsFo ψ. The proof treats (γ ⊨ φ) ⊓ (γ ⊨ ψ) simply as a proposition in hProp ℓ: it uses congruence alone, without assuming or decomposing any pair representation.

      (⟦⟧-place t (λ i → θ (padRight (countTm u) i)) γ σ
        (leftHalf θ γ σ (constantsTm t) (constantsTm u) h))
      (⟦⟧-place u (λ j → θ (padLeft (countTm t) j)) γ σ
        (rightHalf (countTm t) θ γ σ (constantsTm t) (constantsTm u) h))
    ⊨-place (φ ∧̇ ψ) θ γ σ h = cong₂ _⊓_

Disjunction repeats the pattern with propositional disjunction ⊔, and implication with propositional implication ⇒. The three propositional clauses differ only in which logical operation cong₂ is applied to; everything else, including the split hypothesis, is identical.

      (⊨-place φ (λ i → θ (padRight (countFo ψ) i)) γ σ
        (leftHalf θ γ σ (constantsFo φ) (constantsFo ψ) h))
      (⊨-place ψ (λ j → θ (padLeft (countFo φ) j)) γ σ
        (rightHalf (countFo φ) θ γ σ (constantsFo φ) (constantsFo ψ) h))
    ⊨-place (φ ∨̇ ψ) θ γ σ h = cong₂ _⊔_

At this point the pattern is worth stating once: every remaining clause either applies a congruence at the logical operation the semantics chose for its constructor, or pushes a value onto the environment and recurses. No clause needs a new idea.

      (⊨-place φ (λ i → θ (padRight (countFo ψ) i)) γ σ
        (leftHalf θ γ σ (constantsFo φ) (constantsFo ψ) h))
      (⊨-place ψ (λ j → θ (padLeft (countFo φ) j)) γ σ
        (rightHalf (countFo φ) θ γ σ (constantsFo φ) (constantsFo ψ) h))
    ⊨-place (φ ⇒̇ ψ) θ γ σ h = cong₂ _⇒_

Falsity confirms this. Both sides of the equation are the false proposition whatever the environment or placement may be, so the clause is refl. It is also the one constructor whose translation never mentions the parameter block.

      (⊨-place φ (λ i → θ (padRight (countFo ψ) i)) γ σ
        (leftHalf θ γ σ (constantsFo φ) (constantsFo ψ) h))
      (⊨-place ψ (λ j → θ (padLeft (countFo φ) j)) γ σ
        (rightHalf (countFo φ) θ γ σ (constantsFo φ) (constantsFo ψ) h))
    ⊨-place ⊥̇       θ γ σ h = refl

The unbounded quantifier ∃̇ φ is the binder case, and its content is that the shift cancels. The traversal placed the body under suc ∘ θ, because consing the bound value onto the left moves every parameter slot up by one; the semantics quantifies over x ∷ γ. The recursive claim is therefore invoked at x ∷ γ, and there lookup (suc (θ j)) (x ∷ γ ++ σ) computes to lookup (θ j) (γ ++ σ), which is exactly h. The cancellation is definitional, so no shifting lemma appears anywhere in the proof.

    ⊨-place (∃̇ φ)   θ γ σ h = cong (λ P → ∃[ x ∶ S ] P x) (funExt (λ x →
      ⊨-place φ (λ j → suc (θ j)) (x ∷ γ) σ h))
    ⊨-place (∀̇ φ)   θ γ σ h = cong (λ P → ∀[ x ∶ S ] P x) (funExt (λ x →
      ⊨-place φ (λ j → suc (θ j)) (x ∷ γ) σ h))
    ⊨-place (∀̇∈ t φ) θ γ σ h = cong (λ P → ∀[ x ∶ S ] P x) (funExt (λ x → cong₂ _⇒_

The universal quantifier ∀̇ is the same argument with the algebra's universal-quantification operation ∀[ x ] P x in place of its existential-quantification operation ∃[ x ] P x; the outer cong is the only place the operation is named, and the induction underneath is identical.

      (cong (x ∈ˢ_) (⟦⟧-place t (λ i → θ (padRight (countFo φ) i)) γ σ
        (leftHalf θ γ σ (constantsTm t) (constantsFo φ) h)))
      (⊨-place φ (λ j → suc (θ (padLeft (countTm t) j))) (x ∷ γ) σ
        (rightHalf (countTm t) θ γ σ (constantsTm t) (constantsFo φ) h))))
    ⊨-place (∃̇∈ t φ) θ γ σ h = cong (λ P → ∃[ x ∶ S ] P x) (funExt (λ x → cong₂ _⊓_

The bounded quantifiers combine the two moves. For ∀̇∈ t φ the traversal abstracted the term t at the front of the context, through padRight past the body's occurrences, and shifted the body's placement by suc composed with padLeft past the term's occurrence. The clause is accordingly a cong₂ _⇒_ of x's membership in the abstracted bound, via the term lemma, and the recursive claim at x ∷ γ, via the shifted induction; leftHalf and rightHalf split h between constantsTm t and constantsFo φ. The existential bounded quantifier ∃̇∈ mirrors it with ⊓ in place of ⇒. Every constructor of the language is now covered by the same invariant.

      (cong (x ∈ˢ_) (⟦⟧-place t (λ i → θ (padRight (countFo φ) i)) γ σ
        (leftHalf θ γ σ (constantsTm t) (constantsFo φ) h)))
      (⊨-place φ (λ j → suc (θ (padLeft (countTm t) j))) (x ∷ γ) σ
        (rightHalf (countTm t) θ γ σ (constantsTm t) (constantsFo φ) h))))

The adequacy proper follows by choosing the placement the abstraction chose and the parameter environment the collection prescribes: the constants themselves, interpreted. Its hypothesis is then the two pad laws in sequence, and the theorem states exactly this. Satisfaction of the original at γ is satisfaction of the abstraction at γ extended by the collected constants.

The main theorem instantiates the induction once. Since absFo φ was produced by the traversal at the placement padLeft n, that placement is the one to apply ⊨-place at, and the parameter environment is chosen to be map ι (constantsFo φ): the recorded constants, in order, each interpreted. The resulting theorem says that satisfaction of the original formula at γ is satisfaction of the abstraction at γ extended by these interpreted constants.

    ⊨-abs : ∀ {n} (φ : Formula K n) (γ : S ^ n)
          → (γ ⊨ φ) ≡ ((γ ++ map ι (constantsFo φ)) ⊨₀ absFo φ)
    ⊨-abs {n} φ γ = ⊨-place φ (padLeft n) γ (map ι (constantsFo φ)) hyp
      where
      hyp : ∀ j → lookup (padLeft n j) (γ ++ map ι (constantsFo φ))

It remains to see that this choice of σ discharges the hypothesis. The placement padLeft n sends occurrence j to the entry n + j, which falls in the second half of the concatenation; lookup-padLeft identifies the entry with lookup j (map ι (constantsFo φ)), and lookup-map pulls the interpretation through, giving exactly ι (lookup j (constantsFo φ)). The two laws composed are the hypothesis, and with it ⊨-place yields the theorem. Mathematically: a parameter-free formula together with a finite ordered vector of parameters has the same extension as the original formula with constants.

                ≡ ι (lookup j (constantsFo φ))
      hyp j = lookup-padLeft n γ (map ι (constantsFo φ)) j
            ∙ lookup-map ι (constantsFo φ) j

What a definable subset is

Parameter abstraction isolates the data behind a definable subset: a parameter-free formula, its finite vector of parameters, and the variable at which membership is tested. Adequacy shows that this presentation has exactly the same extension as the original formula with constants.

One point of shape, and the reason the arity-one case is worth writing down: at arity one the extended environment is x ∷ map ι p, a single member followed by the parameters, which is the very shape a one-entry environment has everywhere else in the book.

For definable subsets of one variable, the corollary fixes the environment to x ∷ []: a formula of arity one is tested at the single member x, and the theorem gives the abstraction tested at x followed by the interpreted parameters. Because the statement is a path between propositions, the two readings of membership are interchangeable, and later chapters coding definable subsets may work with the parameter-free formula plus the parameter vector map ι (constantsFo φ) directly, without renaming constants or modifying the formula.

    ⊨-abs₁ : (φ : Formula K ) (x : S)
           → ((x ∷ []) ⊨ φ) ≡ ((x ∷ map ι (constantsFo φ)) ⊨₀ absFo φ)
    ⊨-abs₁ φ x = ⊨-abs φ (x ∷ [])

Recap

absFo removes constants by adding one variable per occurrence, and ⊨-abs identifies satisfaction after the recorded constants are appended to the environment. This is the finite parameter presentation used when formulas themselves must be coded.