Lax Lean Archive

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

NP and PTIME are the textbook classes on bit strings

Lax832283.MachineBridge · concepts/Lax832283/MachineBridge.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 the language of the binary encodings of its yes-instances has polynomially bounded certificates checked by a polynomial-time Mathlib machine, and in PTIME exactly when a polynomial-time Mathlib machine decides that language. The encodings of the yes-instances of SAT and of HORN-SAT are examples, for any numbering of their vocabulary.

    Concept map
    40 concepts
    100%
    The classes L and coLThe classes NL and coNLThe complement of a decision problemFirst-order logic with a deterministictransitive closureThe Krom fragment of existentialsecond-order logicProblems given by a property of structuresAtoms in second-order relation variablesFirst-order logic with a transitive closureThe circuit value problemThe classes PTIME and coPTIMEAcceptance by deterministic Turing machinesGAME, alternating reachabilityThe Horn fragment of existentialsecond-order logicSatisfiability of Horn formulasHORN-SAT is PTIME-completeFirst-order logic with inflationary fixedpointsFirst-order logic with least fixed pointsPolynomial-time evaluation of fixed-pointqueriesSemantics and definability in FO(LFP)First-order logic with least fixed pointsThe Immerman–Vardi theoremLeast fixed points on finite relationsFinite ordered relational structures andqueriesPolynomial-time queries on orderedstructuresBinary encodings of ordered structures andtuplesNP and PTIME against the logics of the twoentriesNP and PTIME are the textbook classes onbit stringsDecision problems of the core on bit stringsComplexity classes, cofinal hardness, and NPThe Cook–Levin theorem, by first-orderreductionsFirst-order interpretations and first-orderreductionsNondeterministic Turing machines as finitestructuresDecision problems on finite structuresRelativized first-order interpretationsSAT, propositional satisfiabilitySecond-order definability with boundedalternationExistential second-order logicFagin’s theoremFinite relational structures and theirpropertiesNP through polynomially boundedcertificates
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

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

    1 HORNSAT_inP proven

    2 mem_NP_iff_inNP proven

    3 mem_NP_iff_languageInNP proven

    4 mem_PTIME_iff_inP proven

    5 SAT_languageInNP proven

    Lean source view on GitHub

    1import Lax832283.LogicalBridge
    2import Lax904597.CookLevin
    3import Lax535992.HornSatPTIMEComplete
    4import Lax751879.ImmermanVardi
    5import Lax988886.Fagin
    6
    7/-!
    8---
    9title: NP and PTIME are the textbook classes on bit strings
    10type: theorem
    11---
    12A decision problem is in NP exactly when the language of the binary encodings of its
    13yes-instances has polynomially bounded certificates checked by a polynomial-time Mathlib
    14machine, and in PTIME exactly when a polynomial-time Mathlib machine decides that language.
    15The encodings of the yes-instances of SAT and of HORN-SAT are examples, for any numbering of
    16their vocabulary.
    17-/
    18
    19namespace Lax832283.MachineBridge
    20
    21open FirstOrder Lax904597.Problems Lax904597.Classes Lax535992.ClassPTIME
    22open Lax832283.StringProblems Lax988886.FiniteStructures
    23open Lax988886.NondeterministicPolynomialTime Lax751879.PolynomialTime
    24
    25/-- NP is the textbook class. -/
    26axiom mem_NP_iff_inNP {L : Language.{0, 0}} [L.IsRelational] (V : FinVocab L)
    27 (P : DecisionProblem L) : NP.Mem P ↔ InNP (toProperty V P)
    28
    29/-- NP, on bit strings. -/
    30axiom mem_NP_iff_languageInNP {L : Language.{0, 0}} [L.IsRelational] (V : FinVocab L)
    31 (P : DecisionProblem L) :
    32 NP.Mem P ↔ LanguageInNP (Lax988886.FiniteStructures.language (toProperty V P))
    33
    34/-- PTIME is the textbook class. -/
    35axiom mem_PTIME_iff_inP {L : Language.{0, 0}} [L.IsRelational] (V : FinVocab L)
    36 (P : DecisionProblem L) : PTIME.Mem P ↔ InP (toQuery V P)
    37
    38/-- The encodings of satisfiable CNF instances form a language in NP. -/
    39axiom SAT_languageInNP (V : FinVocab Lax904597.Sat.sat) :
    40 LanguageInNP (Lax988886.FiniteStructures.language (toProperty V Lax904597.Sat.SAT))
    41
    42/-- A polynomial-time machine decides the encodings of the satisfiable Horn instances. -/
    43axiom HORNSAT_inP (V : FinVocab Lax904597.Sat.sat) :
    44 InP (toQuery V Lax535992.HornSat.HORNSAT)
    45
    46end Lax832283.MachineBridge
    47
    Show ProofShow ProofShow ProofShow 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…