First-order logic with least fixed points

FO(LFP) is an instance of the common first-order operator syntax. An arity-k binder adds one k-ary relation and k first-order variables to its body. Other free variables are parameters, fixed throughout the iteration. Terms at the application site are evaluated in the outer scope.

RawFormula includes unchecked syntax; its total interpretation takes the intersection of pre-fixed relations. For nonpositive bodies this need not be a fixed point. Formula bundles the decidable well-formedness condition, checking positive recursion at every nested binder. All fixed-point laws explicitly require positivity, which is proved to imply monotonicity. Negation outside a fixed-point binder and arbitrary nesting remain available.

Main definitions

• shape, policy, interpretation: the LFP instance of the shared operator interface.
• RawFormula, Formula, lfp, Formula.lfp: raw and checked FO(LFP) constructors.
• step, stepHom: the induced relation operator with fixed first-order parameters.

Main results

• step_monotone: syntactic positivity implies semantic monotonicity.
• realize_lfp: LFP semantics agrees with Mathlib's OrderHom.lfp.
• step_lfp, lfp_le: fixed-point and leastness laws.
• iterate_card_pow_eq_lfp: on a domain of size n, arity k stabilizes at stage n^k.

References

• N. Immerman, Descriptive Complexity, Chapter 4.
• N. Immerman, Relational Queries Computable in Polynomial Time, Section 1 (positive nested syntax) and Section 2, Fact 2.1 (the finite-stage bound).

This module implements the logic and finite-stage semantics. The native polynomial-time evaluator is in CslibFrontier.Computability.Complexity.Classes.P.FirstOrder; the ordered characterization is in CslibFrontier.Computability.Complexity.ImmermanVardi.

@[reducible, inline]

abbrev Cslib.Logic.FO.LFP.shape (k : ℕ) : Operator.Shape

A least fixed point binds a relation and a tuple of the same arity.

def Cslib.Logic.FO.LFP.policy : Operator.Policy shape

Least fixed points are monotone in their body and require positive self-reference.

@[reducible, inline]

abbrev Cslib.Logic.FO.LFP.RawFormula (L : FirstOrder.Language) (Γ : List ℕ) (α : Type w) : Type (max u v (w + 1))

FO(LFP) syntax before its recursive positivity conditions have been checked.

@[reducible, inline]

abbrev Cslib.Logic.FO.LFP.Formula (L : FirstOrder.Language) (Γ : List ℕ) (α : Type w) : Type (max 0 (max u v) (w + 1))

FO(LFP) syntax with positive recursion at every nested binder.

def Cslib.Logic.FO.LFP.interpretation {M : Type z} : Operator.Interpretation shape M

Total raw semantics: intersect all pre-fixed relations. The fixed-point laws below require positive bodies; no fixed-point claim is made for invalid raw syntax.

theorem Cslib.Logic.FO.LFP.interpretation_respects {M : Type z} : interpretation.Respects policy.variance

Raw LFP interpretation is monotone in the body transformer, even before checking positivity.

def Cslib.Logic.FO.LFP.lfp {L : FirstOrder.Language} {Γ : List ℕ} {α : Type w} {k : ℕ} (body : RawFormula L (k :: Γ) (α ⊕ Fin k)) (args : Fin k → L.Term α) : RawFormula L Γ α

Apply a raw least-fixed-point binder to a tuple of terms.

def Cslib.Logic.FO.LFP.headMark {Γ : List ℕ} {k : ℕ} : Operator.Marking (k :: Γ)

Mark just the newly bound relation, leaving all outer relations fixed.

def Cslib.Logic.FO.LFP.Positive {L : FirstOrder.Language} {Γ : List ℕ} {α : Type w} {k : ℕ} (body : RawFormula L (k :: Γ) (α ⊕ Fin k)) : Prop

A body is syntactically positive in the relation bound by this LFP.

@[instance_reducible]

instance Cslib.Logic.FO.LFP.instDecidablePositive {L : FirstOrder.Language} {Γ : List ℕ} {α : Type w} {k : ℕ} (body : RawFormula L (k :: Γ) (α ⊕ Fin k)) : Decidable (Positive body)

Positivity is a decidable syntactic property.

theorem Cslib.Logic.FO.LFP.inner_positive_eq_headMark {Γ : List ℕ} {k : ℕ} : (@Operator.Marking.inner Γ [k] fun {k_1 : ℕ} => policy.positive k 0) = @headMark Γ k

The generic local marking specializes to the nearest LFP relation.

@[simp]

theorem Cslib.Logic.FO.LFP.wellFormed_lfp {L : FirstOrder.Language} {Γ : List ℕ} {α : Type w} {k : ℕ} (body : RawFormula L (k :: Γ) (α ⊕ Fin k)) (args : Fin k → L.Term α) : Operator.Formula.wellFormed policy (lfp body args) = true ↔ Operator.Formula.wellFormed policy body = true ∧ Positive body

An LFP is well formed exactly when its body is well formed and positive in its own relation.

def Cslib.Logic.FO.LFP.Formula.lfp {L : FirstOrder.Language} {Γ : List ℕ} {α : Type w} {k : ℕ} (body : Formula L (k :: Γ) (α ⊕ Fin k)) (hpos : Positive ↑body) (args : Fin k → L.Term α) : Formula L Γ α

Construct a checked least fixed point from a checked, positive body.

