Lax Lean Archive

First-order definability on ordered structures

Lax485149.FirstOrderDefinability · concepts/Lax485149/FirstOrderDefinability.lean · lax-485149

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 PP over a relational vocabulary LL is FO(≤\le) definable when there is a first-order sentence φ\varphi over L∪{≤}L \cup \{\le\} such that, for every nonempty finite LL-structure AA and every linear order on AA, AA is a yes-instance of PP if and only if (A,≤)⊨φ(A, \le) \models \varphi. The sentence may use the order; the problem does not depend on it.

    Concept map
    3 concepts; 21 descendants hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

    Lean source view on GitHub

    1import Mathlib.ModelTheory.Order
    2import Mathlib.ModelTheory.Semantics
    3import Lax904597.Problems
    4import Lax904597.Interpretations
    5
    6/-!
    7---
    8title: First-order definability on ordered structures
    9type: definition
    10---
    11A decision problem PP over a relational vocabulary LL is FO(≤\le)
    12definable when there is a first-order sentence φ\varphi over
    13L∪{≤}L \cup \{\le\} such that, for every nonempty finite LL-structure AA
    14and every linear order on AA, AA is a yes-instance of PP if and only if
    15(A,≤)⊨φ(A, \le) \models \varphi. The sentence may use the order; the problem
    16does not depend on it.
    17-/
    18
    19namespace Lax485149.FirstOrderDefinability
    20
    21open Lax904597.Problems
    22
    23open FirstOrder
    24
    25open Language
    26
    27variable {L : Language.{0, 0}} [L.IsRelational]
    28
    29/-- A decision problem is *FO(≤) definable* if a single sentence over the
    30ordered expansion of its vocabulary decides it on nonempty finite ordered
    31structures. The equivalence is required for
    32*every* linear order, so the notion is order-invariant: the sentence sees the
    33order, the problem does not. -/
    34def FODefinable (P : DecisionProblem L) : Prop :=
    35 ∃ φ : (L.sum Language.order).Sentence,
    36 ∀ (A : Type) [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A], P A ↔ A ⊨ φ
    37
    38end Lax485149.FirstOrderDefinability
    39
    Builds on
    Used by
    From Mathlib

    Discussion

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

    Loading discussion…