# Fixed-Point Logic

**Origin.** Fixed-point extensions of first-order logic emerged in 1970s-80s. LFP (least fixed point) and IFP (inflationary fixed point) capture P on ordered structures (Immerman, Vardi). Connects logic and complexity theory. Foundation for descriptive complexity.

**Models.** Inductive definitions via fixed points. First-order logic cannot express transitive closure. Fixed-point operators allow recursive definitions. LFP: iterate until least fixed point. On finite structures: captures polynomial time (with order). Hierarchy: FO < LFP = IFP = PFP on ordered structures.

**Formalism.**

*Least Fixed Point (LFP):*
[LFP_{R,x̄} φ(R, x̄)](t̄)

R is a relation variable (positive in φ).
Meaning: smallest R such that R = φ(R).
Applied to tuple t̄.

*Semantics:*
Define R⁰ = ∅, R^{i+1} = φ(R^i).
LFP = ⋃ᵢ Rⁱ (least fixed point).
Monotone: R ⊆ φ(R) ensures convergence.

*Example — transitive closure:*
TC(E)(x,y) = [LFP_{T,u,v} (E(u,v) ∨ ∃z.T(u,z) ∧ T(z,v))](x,y)

*Inflationary Fixed Point (IFP):*
R^{i+1} = R^i ∪ φ(R^i) (always grows)
Doesn't require positivity.
On finite structures: IFP = LFP.

*Partial Fixed Point (PFP):*
Iterate until fixed point or cycle.
Captures PSPACE on ordered structures.

*Nesting:*
Fixed points can be nested.
Alternation hierarchy for complexity.

**Symbols.**

| Symbol | Unicode | Name | Meaning |
|--------|---------|------|---------|
| LFP | — | Least fixed point | Smallest solution |
| IFP | — | Inflationary FP | Always-growing |
| PFP | — | Partial FP | If converges |
| μ | U+03BC | Mu | Least FP (alternative) |
| ν | U+03BD | Nu | Greatest FP |
| R | — | Relation variable | Recursive relation |
| ⊆ | U+2286 | Subset | Monotonicity |

**Metatheory.** LFP = IFP on finite structures. LFP captures P on ordered structures (Immerman-Vardi). PFP captures PSPACE on ordered structures. Without order: LFP ⊊ P. Over all structures (infinite): LFP ⊊ Δ¹₁. Monadic second-order logic incomparable to LFP. Relates to Datalog (stratified negation).

**Applies to.** Descriptive complexity theory. Database query languages (Datalog). Program verification (reachability). Graph algorithms (connectivity). Knowledge representation (inductive definitions). Model checking (relation to μ-calculus).

**Limitations.** Order required for full P-capture. Infinite structures: convergence issues. Positive occurrence requirement for LFP. Complexity bounds not tight without order. Syntax less natural than recursion schemes. Proof theory less developed than FO.

© 2026 Lingenic LLC