Lax Lean Archive

While this submission is a draft, it cannot be used by other submissions.

NP and PTIME against the logics of the two entries

Lax832283.LogicalBridge · concepts/Lax832283/LogicalBridge.lean · lax-832283

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

    A decision problem is in NP exactly when it reads as a property defined by an existential second-order sentence of the Fagin entry, and in PTIME exactly when it reads as a query defined by an FO(LFP) formula of the Immerman–Vardi entry. Neither statement mentions a machine, and neither proof assumes a capture theorem. The second is the substance of this submission: the formulas of the entry may nest, negate, and parameterize their fixed points, whereas the definitions of the library have one simultaneous fixed point.

    Concept map
    18 concepts; 1 descendant hidden
    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 mem_NP_iff_definable proven

    2 mem_PTIME_iff_definable proven

    Lean source view on GitHub

    1import Lax832283.StringProblems
    2import Lax904597.Classes
    3import Lax535992.ClassPTIME
    4import Lax751879.FixedPointSemantics
    5import Lax988886.ExistentialSecondOrder
    6
    7/-!
    8---
    9title: NP and PTIME against the logics of the two entries
    10type: theorem
    11---
    12A decision problem is in NP exactly when it reads as a property defined by an existential
    13second-order sentence of the Fagin entry, and in PTIME exactly when it reads as a query
    14defined by an FO(LFP) formula of the Immerman–Vardi entry. Neither statement mentions a
    15machine, and neither proof assumes a capture theorem. The second is the substance of this
    16submission: the formulas of the entry may nest, negate, and parameterize their fixed points,
    17whereas the definitions of the library have one simultaneous fixed point.
    18-/
    19
    20namespace Lax832283.LogicalBridge
    21
    22open FirstOrder Lax904597.Problems Lax904597.Classes Lax535992.ClassPTIME
    23open Lax832283.StringProblems
    24
    25/-- NP, against the existential second-order logic of the Fagin entry. -/
    26axiom mem_NP_iff_definable {L : Language.{0, 0}} [L.IsRelational] (V : FinVocab L)
    27 (P : DecisionProblem L) :
    28 NP.Mem P ↔ Lax988886.ExistentialSecondOrder.Definable (toProperty V P)
    29
    30/-- PTIME, against the FO(LFP) of the Immerman–Vardi entry. -/
    31axiom mem_PTIME_iff_definable {L : Language.{0, 0}} [L.IsRelational] (V : FinVocab L)
    32 (P : DecisionProblem L) :
    33 PTIME.Mem P ↔ Lax751879.FixedPointSemantics.Definable (toQuery V P)
    34
    35end Lax832283.LogicalBridge
    36
    Show ProofShow Proof
    Builds on
    Used by
    From Mathlib

    none

    Discussion

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

    Loading discussion…