Ordered full-tuple interpretations preserve transitive-closure definability

The ordinary full-tuple interpretation, with its native canonical order, BIT and constants, extends to FO(TC) sentences. A closure over pairs of width-w target tuples becomes a closure over pairs of width-w * k source tuples; closure polarity is preserved. The sentence pullback has exactly the truth value of the original sentence on the canonical rank universe, so a sentence written over a polynomially larger universe Fin (n ^ k) becomes a sentence over the input universe Fin n.

Main definitions

• FullTupleInterpretation.onTCSentence: pull back an FO(TC) sentence.

Main results

• FullTupleInterpretation.positive_onTCSentence: the pullback preserves closure polarity.
• FullTupleInterpretation.realize_onTCSentence_closureBy: the pullback preserves truth under every closure semantics TC.Tuple.closureBy T whose transform commutes with bijections.
• FullTupleInterpretation.realize_onTCSentence: the pullback preserves truth.

References

• N. Immerman, Languages That Capture Complexity Classes, Section 3: machine configurations of logarithmic size are coded by tuples of a fixed number of variables, and their reachability is expressed by one transitive closure over those tuples.

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

Pull back an FO(TC) sentence, multiplying every closure width by the tuple dimension.

@[simp]

theorem Cslib.Logic.FO.Ordered.FullTupleInterpretation.positive_onTCSentence {L : FirstOrder.Language} {L' : FirstOrder.Language} [L'.IsRelational] {k : ℕ} (I : FullTupleInterpretation L L' k) (φ : Operator.Formula (language L') TC.shape [] Empty) (s : Bool) : TC.Positive (I.onTCSentence φ) s ↔ TC.Positive φ s

The sentence pullback preserves the polarity of every closure.

theorem Cslib.Logic.FO.Ordered.FullTupleInterpretation.realize_onTCSentence_closureBy {L : FirstOrder.Language} {L' : FirstOrder.Language} [L'.IsRelational] {k : ℕ} (I : FullTupleInterpretation L L' k) {n : ℕ} [Fact (2 ≤ n)] [L.Structure (Fin n)] {T : {β : Type} → (β → β → Prop) → β → β → Prop} (hT : TC.Tuple.Transports fun {β : Type} => T) (hk : 0 < k) (φ : Operator.Formula (language L') TC.shape [] Empty) : Operator.Formula.Realize (TC.Tuple.closureBy fun {β : Type} => T) (I.onTCSentence φ) (fun {k : ℕ} => Operator.RelEnv.empty) Empty.elim ↔ Operator.Formula.Realize (TC.Tuple.closureBy fun {β : Type} => T) φ (fun {k_1 : ℕ} => Operator.RelEnv.empty) Empty.elim

The sentence pullback preserves truth on the canonical lexicographically ranked universe, under every closure semantics TC.Tuple.closureBy T whose transform commutes with bijections.

theorem Cslib.Logic.FO.Ordered.FullTupleInterpretation.realize_onTCSentence {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) (φ : Operator.Formula (language L') TC.shape [] Empty) : Operator.Formula.Realize TC.interpretation (I.onTCSentence φ) (fun {k : ℕ} => Operator.RelEnv.empty) Empty.elim ↔ Operator.Formula.Realize TC.interpretation φ (fun {k_1 : ℕ} => Operator.RelEnv.empty) Empty.elim

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