First-order logic with tuple transitive closure

The operator of width k binds two k-tuples in one formula body and is applied to two k-tuples of terms. Its interpretation is the reflexive transitive closure of the relation defined by the body. Free parameters are held fixed along the path, and bodies may contain nested closure operators. Width zero is allowed: there is one empty tuple, even on an empty domain, and its reflexive reachability always holds.

Main definitions

• shape, policy, interpretation: tuple closure as a scoped, positive logical operator.
• tc: the formula constructor.
• pair, left, right: concatenate and split the endpoint tuples.

Main results

• interpretation_respects: closure is monotone in its body relation.
• realize_tc: semantics in terms of Mathlib's Relation.ReflTransGen.
• realize_tc_pair: the same semantics with explicit source and target term tuples.
• realize_tc_refl, realize_tc_of_body, realize_tc_trans: reflexivity, edge inclusion, and composition of paths.

This file provides logical syntax and semantics, not a complexity-class capture theorem.

References

• N. Immerman, Descriptive Complexity, Chapter 9

def Cslib.Logic.FO.TC.pair {A : Type u_1} {k : ℕ} (xs ys : Fin k → A) : Fin (2 * k) → A

Concatenate equal-length tuples, with the resulting arity written as 2 * k.

def Cslib.Logic.FO.TC.left {A : Type u_1} {k : ℕ} (xs : Fin (2 * k) → A) : Fin k → A

The source tuple of a closure application.

def Cslib.Logic.FO.TC.right {A : Type u_1} {k : ℕ} (xs : Fin (2 * k) → A) : Fin k → A

The target tuple of a closure application.

@[simp]

theorem Cslib.Logic.FO.TC.left_pair {A : Type u_1} {k : ℕ} (xs ys : Fin k → A) : left (pair xs ys) = xs

Concatenation preserves the source tuple.

@[simp]

theorem Cslib.Logic.FO.TC.right_pair {A : Type u_1} {k : ℕ} (xs ys : Fin k → A) : right (pair xs ys) = ys

Concatenation preserves the target tuple.

@[simp]

theorem Cslib.Logic.FO.TC.pair_left_right {A : Type u_1} {k : ℕ} (xs : Fin (2 * k) → A) : pair (left xs) (right xs) = xs

A closure tuple is the concatenation of its source and target tuples.

def Cslib.Logic.FO.TC.shape (k : ℕ) : Operator.Shape

Tuple closure binds two tuples and no relation variables.

def Cslib.Logic.FO.TC.policy : Operator.Policy shape

Closure is positive in its single body and imposes no local relation constraints.

def Cslib.Logic.FO.TC.interpretation {M : Type z} : Operator.Interpretation shape M

Interpret closure as reflexive reachability between endpoint tuples.

theorem Cslib.Logic.FO.TC.interpretation_respects {M : Type z} : interpretation.Respects policy.variance

Enlarging the body relation preserves all paths.

def Cslib.Logic.FO.TC.tc {L : FirstOrder.Language} {Γ : List ℕ} {α : Type w} {k : ℕ} (body : Operator.Formula L shape Γ (α ⊕ Fin (2 * k))) (args : Fin (2 * k) → L.Term α) : Operator.Formula L shape Γ α

Apply tuple closure to a body with two locally bound endpoint tuples.

@[simp]

theorem Cslib.Logic.FO.TC.wellFormed_tc {L : FirstOrder.Language} {Γ : List ℕ} {α : Type w} {k : ℕ} (body : Operator.Formula L shape Γ (α ⊕ Fin (2 * k))) (args : Fin (2 * k) → L.Term α) : Operator.Formula.wellFormed policy (tc body args) = Operator.Formula.wellFormed policy body

Closure adds no formation condition beyond those already present in its body.

@[simp]

theorem Cslib.Logic.FO.TC.realize_tc {L : FirstOrder.Language} {Γ : List ℕ} {α : Type w} {M : Type z} [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 interpretation (tc body args) (fun {k : ℕ} => ρ) v ↔ Relation.ReflTransGen (fun (xs ys : Fin k → M) => Operator.Formula.Realize interpretation 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)

Closure holds exactly when a finite path connects the evaluated endpoint tuples.

theorem Cslib.Logic.FO.TC.realize_tc_pair {L : FirstOrder.Language} {Γ : List ℕ} {α : Type w} {M : Type z} [L.Structure M] {k : ℕ} (body : Operator.Formula L shape Γ (α ⊕ Fin (2 * k))) (xs ys : Fin k → L.Term α) (ρ : Operator.RelEnv Γ M) (v : α → M) : Operator.Formula.Realize interpretation (tc body (pair xs ys)) (fun {k : ℕ} => ρ) v ↔ Relation.ReflTransGen (fun (us vs : Fin k → M) => Operator.Formula.Realize interpretation body (fun {k : ℕ} => ρ) (Sum.elim v (pair us vs))) (fun (i : Fin k) => FirstOrder.Language.Term.realize v (xs i)) fun (i : Fin k) => FirstOrder.Language.Term.realize v (ys i)

Applying closure to concatenated endpoint terms realizes ordinary tuple reachability.

theorem Cslib.Logic.FO.TC.realize_tc_refl {L : FirstOrder.Language} {Γ : List ℕ} {α : Type w} {M : Type z} [L.Structure M] {k : ℕ} (body : Operator.Formula L shape Γ (α ⊕ Fin (2 * k))) (xs : Fin k → L.Term α) (ρ : Operator.RelEnv Γ M) (v : α → M) : Operator.Formula.Realize interpretation (tc body (pair xs xs)) (fun {k : ℕ} => ρ) v

The empty path makes every tuple reachable from itself.

theorem Cslib.Logic.FO.TC.realize_tc_of_body {L : FirstOrder.Language} {Γ : List ℕ} {α : Type w} {M : Type z} [L.Structure M] {k : ℕ} (body : Operator.Formula L shape Γ (α ⊕ Fin (2 * k))) (xs ys : Fin k → L.Term α) (ρ : Operator.RelEnv Γ M) (v : α → M) (h : Operator.Formula.Realize interpretation body (fun {k : ℕ} => ρ) (Sum.elim v (pair (fun (i : Fin k) => FirstOrder.Language.Term.realize v (xs i)) fun (i : Fin k) => FirstOrder.Language.Term.realize v (ys i)))) : Operator.Formula.Realize interpretation (tc body (pair xs ys)) (fun {k : ℕ} => ρ) v

Every edge defined by the body is a closure path of length one.

theorem Cslib.Logic.FO.TC.realize_tc_trans {L : FirstOrder.Language} {Γ : List ℕ} {α : Type w} {M : Type z} [L.Structure M] {k : ℕ} (body : Operator.Formula L shape Γ (α ⊕ Fin (2 * k))) (xs ys zs : Fin k → L.Term α) (ρ : Operator.RelEnv Γ M) (v : α → M) (hxy : Operator.Formula.Realize interpretation (tc body (pair xs ys)) (fun {k : ℕ} => ρ) v) (hyz : Operator.Formula.Realize interpretation (tc body (pair ys zs)) (fun {k : ℕ} => ρ) v) : Operator.Formula.Realize interpretation (tc body (pair xs zs)) (fun {k : ℕ} => ρ) v

Paths with a common intermediate tuple compose.