Lax Lean Archive

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

Lax979537.FixedPointSyntax

First-order logic with least fixed points

concepts/Lax979537/FixedPointSyntax.lean · lax-979537

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

    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.

    Lean source view on GitHub

    1import Lax979537.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 Lax979537.FixedPointSyntax
    27
    28open Lax979537.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 Lax979537.FixedPointSyntax
    70

    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…