Lax Lean Archive

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

Lax52.MSOSemantics

Semantics of monadic second-order logic

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.

    Concept map

    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

    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.

    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

    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…