5.3. Capturing Polynomial Time🔗

Cslib.Logic.FO.Ordered.lfpDefinable_iff_encodedLanguage_mem_P proves the Immerman–Vardi characterization using the library's native multitape Turing-machine class P:

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

The vocabulary is fixed, finite, and relational. An ordered structure has universe Fin n with n ≥ 2; order, BIT, zero, one, and maximum have their canonical numeric meanings. Its encoded input contains the unary cardinality and full truth tables of the source relations. Numeric symbols are computed from the universe size. Malformed table shapes and universes below two are rejected by the language. This is the existing FO(≤, BIT) convention; the theorem does not include a separate elimination of BIT from pure-order FO(LFP).

The forward direction is Cslib.Logic.FO.Ordered.LFPDefinable.encodedLanguage_mem_P. For each fixed formula, the executable evaluator enumerates assignments and builds finite relation tables, using n ^ k iterations at each arity-k binder. The native loop calculus accounts for intermediate tables and captured input. The claim is data complexity: the formula and vocabulary are fixed while the input structure varies.

The converse is Cslib.Logic.FO.Ordered.LFPDefinable.of_encodedLanguage_mem_P. It takes an actual native polynomial-time machine and constructs one syntactically positive tableau formula. Its least fixed point equals the native execution table. First-order formulas recover the input symbols directly from the source encoding, including its framing and the machine's input endmarkers. One tuple width bounds the runtime, input length, and finite feature tags for every structure. The width and sentence are chosen before the input structure.

Cslib.Logic.FO.Ordered.FullTupleInterpretation.onLFPSentence transports that sentence back to the original universe. The reusable translation handles nested binders, scales relation arities by the tuple width, and preserves both syntactic positivity and realization. Its proof transports all candidate fixed-point relations through the tuple equivalence.