Lax Lean Archive

Decision problems on finite structures

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

definition

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

    Definition

    A decision problem over a relational vocabulary LL is an isomorphism-invariant property of LL-structures: for each universe AA carrying an LL-structure, whether AA is a yes-instance, with the requirement that isomorphic structures are both yes-instances or both no-instances. Invariance is part of the notion, as in finite model theory: a problem cannot tell apart two presentations of the same structure. Finiteness is not built in; it is a hypothesis of every statement that needs it, and every complexity-theoretic notion below reads a problem on its finite instances only.

    Concept map
    1 concept; 9 descendants hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

    Lean source view on GitHub

    1import Mathlib.ModelTheory.Semantics
    2
    3/-!
    4---
    5title: Decision problems on finite structures
    6type: definition
    7---
    8A decision problem over a relational vocabulary LL is an
    9isomorphism-invariant property of LL-structures: for each universe AA
    10carrying an LL-structure, whether AA is a yes-instance, with the
    11requirement that isomorphic structures are both yes-instances or both
    12no-instances. Invariance is part of the notion, as in finite model theory: a
    13problem cannot tell apart two presentations of the same structure.
    14Finiteness is not built in; it is a hypothesis of every statement that needs
    15it, and every complexity-theoretic notion below reads a problem on its
    16finite instances only.
    17-/
    18
    19namespace Lax904597.Problems
    20
    21open FirstOrder FirstOrder.Language
    22
    23/-- A decision problem: an isomorphism-closed property of `L`-structures,
    24whose yes-instances are the `L`-structures satisfying it. -/
    25structure DecisionProblem (L : Language.{0, 0}) [L.IsRelational] where
    26 /-- The predicate: `P A` (through the function coercion) states that the
    27 structure `A` is a yes-instance. -/
    28 Holds : ∀ (A : Type) [L.Structure A], Prop
    29 /-- Decision problems do not distinguish isomorphic structures. -/
    30 iso_invariant : ∀ {A B : Type} [L.Structure A] [L.Structure B],
    31 (A ≃[L] B) → (Holds A ↔ Holds B)
    32
    33namespace DecisionProblem
    34
    35variable {L : Language.{0, 0}} [L.IsRelational]
    36
    37instance instCoeFun : CoeFun (DecisionProblem L) fun _ => ∀ (A : Type) [L.Structure A], Prop :=
    38 ⟨Holds⟩
    39
    40end DecisionProblem
    41
    42end Lax904597.Problems
    43
    Builds on

    none

    Used by
    From Mathlib

    Discussion

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

    Loading discussion…