Pulling transitive-closure formulas back to tuples

An interpretation of target elements by full d-tuples lifts from ordinary first-order formulas to FO(TC). A closure over pairs of k-tuples of targets becomes a closure over pairs of k * d-tuples of source elements, and relation arities are multiplied by d. Term values are named by existential coordinates, as in the least-fixed-point pullback, so the translation reuses an ordinary first-order pullback, including its handling of target constants.

The semantic theorem uses a bijection between source tuples and target elements. It induces a bijection between closure vertices, which carries one edge relation to the other and so preserves reflexive reachability. The translation also preserves the closure polarity TC.Positive.

The semantic theorem is stated once for every closure semantics closureBy T, the reflexive transitive closure of T applied to the body relation, where T commutes with relabelling the vertices along a bijection (Transports T). Ordinary closure is T = id (interpretation_eq_closureBy_id); deterministic closure takes for T the deterministic reduct.

Main definitions

• Cslib.Logic.FO.TC.Tuple.onFormula: extend a first-order tuple pullback to FO(TC).
• Cslib.Logic.FO.TC.Tuple.closureBy: closure of a transformed body relation.
• Cslib.Logic.FO.TC.Tuple.Transports: a relation transform commutes with bijections.

Main results

• Cslib.Logic.FO.TC.Tuple.realize_onFormula_closureBy: the pullback preserves truth under every transported closure semantics, for all relation valuations that correspond blockwise.
• Cslib.Logic.FO.TC.Tuple.realize_onFormula: the instance for ordinary closure.
• Cslib.Logic.FO.TC.Tuple.positive_onFormula: the pullback preserves closure polarity.

theorem Cslib.Logic.FO.TC.Tuple.blockEquiv_pair {d : ℕ} {M : Type u_1} {N : Type u_2} (e : (Fin d → M) ≃ N) {k : ℕ} (xs ys : Fin (k * d) → M) : ((Operator.Tuple.blockEquiv e (2 * k)) fun (i : Fin (2 * k * d)) => pair xs ys (Fin.cast ⋯ i)) = pair ((Operator.Tuple.blockEquiv e k) xs) ((Operator.Tuple.blockEquiv e k) ys)

Concatenated coordinate blocks are carried to concatenated targets.

def Cslib.Logic.FO.TC.Tuple.endpointMap {d : ℕ} {β : Type u_1} {k : ℕ} : β ⊕ Fin (2 * k * d) → β ⊕ Fin (2 * (k * d))

Lay out the flattened coordinates of two endpoint tuples as one closure tuple.

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

Extend an ordinary first-order tuple pullback to FO(TC) syntax. A closure of width k becomes a closure of width k * d.

@[simp]