def Cslib.Logic.FO.LFP.Formula.Realize {L : FirstOrder.Language} {Γ : List ℕ} {α : Type w} {M : Type z} [L.Structure M] (φ : Formula L Γ α) (ρ : Operator.RelEnv Γ M) (v : α → M) : Prop

Realization of a checked FO(LFP) formula.

def Cslib.Logic.FO.LFP.step {L : FirstOrder.Language} {Γ : List ℕ} {α : Type w} {k : ℕ} {M : Type z} [L.Structure M] (body : RawFormula L (k :: Γ) (α ⊕ Fin k)) (ρ : Operator.RelEnv Γ M) (v : α → M) (R : Set (Fin k → M)) : Set (Fin k → M)

The relation operator induced by a body, with its outer assignment and relations fixed.

theorem Cslib.Logic.FO.LFP.step_monotone {L : FirstOrder.Language} {Γ : List ℕ} {α : Type w} {k : ℕ} {M : Type z} [L.Structure M] (body : RawFormula L (k :: Γ) (α ⊕ Fin k)) (hpos : Positive body) (ρ : Operator.RelEnv Γ M) (v : α → M) : Monotone (step body (fun {k : ℕ} => ρ) v)

Positive recursion induces a monotone relation operator.

def Cslib.Logic.FO.LFP.stepHom {L : FirstOrder.Language} {Γ : List ℕ} {α : Type w} {k : ℕ} {M : Type z} [L.Structure M] (body : RawFormula L (k :: Γ) (α ⊕ Fin k)) (hpos : Positive body) (ρ : Operator.RelEnv Γ M) (v : α → M) : Set (Fin k → M) →o Set (Fin k → M)

Bundle the syntactically certified relation operator as a Mathlib order homomorphism.

theorem Cslib.Logic.FO.LFP.realize_lfp {L : FirstOrder.Language} {Γ : List ℕ} {α : Type w} {k : ℕ} {M : Type z} [L.Structure M] (body : RawFormula L (k :: Γ) (α ⊕ Fin k)) (hpos : Positive body) (args : Fin k → L.Term α) (ρ : Operator.RelEnv Γ M) (v : α → M) : Operator.Formula.Realize interpretation (lfp body args) (fun {k : ℕ} => ρ) v ↔ (fun (i : Fin k) => FirstOrder.Language.Term.realize v (args i)) ∈ OrderHom.lfp (stepHom body hpos (fun {k : ℕ} => ρ) v)

A positive raw LFP has the standard least-fixed-point semantics. This rewrites syntax to the mathematical fixed point without recursively unfolding its defining equation.

@[simp]

theorem Cslib.Logic.FO.LFP.Formula.realize_lfp {L : FirstOrder.Language} {Γ : List ℕ} {α : Type w} {k : ℕ} {M : Type z} [L.Structure M] (body : Formula L (k :: Γ) (α ⊕ Fin k)) (hpos : Positive ↑body) (args : Fin k → L.Term α) (ρ : Operator.RelEnv Γ M) (v : α → M) : (body.lfp hpos args).Realize (fun {k : ℕ} => ρ) v ↔ (fun (i : Fin k) => FirstOrder.Language.Term.realize v (args i)) ∈ OrderHom.lfp (stepHom (↑body) hpos (fun {k : ℕ} => ρ) v)

The checked constructor exposes the same fixed-point semantics directly to simplification.

theorem Cslib.Logic.FO.LFP.step_lfp {L : FirstOrder.Language} {Γ : List ℕ} {α : Type w} {k : ℕ} {M : Type z} [L.Structure M] (body : RawFormula L (k :: Γ) (α ⊕ Fin k)) (hpos : Positive body) (ρ : Operator.RelEnv Γ M) (v : α → M) : step body (fun {k : ℕ} => ρ) v (OrderHom.lfp (stepHom body hpos (fun {k : ℕ} => ρ) v)) = OrderHom.lfp (stepHom body hpos (fun {k : ℕ} => ρ) v)

The denotation is a fixed point of the body's actual relation operator.

theorem Cslib.Logic.FO.LFP.lfp_le {L : FirstOrder.Language} {Γ : List ℕ} {α : Type w} {k : ℕ} {M : Type z} [L.Structure M] (body : RawFormula L (k :: Γ) (α ⊕ Fin k)) (hpos : Positive body) (ρ : Operator.RelEnv Γ M) (v : α → M) {R : Set (Fin k → M)} (hR : step body (fun {k : ℕ} => ρ) v R ⊆ R) : OrderHom.lfp (stepHom body hpos (fun {k : ℕ} => ρ) v) ⊆ R

The denotation is contained in every pre-fixed relation: the useful LFP induction rule.

theorem Cslib.Logic.FO.LFP.iterate_card_pow_eq_lfp {L : FirstOrder.Language} {Γ : List ℕ} {α : Type w} {k : ℕ} {M : Type z} [L.Structure M] [Fintype M] (body : RawFormula L (k :: Γ) (α ⊕ Fin k)) (hpos : Positive body) (ρ : Operator.RelEnv Γ M) (v : α → M) : (step body (fun {k : ℕ} => ρ) v)^[Fintype.card M ^ k] ∅ = OrderHom.lfp (stepHom body hpos (fun {k : ℕ} => ρ) v)

A k-ary positive operator on a domain of size n reaches its least fixed point after n^k applications from the empty relation. This includes empty domains and nullary relations.