Documentation

Complexitylib.DescriptiveComplexity.FirstOrder.Substitution

First-order substitution #

Simultaneous substitution of terms for the free (de Bruijn) variables of a formula, and its semantic correctness — the substitution theorem Formula.subst_sat: satisfaction of φ.subst ρ under σ equals satisfaction of φ under the environment k ↦ ⟦ρ k⟧_σ.

The de Bruijn bookkeeping is handled by Term.shift (raise every index by one, for crossing a binder) and liftSubst (extend a substitution under a binder: the new variable 0 stays, everything else is shifted). This is the engine behind the fundamental theorem of first-order interpretations (roadmap L6): the transport of a formula along an FOInterpretation.

Main definitions and results #

source
def Complexity.DescriptiveComplexity.Term.shift {V : Vocabulary} {n : Nat} :
Term V n → Term V (n + 1)

Shift every variable of a term up by one de Bruijn index (to cross a binder).

Equations
Instances For
    source
    theorem Complexity.DescriptiveComplexity.Term.shift_eval {V : Vocabulary} {n : Nat} (A : FinStruct V) (a : Fin A.card) (σ : Env A.card n) (t : Term V n) :
    eval A (envCons a σ) t.shift = eval A σ t

    Shifting a term and evaluating under an extended environment recovers the original evaluation: the fresh variable 0 is never referenced by a shifted term.

    source
    def Complexity.DescriptiveComplexity.Term.substTerm {V : Vocabulary} {m n : Nat} (ρ : Fin m → Term V n) :
    Term V m → Term V n

    Apply a substitution (a term for each variable) to a term.

    Equations
    Instances For
      source
      theorem Complexity.DescriptiveComplexity.Term.substTerm_eval {V : Vocabulary} {m n : Nat} (A : FinStruct V) (σ : Env A.card n) (ρ : Fin m → Term V n) (t : Term V m) :
      eval A σ (substTerm ρ t) = eval A (fun (k : Fin m) => eval A σ (ρ k)) t

      Evaluating a substituted term is evaluating the original under the substituted environment.

      source
      def Complexity.DescriptiveComplexity.liftSubst {V : Vocabulary} {m n : Nat} (ρ : Fin m → Term V n) :
      Fin (m + 1) → Term V (n + 1)

      Lift a substitution under a binder: variable 0 maps to itself, and every other variable takes its old (shifted) image.

      Equations
      Instances For
        source
        theorem Complexity.DescriptiveComplexity.liftSubst_eval {V : Vocabulary} {m n : Nat} (A : FinStruct V) (a : Fin A.card) (σ : Env A.card n) (ρ : Fin m → Term V n) :
        (fun (k : Fin (m + 1)) => Term.eval A (envCons a σ) (liftSubst ρ k)) = envCons a fun (k : Fin m) => Term.eval A σ (ρ k)

        The environment induced by a lifted substitution is the extension (by the new element) of the environment induced by the original — the compatibility fact that drives the quantifier case of the substitution theorem.

        source
        def Complexity.DescriptiveComplexity.Formula.subst {V : Vocabulary} {m n : Nat} :
        Formula V m → (Fin m → Term V n) → Formula V n

        Simultaneous substitution of terms for the free variables of a formula. Under a quantifier the substitution is lifted, so de Bruijn indices stay aligned.

        Equations
        Instances For
          source
          theorem Complexity.DescriptiveComplexity.Formula.quantifierRank_subst {V : Vocabulary} {m n : Nat} (φ : Formula V m) (ρ : Fin m → Term V n) :
          (φ.subst ρ).quantifierRank = φ.quantifierRank

          Substituting terms for free variables preserves quantifier rank exactly.

          source
          theorem Complexity.DescriptiveComplexity.Formula.subst_sat {V : Vocabulary} (A : FinStruct V) {m n : Nat} (σ : Env A.card n) (ρ : Fin m → Term V n) (φ : Formula V m) :
          Sat A σ (φ.subst ρ) ↔ Sat A (fun (k : Fin m) => Term.eval A σ (ρ k)) φ

          The substitution theorem. Satisfaction of a substituted formula under σ equals satisfaction of the original formula under the environment that evaluates each substituted term.