Lax Lean Archive

Draft — mutable and not usable as a dependency; its citation marks the draft state.

Lax979537.ImmermanVardi

The Immerman–Vardi theorem

concepts/Lax979537/ImmermanVardi.lean · lax-979537

proven

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Concept map

    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

    Evidence

    This concept declares 2 statements. Each proof establishes one of them relative to its assumptions.

    1st statement capturesPtime proven

    2nd statement ptimeDefinable proven

    Theorem

    On finite linearly ordered relational structures, a query is definable in first-order logic with least fixed points if and only if it is decidable in deterministic polynomial time.

    The vocabulary and query arity are arbitrary but fixed. The order is part of the logical structure. Queries may depend on it; no order-independence condition is imposed. The arity-zero instance is the usual statement for Boolean properties of ordered structures.

    The expressive direction is stated separately: every polynomial-time query has an FO(LFP) definition. Its proof must represent polynomially bounded Turing computations using tuples ordered lexicographically, and construct the defining fixed-point formula. All such simulation work belongs to the proof package, with no simulation premise added to the theorem.

    References: Immerman, Relational Queries Computable in Polynomial Time (1986), Theorem 2; Vardi, The Complexity of Relational Query Languages (STOC 1982).

    Lean source view on GitHub

    1import Lax979537.FixedPointEvaluation
    2
    3/-!
    4---
    5title: The Immerman–Vardi theorem
    6type: theorem
    7---
    8On finite linearly ordered relational structures, a query is definable in
    9first-order logic with least fixed points if and only if it is decidable
    10in deterministic polynomial time.
    11
    12The vocabulary and query arity are arbitrary but fixed. The order is part
    13of the logical structure. Queries may depend on it; no order-independence
    14condition is imposed. The arity-zero instance is the usual statement for
    15Boolean properties of ordered structures.
    16
    17The expressive direction is stated separately: every polynomial-time query
    18has an FO(LFP) definition. Its proof must represent polynomially bounded
    19Turing computations using tuples ordered lexicographically, and construct
    20the defining fixed-point formula. All such simulation work belongs to the
    21proof package, with no simulation premise added to the theorem.
    22
    23References: Immerman, *Relational Queries Computable in Polynomial Time*
    24(1986), Theorem 2; Vardi, *The Complexity of Relational Query Languages*
    25(STOC 1982).
    26-/
    27
    28namespace Lax979537.ImmermanVardi
    29
    30open Lax979537.OrderedStructures Lax979537.FixedPointSemantics
    31open Lax979537.PolynomialTime
    32
    33axiom ptimeDefinable {σ : Vocabulary} {k : Nat} (Q : Query σ k) :
    34 InP Q → Definable Q
    35
    36axiom capturesPtime {σ : Vocabulary} {k : Nat} (Q : Query σ k) :
    37 Definable Q ↔ InP Q
    38
    39end Lax979537.ImmermanVardi
    40
    Show ProofShow Proof

    Builds on

    Used by

    none

    From Mathlib

    none

    Community review

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above; your ORCID profile must share a public name.

    0 comments

    Loading discussion…