Lax Lean Archive

Semantics of monadic second-order logic

Lax146103.MSOSemantics · concepts/Lax146103/MSOSemantics.lean · lax-146103

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; 11 descendants hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

    Lean source view on GitHub

    1import Lax146103.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 Lax146103.MSOSemantics
    16
    17open FirstOrder
    18open FirstOrder.Language
    19open FirstOrder.Language.Structure
    20open Lax146103.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 Lax146103.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…