Formula pullback for tagged tuple interpretations

The dual of an interpretation replaces variables by tuples, relation atoms by their defining formulas, equality by equality of tags and coordinates, and each quantifier by a finite tag choice followed by a block of coordinate quantifiers. This is Immerman's Definition 3.3 and Proposition 3.5, using the tagged full universe of Senellart--Gnatenko (2026), Sections 3.2--3.3. Constants are tuples of source constants, the special case in the footnote to Definition 3.3.

pullbackWith accepts arbitrary source terms for the coordinates of free target variables. This stronger interface makes substitution and interpretation composition possible without special cases for closed formulas.

def Complexity.DescriptiveComplexity.TaggedFOInterpretation.termTag {V W : Vocabulary} {tags dim n : ℕ} (I : TaggedFOInterpretation V W tags dim) (τ : Fin n → Fin tags) : Term W n → Fin tags

The tag of a target term under a tag assignment.

Equations

• I.termTag τ (Complexity.DescriptiveComplexity.Term.var i) = τ i
• I.termTag τ (Complexity.DescriptiveComplexity.Term.const c) = I.constTag c

def Complexity.DescriptiveComplexity.TaggedFOInterpretation.termCoords {V W : Vocabulary} {tags dim n m : ℕ} (I : TaggedFOInterpretation V W tags dim) (κ : Fin n → Fin dim → Term V m) : Term W n → Fin dim → Term V m

Source terms describing the coordinates of a target term.

Equations

• I.termCoords κ (Complexity.DescriptiveComplexity.Term.var i) = κ i
• I.termCoords κ (Complexity.DescriptiveComplexity.Term.const c) = fun (j : Fin dim) => Complexity.DescriptiveComplexity.Term.const (I.constCoord c j)

def Complexity.DescriptiveComplexity.TaggedFOInterpretation.liftCoords {V : Vocabulary} {dim n m : ℕ} (κ : Fin n → Fin dim → Term V m) : Fin (n + 1) → Fin dim → Term V (m + dim)

Under a tuple binder, new coordinates are variables and old coordinates are shifted.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.DescriptiveComplexity.TaggedFOInterpretation.coordEnv {V : Vocabulary} {tags dim n m : ℕ} (A : FinStruct V) (τ : Fin n → Fin tags) (κ : Fin n → Fin dim → Term V m) (σ : Env A.card m) : Env (tags * A.card ^ dim) n

Interpret a target variable assignment from source terms for its coordinates.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.DescriptiveComplexity.TaggedFOInterpretation.pullbackWith {V W : Vocabulary} {tags dim : ℕ} (I : TaggedFOInterpretation V W tags dim) {n m : ℕ} : Formula W n → (Fin n → Fin tags) → (Fin n → Fin dim → Term V m) → Formula V m

Pull back a formula using a tag and a tuple of source terms for every free variable.

Equations

• One or more equations did not get rendered due to their size.
• I.pullbackWith φ.neg x✝¹ x✝ = (I.pullbackWith φ x✝¹ x✝).neg
• I.pullbackWith (φ.conj ψ) x✝¹ x✝ = (I.pullbackWith φ x✝¹ x✝).conj (I.pullbackWith ψ x✝¹ x✝)
• I.pullbackWith (φ.disj ψ) x✝¹ x✝ = (I.pullbackWith φ x✝¹ x✝).disj (I.pullbackWith ψ x✝¹ x✝)

def Complexity.DescriptiveComplexity.TaggedFOInterpretation.translate {V W : Vocabulary} {tags dim n : ℕ} (I : TaggedFOInterpretation V W tags dim) (φ : Formula W n) (τ : Fin n → Fin tags) : Formula V (n * dim)

Pull back an open formula with one block of source variables per target variable.

Equations

• I.translate φ τ = I.pullbackWith φ τ fun (i : Fin n) (j : Fin dim) => Complexity.DescriptiveComplexity.Term.var (finProdFinEquiv (i, j))

def Complexity.DescriptiveComplexity.TaggedFOInterpretation.translateSentence {V W : Vocabulary} {tags dim : ℕ} (I : TaggedFOInterpretation V W tags dim) (φ : Sentence W) : Sentence V

Pull back a sentence; there are no free tags or coordinates to supply.

Equations

• I.translateSentence φ = I.pullbackWith φ Fin.elim0 fun (i : Fin 0) => i.elim0