Lax Lean Archive

The Immerman–Vardi theorem

Lax751879.ImmermanVardi · concepts/Lax751879/ImmermanVardi.lean · lax-751879

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.

    Natural Language Statement

    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).

    Concept map
    8 concepts
    100%
    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.

    1 capturesPtime proven

    2 ptimeDefinable proven

    Lean source view on GitHub

    1import Lax751879.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 Lax751879.ImmermanVardi
    29
    30open Lax751879.OrderedStructures Lax751879.FixedPointSemantics
    31open Lax751879.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 Lax751879.ImmermanVardi
    40
    Show ProofShow Proof
    Builds on
    Used by

    none

    From Mathlib

    none

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…