The Immerman–Vardi characterization of polynomial time

On the library's canonically ordered finite structures, a query is definable by one checked FO(LFP) sentence exactly when its source-only encoded language belongs to native P. The vocabulary is finite and relational; its fixed enumeration determines truth-table order. Universes are Fin n with n ≥ 2. Order, BIT, zero, one, and maximum are canonical numeric symbols, computed from the universe size rather than supplied as input tables.

The forward direction compiles a fixed formula to a native polynomial-time model checker. For the converse, a native deterministic machine has a positive local tableau. Its input symbols are defined directly from the actual binary encoding. A fixed tuple width bounds the machine's time, input length, and finite feature tags for all input sizes. Pullback along the canonical full-tuple interpretation gives one sentence over the original input universe.

Main results

• FO.Ordered.LFPDefinable.of_encodedLanguage_mem_P: every native polynomial-time ordered query has a uniform checked FO(LFP) sentence.
• FO.Ordered.lfpDefinable_iff_encodedLanguage_mem_P: FO(LFP) captures native polynomial time.

References

• N. Immerman, Relational Queries Computable in Polynomial Time, Theorem 1 and Section 3. The theorem is instantiated here at the existing canonical ordered vocabulary and unary-cardinality/full-truth-table encoding. Malformed table shapes and universes below two are rejected.

theorem Cslib.Logic.FO.Ordered.LFPDefinable.of_encodedLanguage_mem_P {L : FirstOrder.Language} [L.IsRelational] (v : Vocabulary L) {K : Query L} (hK : K.encodedLanguage v ∈ Complexity.P encStructure) : LFPDefinable K

Every ordered query decided by an actual native polynomial-time machine is defined by one checked FO(LFP) sentence over the original ordered input structures.

theorem Cslib.Logic.FO.Ordered.lfpDefinable_iff_encodedLanguage_mem_P {L : FirstOrder.Language} [L.IsRelational] (v : Vocabulary L) (K : Query L) : LFPDefinable K ↔ K.encodedLanguage v ∈ Complexity.P encStructure

Immerman–Vardi: a single checked FO(LFP) sentence defines an ordered query exactly when its source-only language is decidable in native polynomial time.