Lax Lean Archive

Draft — mutable and not usable as a dependency; its citation marks the draft state.

Lax678846.Fagin

Fagin’s theorem

concepts/Lax678846/Fagin.lean · lax-678846

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.

    Concept map

    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.

    1st statement capturesNP proven

    2nd statement definableInNP proven

    3rd statement npDefinable proven

    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.

    Lean source view on GitHub

    1import Lax678846.ExistentialSecondOrder
    2import Lax678846.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 Lax678846.Fagin
    26
    27open Lax678846.FiniteStructures Lax678846.ExistentialSecondOrder
    28open Lax678846.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 Lax678846.Fagin
    39
    Show ProofShow ProofShow Proof

    Builds on

    Used by

    none

    From Mathlib

    none

    Community review

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above; your ORCID profile must share a public name.

    0 comments

    Loading discussion…