Transitive-closure definability of ordered queries

An ordered query is TCDefinable if a single FO(TC) sentence defines it on all canonically ordered structures, and PosTCDefinable if moreover every closure of that sentence occurs positively. As for LFPDefinable, the input relations vary while order, BIT and the numeric constants keep the meanings supplied by Ordered.language, and structures have at least two elements. Closure is reflexive transitive closure on tuples of any fixed width, including width zero.

Main definitions

• Cslib.Logic.FO.Ordered.TCDefinable: definability by one FO(TC) sentence.
• Cslib.Logic.FO.Ordered.PosTCDefinable: definability by one FO(positive TC) sentence.

Main results

• Cslib.Logic.FO.Ordered.Definable.posTCDefinable: first-order definable queries are FO(positive TC) definable.

References

• N. Immerman, Languages That Capture Complexity Classes, Section 3

def Cslib.Logic.FO.Ordered.TCDefinable {L : FirstOrder.Language} (K : Query L) : Prop

One FO(TC) sentence defines the query uniformly over all ordered inputs.

def Cslib.Logic.FO.Ordered.PosTCDefinable {L : FirstOrder.Language} (K : Query L) : Prop

One FO(TC) sentence whose closure operators all occur positively defines the query.

theorem Cslib.Logic.FO.Ordered.PosTCDefinable.tcDefinable {L : FirstOrder.Language} {K : Query L} (h : PosTCDefinable K) : TCDefinable K

Positive closure definability is closure definability.

theorem Cslib.Logic.FO.Ordered.Definable.posTCDefinable {L : FirstOrder.Language} {K : Query L} (hK : Definable K) : PosTCDefinable K

Ordinary ordered first-order definability embeds into positive closure definability.