Lax Lean Archive

While this submission is a draft, it cannot be used by other submissions.

First-order definability without an order

Lax945089.OrderFreeFirstOrder · concepts/Lax945089/OrderFreeFirstOrder.lean · lax-945089

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 order-free first-order definable when there is a first-order sentence φ\varphi over LL alone such that every nonempty finite LL-structure is a yes-instance of PP if and only if it satisfies φ\varphi. No order is available to the sentence, in contrast with FO(≤\le) definability.

    Concept map
    2 concepts; 12 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
    4
    5/-!
    6---
    7title: First-order definability without an order
    8type: definition
    9---
    10A decision problem PP over a relational vocabulary LL is order-free
    11first-order definable when there is a first-order sentence φ\varphi over
    12LL alone such that every nonempty finite LL-structure is a yes-instance of
    13PP if and only if it satisfies φ\varphi. No order is available to the
    14sentence, in contrast with FO(≤\le) definability.
    15-/
    16
    17namespace Lax945089.OrderFreeFirstOrder
    18
    19open Lax904597.Problems
    20
    21open FirstOrder
    22
    23open Language
    24
    25/-- A decision problem is *order-free first-order definable* if a single
    26sentence over its own vocabulary decides it on nonempty finite structures. -/
    27def FODefinableFree {L : Language.{0, 0}} [L.IsRelational] (P : DecisionProblem L) : Prop :=
    28 ∃ φ : L.Sentence, ∀ (A : Type) [L.Structure A] [Finite A] [Nonempty A], P A ↔ A ⊨ φ
    29
    30end Lax945089.OrderFreeFirstOrder
    31
    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…