Pulling least-fixed-point formulas back to tuples

An interpretation of target elements by full tuples lifts from ordinary first-order formulas to FO(LFP). Relation arities are multiplied by the tuple dimension. Existentially named term values let the construction reuse an ordinary first-order pullback, including its handling of target constants. It preserves both formation and syntactic polarity. The operator-independent pieces are shared with the transitive-closure pullback through CslibFrontier.Logics.FirstOrder.Operator.Tuple.

The semantic theorem uses a bijection between source tuples and target elements. Thus the relation spaces are also in bijection, and the intersection of pre-fixed relations is preserved.

noncomputable def Cslib.Logic.FO.LFP.Tuple.onFormula {L : FirstOrder.Language} {L' : FirstOrder.Language} {d : ℕ} (f : Operator.Tuple.FOMap L L' d) {Γ : List ℕ} {α : Type} : RawFormula L' Γ α → RawFormula L (List.map (fun (x : ℕ) => x * d) Γ) (α × Fin d)

Extend an ordinary first-order tuple pullback to scoped FO(LFP) syntax.

@[simp]

theorem Cslib.Logic.FO.LFP.Tuple.checkPolarity_onFormula {L : FirstOrder.Language} {L' : FirstOrder.Language} {d : ℕ} {Γ : List ℕ} {α : Type} (f : Operator.Tuple.FOMap L L' d) (φ : RawFormula L' Γ α) (sign : Bool) (mark : Operator.Marking (List.map (fun (x : ℕ) => x * d) Γ)) : (Operator.Formula.checkPolarity policy.variance (onFormula (fun {α : Type} => f) φ) sign fun {k : ℕ} => mark) = Operator.Formula.checkPolarity policy.variance φ sign fun {x : ℕ} (r : Operator.RelVar Γ x) => mark (Operator.RelVar.scale d r)

Tuple pullback preserves the syntactic polarity check.

@[simp]

theorem Cslib.Logic.FO.LFP.Tuple.wellFormed_onFormula {L : FirstOrder.Language} {L' : FirstOrder.Language} {d : ℕ} {Γ : List ℕ} {α : Type} (f : Operator.Tuple.FOMap L L' d) (φ : RawFormula L' Γ α) : Operator.Formula.wellFormed policy (onFormula (fun {α : Type} => f) φ) = Operator.Formula.wellFormed policy φ

Tuple pullback preserves the formation check at every nested fixed-point binder.