Lax Lean Archive

Fagin’s theorem

Lax988886.Fagin · concepts/Lax988886/Fagin.lean · lax-988886

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 relational structures, existential second-order logic captures NP. Every existential second-order sentence defines a property in NP; every isomorphism-invariant property in NP has an existential second-order definition. No order on the input structure is assumed. The vocabulary is arbitrary but fixed independently of the input.

    The computational and expressive directions are stated separately as well as together. Their proofs must supply the certificate verifier and the logical encoding of accepting computations, including any chosen auxiliary order. None of those constructions is an assumption of the theorem.

    References: Fagin, Generalized first-order spectra and polynomial-time recognizable sets (1974); Libkin, Elements of Finite Model Theory, Theorem 9.6 and its proof in Section 9.2.

    Concept map
    6 concepts
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

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

    1 capturesNP proven

    2 definableInNP proven

    3 npDefinable proven

    Lean source view on GitHub

    1import Lax988886.ExistentialSecondOrder
    2import Lax988886.NondeterministicPolynomialTime
    3
    4/-!
    5---
    6title: Fagin’s theorem
    7type: theorem
    8---
    9On finite relational structures, existential second-order logic captures NP.
    10Every existential second-order sentence defines a property in NP; every
    11isomorphism-invariant property in NP has an existential second-order
    12definition. No order on the input structure is assumed. The vocabulary is
    13arbitrary but fixed independently of the input.
    14
    15The computational and expressive directions are stated separately as well
    16as together. Their proofs must supply the certificate verifier and the
    17logical encoding of accepting computations, including any chosen auxiliary
    18order. None of those constructions is an assumption of the theorem.
    19
    20References: Fagin, *Generalized first-order spectra and polynomial-time
    21recognizable sets* (1974); Libkin, *Elements of Finite Model Theory*,
    22Theorem 9.6 and its proof in Section 9.2.
    23-/
    24
    25namespace Lax988886.Fagin
    26
    27open Lax988886.FiniteStructures Lax988886.ExistentialSecondOrder
    28open Lax988886.NondeterministicPolynomialTime
    29
    30axiom definableInNP {σ : Vocabulary} (Q : Property σ) : Definable Q → InNP Q
    31
    32axiom npDefinable {σ : Vocabulary} (Q : Property σ)
    33 (hQ : IsomorphismInvariant Q) : InNP Q → Definable Q
    34
    35axiom capturesNP {σ : Vocabulary} (Q : Property σ)
    36 (hQ : IsomorphismInvariant Q) : Definable Q ↔ InNP Q
    37
    38end Lax988886.Fagin
    39
    Show 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…