Least-fixed-point definability of ordered queries

An ordered query is LFPDefinable if a single checked FO(LFP) sentence defines it on all canonically ordered structures. The input relations vary, while order, BIT, and the numeric constants retain the meanings supplied by Ordered.language. Structures have at least two elements, as in the existing ordered-query convention.

This is the logical side of the Immerman–Vardi characterization. The machine side uses the existing source-only Query.encodedLanguage and native polynomial-time class.

References

• N. Immerman, Relational Queries Computable in Polynomial Time, Theorem 1.

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

One checked least-fixed-point sentence defines the query uniformly over all ordered inputs.

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

Ordinary ordered first-order definability embeds into least-fixed-point definability.