Lax Lean Archive

Finite relational structures and their properties

Lax988886.FiniteStructures · concepts/Lax988886/FiniteStructures.lean · lax-988886

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 finite relational vocabulary is a finite list of relation arities. A structure has universe FinnFin n and an interpretation of each relation. The numbering is used for binary input encodings; it is not available as an order predicate in the logic. Properties are required to be invariant under isomorphism, so they do not depend on the numbering.

    The representation and dense binary encoding are reused from the Immerman–Vardi submission. Here we forget its distinguished order. Empty universes and nullary relations are allowed.

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

    Lean source view on GitHub

    1import Lax751879.OrderedStructures
    2import Lax751879.StructureEncoding
    3
    4/-!
    5---
    6title: Finite relational structures and their properties
    7type: definition
    8---
    9A finite relational vocabulary is a finite list of relation arities. A
    10structure has universe `Fin n` and an interpretation of each relation.
    11The numbering is used for binary input encodings; it is not available as
    12an order predicate in the logic. Properties are required to be invariant
    13under isomorphism, so they do not depend on the numbering.
    14
    15The representation and dense binary encoding are reused from the
    16Immerman–Vardi submission. Here we forget its distinguished order. Empty
    17universes and nullary relations are allowed.
    18-/
    19
    20namespace Lax988886.FiniteStructures
    21
    22abbrev Vocabulary := Lax751879.OrderedStructures.Vocabulary
    23abbrev Symbol := Lax751879.OrderedStructures.Symbol
    24abbrev Structure := Lax751879.OrderedStructures.OrderedStructure
    25abbrev Interpretation (σ : Vocabulary) (n : Nat) :=
    26 (r : Symbol σ) → (Fin (σ.get r) → Fin n) → Bool
    27abbrev Property (σ : Vocabulary) := Structure σ → Prop
    28
    29structure Isomorphism {σ : Vocabulary} (A B : Structure σ) where
    30 equivalence : Fin A.size ≃ Fin B.size
    31 preserves : ∀ (r : Symbol σ) (a : Fin (σ.get r) → Fin A.size),
    32 B.relation r (equivalence ∘ a) = A.relation r a
    33
    34def IsomorphismInvariant {σ : Vocabulary} (Q : Property σ) : Prop :=
    35 ∀ A B : Structure σ, Nonempty (Isomorphism A B) → (Q A ↔ Q B)
    36
    37def encode {σ : Vocabulary} (A : Structure σ) : List Bool :=
    38 Lax751879.StructureEncoding.encode ⟨A, Fin.elim0⟩
    39
    40def language {σ : Vocabulary} (Q : Property σ) (w : List Bool) : Prop :=
    41 ∃ A : Structure σ, encode A = w ∧ Q A
    42
    43end Lax988886.FiniteStructures
    44
    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…