theorem Cslib.Logic.FO.TC.Tuple.positive_applyTerms {L : FirstOrder.Language} {L' : FirstOrder.Language} {d : ℕ} {Γ : List ℕ} {α : Type} (f : Operator.Tuple.FOMap L L' d) {k : ℕ} (args : Fin k → L'.Term α) (φ : Operator.Formula L shape Γ (α × Fin d ⊕ Fin (k * d))) (s : Bool) : Positive (Operator.Tuple.applyTerms (fun {α : Type} => f) args φ) s ↔ Positive φ s

Naming term values does not change the polarity of closures.

@[simp]

theorem Cslib.Logic.FO.TC.Tuple.positive_onFormula {L : FirstOrder.Language} {L' : FirstOrder.Language} {d : ℕ} {Γ : List ℕ} {α : Type} (f : Operator.Tuple.FOMap L L' d) (φ : Operator.Formula L' shape Γ α) (s : Bool) : Positive (onFormula (fun {α : Type} => f) φ) s ↔ Positive φ s

Tuple pullback preserves the polarity of every closure.

def Cslib.Logic.FO.TC.Tuple.closureBy (T : {β : Type} → (β → β → Prop) → β → β → Prop) {M : Type} : Operator.Interpretation shape M

Closure of a transformed body relation: reflexive reachability along T of the relation that the body defines on closure tuples. closureBy id is interpretation; taking for T the deterministic reduct gives deterministic closure.

def Cslib.Logic.FO.TC.Tuple.Transports (T : {β : Type} → (β → β → Prop) → β → β → Prop) : Prop

A relation transform T commutes with relabelling the vertices along a bijection.

theorem Cslib.Logic.FO.TC.Tuple.transports_id : Transports fun {β : Type} (r : β → β → Prop) => r

The identity transform commutes with bijections.

theorem Cslib.Logic.FO.TC.Tuple.interpretation_eq_closureBy_id {M : Type} : interpretation = closureBy fun {β : Type} (r : β → β → Prop) => r

Ordinary closure is closure of the untransformed body relation.

theorem Cslib.Logic.FO.TC.Tuple.realize_tc_closureBy {L : FirstOrder.Language} {Γ : List ℕ} {α : Type} (T : {β : Type} → (β → β → Prop) → β → β → Prop) {M : Type} [L.Structure M] {k : ℕ} (body : Operator.Formula L shape Γ (α ⊕ Fin (2 * k))) (args : Fin (2 * k) → L.Term α) (ρ : Operator.RelEnv Γ M) (v : α → M) : Operator.Formula.Realize (closureBy fun {β : Type} => T) (tc body args) (fun {k : ℕ} => ρ) v ↔ Relation.ReflTransGen (T fun (xs ys : Fin k → M) => Operator.Formula.Realize (closureBy fun {β : Type} => T) body (fun {k : ℕ} => ρ) (Sum.elim v (pair xs ys))) (fun (i : Fin k) => FirstOrder.Language.Term.realize v (left args i)) fun (i : Fin k) => FirstOrder.Language.Term.realize v (right args i)

A closure under closureBy T follows T of the body relation.

theorem Cslib.Logic.FO.TC.Tuple.realize_onFormula_closureBy {L : FirstOrder.Language} {L' : FirstOrder.Language} {d : ℕ} {Γ : List ℕ} {α M N : Type} [L.Structure M] [L'.Structure N] (f : Operator.Tuple.FOMap L L' d) (e : (Fin d → M) ≃ N) (hf : ∀ {α : Type} (φ : L'.Formula α) (v : α × Fin d → M), (f φ).Realize v ↔ φ.Realize fun (a : α) => e fun (i : Fin d) => v (a, i)) {T : {β : Type} → (β → β → Prop) → β → β → Prop} (hT : Transports fun {β : Type} => T) (φ : Operator.Formula L' shape Γ α) (ρs : Operator.RelEnv (List.map (fun (x : ℕ) => x * d) Γ) M) (ρt : Operator.RelEnv Γ N) : (∀ {k : ℕ} (r : Operator.RelVar Γ k) (xs : Fin (k * d) → M), xs ∈ ρs (Operator.RelVar.scale d r) ↔ (Operator.Tuple.blockEquiv e k) xs ∈ ρt r) → ∀ (v : α × Fin d → M), Operator.Formula.Realize (closureBy fun {β : Type} => T) (onFormula (fun {α : Type} => f) φ) (fun {k : ℕ} => ρs) v ↔ Operator.Formula.Realize (closureBy fun {β : Type} => T) φ (fun {k : ℕ} => ρt) fun (a : α) => e fun (i : Fin d) => v (a, i)

Full-tuple pullback preserves truth under every transported closure semantics, for arbitrary scoped relation valuations and nested closures. The relation valuations correspond blockwise through blockEquiv.

theorem Cslib.Logic.FO.TC.Tuple.realize_onFormula {L : FirstOrder.Language} {L' : FirstOrder.Language} {d : ℕ} {Γ : List ℕ} {α M N : Type} [L.Structure M] [L'.Structure N] (f : Operator.Tuple.FOMap L L' d) (e : (Fin d → M) ≃ N) (hf : ∀ {α : Type} (φ : L'.Formula α) (v : α × Fin d → M), (f φ).Realize v ↔ φ.Realize fun (a : α) => e fun (i : Fin d) => v (a, i)) (φ : Operator.Formula L' shape Γ α) (ρs : Operator.RelEnv (List.map (fun (x : ℕ) => x * d) Γ) M) (ρt : Operator.RelEnv Γ N) : (∀ {k : ℕ} (r : Operator.RelVar Γ k) (xs : Fin (k * d) → M), xs ∈ ρs (Operator.RelVar.scale d r) ↔ (Operator.Tuple.blockEquiv e k) xs ∈ ρt r) → ∀ (v : α × Fin d → M), Operator.Formula.Realize interpretation (onFormula (fun {α : Type} => f) φ) (fun {k : ℕ} => ρs) v ↔ Operator.Formula.Realize interpretation φ (fun {k : ℕ} => ρt) fun (a : α) => e fun (i : Fin d) => v (a, i)

Full-tuple pullback preserves truth for arbitrary scoped relation valuations, including nested closures. The relation valuations correspond blockwise through blockEquiv.