Lax Lean Archive

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

Environment v4.30.0. The archive's epoch is v4.33.0; only submissions in v4.30.0 can cite this work.

Semantics of monadic second-order logic

Lax52.MSOSemantics · concepts/Lax52/MSOSemantics.lean · lax-52

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

    The satisfaction relation for monadic second-order formulas over an arbitrary first-order structure. First-order terms and relation symbols are interpreted by mathlib's first-order semantics, while a monadic valuation assigns a set of elements to every monadic variable.

    Concept map
    2 concepts
    100%
    DefinitionThis conceptRelated conceptA → B: B builds on ADescendants are omitted for concepts with more than 10 descendants.

    Lean source view on GitHub

    1import Lax52.MSOSyntax
    2
    3/-!
    4---
    5title: Semantics of monadic second-order logic
    6type: definition
    7---
    8
    9The satisfaction relation for monadic second-order formulas over an arbitrary
    10first-order structure. First-order terms and relation symbols are interpreted
    11by mathlib's first-order semantics, while a monadic valuation assigns a set of
    12elements to every monadic variable.
    13-/
    14
    15namespace Lax52.MSOSemantics
    16
    17open FirstOrder
    18open FirstOrder.Language
    19open FirstOrder.Language.Structure
    20open Lax52.MSOSyntax
    21
    22universe u v w
    23
    24variable {L : Language.{u, v}} {M : Type w} [L.Structure M]
    25
    26/-- Extend a valuation by putting a newly bound variable at index zero. -/
    27def consVal {n : Nat} (x : M) (v : Fin n → M) : Fin (n + 1) → M :=
    28 Fin.cases x v
    29
    30/-- Satisfaction of an MSO formula under first-order and monadic valuations. -/
    31def Realize : {n m : Nat} → Formula L n m → (Fin n → M) →
    32 (Fin m → Set M) → Prop
    33 | _, _, .falsum, _, _ => False
    34 | _, _, .equal t₁ t₂, v, _ => t₁.realize v = t₂.realize v
    35 | _, _, .rel r ts, v, _ => RelMap r (fun i => (ts i).realize v)
    36 | _, _, .mem t X, v, V => t.realize v ∈ V X
    37 | _, _, .or phi psi, v, V => Realize phi v V ∨ Realize psi v V
    38 | _, _, .neg phi, v, V => ¬Realize phi v V
    39 | _, _, .exFO phi, v, V => ∃ x : M, Realize phi (consVal x v) V
    40 | _, _, .exSO phi, v, V => ∃ X : Set M, Realize phi v (consVal X V)
    41
    42end Lax52.MSOSemantics
    43
    Builds on
    Used by
    From Mathlib

    none

    Discussion

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

    Loading discussion…