Lax Lean Archive

Positive first-order logic on finite words

Lax503819.PositiveLogic · concepts/Lax503819/PositiveLogic.lean · lax-503819

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

    FO⁺ has upward letter tests, the two order tests ≤ and <, conjunction, disjunction, and existential and universal quantification over positions. There is no negation of letter tests. A language is FO⁺-definable when one sentence defines it on all finite words, including the empty word.

    FormulaAnFormula A n has n available free variables. A quantifier adds variable 0 and shifts the existing variables. Truth and falsity are included as empty conjunction and disjunction; they are also expressible by quantified order tests. On a powerset alphabet the test for S means that every predicate in S holds at that position, precisely the convention in Section 3.1.

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

    Lean source view on GitHub

    1import Lax503819.Words
    2import Mathlib.Data.Fin.Tuple.Basic
    3
    4/-!
    5---
    6title: Positive first-order logic on finite words
    7type: definition
    8---
    9FO⁺ has upward letter tests, the two order tests ≤ and <, conjunction,
    10disjunction, and existential and universal quantification over positions.
    11There is no negation of letter tests. A language is FO⁺-definable when one
    12sentence defines it on all finite words, including the empty word.
    13
    14`Formula A n` has n available free variables. A quantifier adds variable 0
    15and shifts the existing variables. Truth and falsity are included as empty
    16conjunction and disjunction; they are also expressible by quantified order
    17tests. On a powerset alphabet the test for S means that every predicate in S
    18holds at that position, precisely the convention in Section 3.1.
    19-/
    20
    21namespace Lax503819.PositiveLogic
    22
    23open Lax503819.Words
    24
    25inductive Formula (A : Type) : ℕ → Type where
    26 | truth {n} : Formula A n
    27 | falsity {n} : Formula A n
    28 | letter {n} : A → Fin n → Formula A n
    29 | le {n} : Fin n → Fin n → Formula A n
    30 | lt {n} : Fin n → Fin n → Formula A n
    31 | conj {n} : Formula A n → Formula A n → Formula A n
    32 | disj {n} : Formula A n → Formula A n → Formula A n
    33 | exists_ {n} : Formula A (n + 1) → Formula A n
    34 | forall_ {n} : Formula A (n + 1) → Formula A n
    35
    36def Formula.Realize {A : Type} [LE A] {n : ℕ}
    37 (φ : Formula A n) (w : List A) (ρ : Fin n → Position w) : Prop :=
    38 match φ with
    39 | .truth => True
    40 | .falsity => False
    41 | .letter a x => a ≤ w.get (ρ x)
    42 | .le x y => ρ x ≤ ρ y
    43 | .lt x y => ρ x < ρ y
    44 | .conj φ ψ => φ.Realize w ρ ∧ ψ.Realize w ρ
    45 | .disj φ ψ => φ.Realize w ρ ∨ ψ.Realize w ρ
    46 | .exists_ φ => ∃ i : Position w, φ.Realize w (Fin.cons i ρ)
    47 | .forall_ φ => ∀ i : Position w, φ.Realize w (Fin.cons i ρ)
    48
    49def Formula.rank {A : Type} {n : ℕ} : Formula A n → ℕ
    50 | .truth | .falsity | .letter _ _ | .le _ _ | .lt _ _ => 0
    51 | .conj φ ψ | .disj φ ψ => max φ.rank ψ.rank
    52 | .exists_ φ | .forall_ φ => φ.rank + 1
    53
    54def sentenceLanguage {A : Type} [LE A] (φ : Formula A 0) : Language A :=
    55 {w | φ.Realize w Fin.elim0}
    56
    57def Definable {A : Type} [LE A] (L : Language A) : Prop :=
    58 ∃ φ : Formula A 0, sentenceLanguage φ = L
    59
    60end Lax503819.PositiveLogic
    61
    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…