The dual-interpretation theorem for tagged tuples

An FO formula over the interpreted structure can be pulled back to an FO formula over the source. Free target variables supply their tags and coordinate tuples; sentences need no such parameters. In particular, FO definability is closed under tagged full-product interpretations.

This is the tagged variant of Immerman, Descriptive Complexity, Proposition 3.5 and Remark 3.6: https://people.cs.umass.edu/~immerman/book/ch3.pdf. Our target constants are tuples of source constants; definable constants, restricted universes, and quotients are not assumed by these statements.

theorem Complexity.DescriptiveComplexity.TaggedFOInterpretation.translate_sat {V W : Vocabulary} {tags dim n : ℕ} (I : TaggedFOInterpretation V W tags dim) (A : FinStruct V) (φ : Formula W n) (σ : Env (I.apply A).card n) : Formula.Sat A (relationEnv σ) (I.translate φ fun (i : Fin n) => ((elementEquiv A.card tags dim) (σ i)).1) ↔ Formula.Sat (I.apply A) σ φ

Tagged formula transport under an arbitrary assignment of target variables.

theorem Complexity.DescriptiveComplexity.TaggedFOInterpretation.translateSentence_models {V W : Vocabulary} {tags dim : ℕ} (I : TaggedFOInterpretation V W tags dim) (A : FinStruct V) (φ : Sentence W) : Sentence.Models A (I.translateSentence φ) ↔ Sentence.Models (I.apply A) φ

A source structure models the translated sentence exactly when its image models it.

theorem Complexity.DescriptiveComplexity.FODefinable.pullQuery {V W : Vocabulary} {tags dim : ℕ} {Q : BooleanQuery W} (hQ : FODefinable Q) (I : TaggedFOInterpretation V W tags dim) : FODefinable (I.pullQuery Q)

FO-definable queries remain FO-definable under tagged tuple interpretations.