Ordered full-tuple interpretations preserve least-fixed-point definability

The ordinary full-tuple interpretation, with its native canonical order, BIT, and constants, extends to checked FO(LFP) formulas. Each target relation argument is replaced by a coordinate block; positivity and nested binding are preserved. The sentence pullback has exactly the truth value of the original sentence on the canonical rank universe.

References

• N. Immerman, Relational Queries Computable in Polynomial Time, Section 3: polynomial-sized tableau domains are represented by tuples over the input structure.

noncomputable def Cslib.Logic.FO.Ordered.FullTupleInterpretation.onLFPFormula {L : FirstOrder.Language} {L' : FirstOrder.Language} [L'.IsRelational] {k : ℕ} (I : FullTupleInterpretation L L' k) {Γ : List ℕ} {α : Type} (φ : LFP.Formula (language L') Γ α) : LFP.Formula (language L) (List.map (fun (x : ℕ) => x * k) Γ) (α × Fin k)

Pull back checked FO(LFP) syntax, multiplying every relation arity by the tuple dimension.

noncomputable def Cslib.Logic.FO.Ordered.FullTupleInterpretation.onLFPSentence {L : FirstOrder.Language} {L' : FirstOrder.Language} [L'.IsRelational] {k : ℕ} (I : FullTupleInterpretation L L' k) (φ : LFP.Formula (language L') [] Empty) : LFP.Formula (language L) [] Empty

Pull back a checked sentence; its empty free-variable context remains empty.

theorem Cslib.Logic.FO.Ordered.FullTupleInterpretation.realize_onLFPSentence {L : FirstOrder.Language} {L' : FirstOrder.Language} [L'.IsRelational] {k : ℕ} (I : FullTupleInterpretation L L' k) {n : ℕ} [Fact (2 ≤ n)] [L.Structure (Fin n)] (hk : 0 < k) (φ : LFP.Formula (language L') [] Empty) : (I.onLFPSentence φ).Realize (fun {k : ℕ} => Operator.RelEnv.empty) Empty.elim ↔ φ.Realize (fun {k_1 : ℕ} => Operator.RelEnv.empty) Empty.elim

The sentence pullback preserves truth on the canonical lexicographically ranked universe.