Lax Lean Archive

The Cook–Levin theorem, in its machine form

Lax904597.MachineForm · concepts/Lax904597/MachineForm.lean · lax-904597

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

    Machine acceptance – does a nondeterministic Turing machine, given as a finite structure, accept its input in fewer steps than there are positions? – is interreducible with SAT, and characterizes NP: a problem is existential second-order definable exactly when it has an ordered first-order reduction to machine acceptance.

    Together with the machine-free Cook–Levin theorem this gives the statement in machine terms: SAT is NP-complete for NP read as nondeterministic polynomial time, where the time available to a machine is the number of positions of the structure a reduction builds, polynomial in the input – the bound is unary by construction – and where the reduction from a machine to a formula is the usual tableau, built here as a first-order interpretation.

    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 mem_NP_iff_le_ntmAccept proven

    2 SAT_complete_for_ntmAccept proven

    Lean source view on GitHub

    1import Lax904597.Classes
    2import Lax904597.Sat
    3import Lax904597.Machines
    4
    5/-!
    6---
    7title: The Cook–Levin theorem, in its machine form
    8type: theorem
    9---
    10Machine acceptance – does a nondeterministic Turing machine, given as a
    11finite structure, accept its input in fewer steps than there are
    12positions? – is interreducible with SAT, and characterizes NP: a problem is
    13existential second-order definable exactly when it has an ordered
    14first-order reduction to machine acceptance.
    15
    16Together with the machine-free Cook–Levin theorem this gives the statement
    17in machine terms: SAT is NP-complete for NP read as nondeterministic
    18polynomial time, where the time available to a machine is the number of
    19positions of the structure a reduction builds, polynomial in the input –
    20the bound is unary by construction – and where the reduction from a machine
    21to a formula is the usual tableau, built here as a first-order
    22interpretation.
    23-/
    24
    25namespace Lax904597.MachineForm
    26
    27open FirstOrder FirstOrder.Language
    28open Lax904597.Problems Lax904597.Interpretations Lax904597.SecondOrder Lax904597.Classes
    29 Lax904597.Sat Lax904597.Machines
    30
    31/-- SAT reduces to machine acceptance, by the machine that guesses an
    32assignment and checks the clauses; and whatever reduces to machine
    33acceptance reduces to SAT, by the tableau of the machine as a first-order
    34interpretation. -/
    35axiom SAT_complete_for_ntmAccept : ∀ (h : NTMAcceptInvariant),
    36 Nonempty (OrderedFOReduction SAT (NTMAccept h)) ∧
    37 ∀ {L : Language.{0, 0}} [L.IsRelational] (P : DecisionProblem L),
    38 Nonempty (OrderedFOReduction P (NTMAccept h)) → Nonempty (OrderedFOReduction P SAT)
    39
    40/-- NP, as existential second-order definability, is the class of problems
    41that reduce to machine acceptance. -/
    42axiom mem_NP_iff_le_ntmAccept : ∀ (h : NTMAcceptInvariant)
    43 {L : Language.{0, 0}} [L.IsRelational] (P : DecisionProblem L),
    44 NP.Mem P ↔ Nonempty (OrderedFOReduction P (NTMAccept h))
    45
    46end Lax904597.MachineForm
    47
    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…