Lax Lean Archive

First-order logic with least fixed points

Lax751879.FixedPointSyntax · concepts/Lax751879/FixedPointSyntax.lean · lax-751879

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(LFP) extends first-order logic with [lfp⁡R,xˉ φ](yˉ)[\operatorname{lfp}_{R,\bar x}\,\varphi](\bar y), where every occurrence of RR in φ\varphi is positive (under an even number of negations). Fixed points may be nested, negated, and have free first-order parameters. Equality, order, relation atoms, negation, conjunction, and existential quantification form the first-order basis; truth is included explicitly.

    The indices record the number of available element variables and the arities of available relation variables. A quantifier binds element variable zero. A fixed point binds relation variable zero and the first kk element variables of its body; the remaining variables are parameters.

    Raw syntax is separated from admissibility solely to express the positivity check. A FormulaFormula always includes admissibility at every nested fixed point. positiveAtpositiveAt traverses nested binders, shifting the relation-variable index, and tracks the parity of negations.

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

    Lean source view on GitHub

    1import Lax751879.OrderedStructures
    2
    3/-!
    4---
    5title: First-order logic with least fixed points
    6type: definition
    7---
    8FO(LFP) extends first-order logic with
    9[lfp⁡R,xˉ φ](yˉ)[\operatorname{lfp}_{R,\bar x}\,\varphi](\bar y), where every occurrence
    10of RR in φ\varphi is positive (under an even number of negations).
    11Fixed points may be nested, negated, and have free first-order parameters.
    12Equality, order, relation atoms, negation, conjunction, and existential
    13quantification form the first-order basis; truth is included explicitly.
    14
    15The indices record the number of available element variables and the arities
    16of available relation variables. A quantifier binds element variable zero.
    17A fixed point binds relation variable zero and the first kk element
    18variables of its body; the remaining variables are parameters.
    19
    20Raw syntax is separated from admissibility solely to express the positivity
    21check. A `Formula` always includes admissibility at every nested fixed point.
    22`positiveAt` traverses nested binders, shifting the relation-variable index,
    23and tracks the parity of negations.
    24-/
    25
    26namespace Lax751879.FixedPointSyntax
    27
    28open Lax751879.OrderedStructures
    29
    30inductive RawFormula (σ : Vocabulary) : Nat → List Nat → Type
    31 | truth {m ρ} : RawFormula σ m ρ
    32 | equal {m ρ} (x y : Fin m) : RawFormula σ m ρ
    33 | less {m ρ} (x y : Fin m) : RawFormula σ m ρ
    34 | relation {m ρ} (r : Symbol σ) (args : Fin (σ.get r) → Fin m) :
    35 RawFormula σ m ρ
    36 | variable {m ρ} (r : Fin ρ.length) (args : Fin (ρ.get r) → Fin m) :
    37 RawFormula σ m ρ
    38 | neg {m ρ} (φ : RawFormula σ m ρ) : RawFormula σ m ρ
    39 | conj {m ρ} (φ ψ : RawFormula σ m ρ) : RawFormula σ m ρ
    40 | exists' {m ρ} (φ : RawFormula σ (m + 1) ρ) : RawFormula σ m ρ
    41 | lfp {m ρ} (k : Nat) (body : RawFormula σ (k + m) (k :: ρ))
    42 (args : Fin k → Fin m) : RawFormula σ m ρ
    43
    44/-- Every occurrence of `r` has the required polarity. `true` means positive. -/
    45def RawFormula.positiveAt {σ : Vocabulary} {m : Nat} {ρ : List Nat}
    46 (φ : RawFormula σ m ρ) (r : Fin ρ.length) (polarity : Bool) : Prop :=
    47 match φ with
    48 | .truth | .equal _ _ | .less _ _ | .relation _ _ => True
    49 | .variable s _ => s = r → polarity = true
    50 | .neg ψ => ψ.positiveAt r (!polarity)
    51 | .conj ψ χ => ψ.positiveAt r polarity ∧ χ.positiveAt r polarity
    52 | .exists' ψ => ψ.positiveAt r polarity
    53 | .lfp _ body _ => body.positiveAt r.succ polarity
    54
    55/-- Every fixed-point binder has a positive defining body. -/
    56def RawFormula.Admissible {σ : Vocabulary} {m : Nat} {ρ : List Nat}
    57 (φ : RawFormula σ m ρ) : Prop :=
    58 match φ with
    59 | .truth | .equal _ _ | .less _ _ | .relation _ _ | .variable _ _ => True
    60 | .neg ψ | .exists' ψ => ψ.Admissible
    61 | .conj ψ χ => ψ.Admissible ∧ χ.Admissible
    62 | .lfp _ body _ => body.Admissible ∧ body.positiveAt 0 true
    63
    64abbrev Formula (σ : Vocabulary) (m : Nat) :=
    65 {φ : RawFormula σ m [] // φ.Admissible}
    66
    67abbrev Sentence (σ : Vocabulary) := Formula σ 0
    68
    69end Lax751879.FixedPointSyntax
    70
    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…