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, with LFP = PFP iff P = PSPACE.
Formalism.
Least Fixed Point (LFP): LFP_{R,x̄} φ(R, x̄)
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))
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 |
|---|---|---|---|
| ¹ | U+00B9 | Superscript one | Second-order level marker in Π¹₁ |
| Π | U+03A0 | Greek capital pi | Universal level of the analytical hierarchy |
| μ | U+03BC | Greek small mu | Least fixed point, in the modal notation |
| ν | U+03BD | Greek small nu | Greatest fixed point |
| φ | U+03C6 | Greek small phi | The formula defining the operator |
| ω | U+03C9 | Greek small omega | The first infinite ordinal; closure stage |
| ᵢ | U+1D62 | Subscript i | Stage index under the union ⋃ᵢ |
| ⁰ | U+2070 | Superscript zero | The zeroth stage, R⁰ |
| ⁱ | U+2071 | Superscript i | The i-th stage, Rⁱ |
| ₁ | U+2081 | Subscript one | Level marker in Π¹₁ |
| ℕ | U+2115 | Double-struck capital N | The natural numbers |
| ∃ | U+2203 | There exists | Existential quantifier |
| ∅ | U+2205 | Empty set | The zeroth stage |
| ∞ | U+221E | Infinity | Infinitary logic L^ω_∞ω |
| ∧ | U+2227 | Logical and | Conjunction |
| ∨ | U+2228 | Logical or | Disjunction |
| ∪ | U+222A | Union | Accumulation of stages in IFP |
| ⊆ | U+2286 | Subset of or equal to | Monotonicity of the operator |
| ⊊ | U+228A | Proper subset | Strict containment of logics or classes |
| ⋃ | U+22C3 | N-ary union | Union of all stages |
| LFP | — | Least fixed point | Smallest R with R = φ(R); requires positivity |
| IFP | — | Inflationary fixed point | Each stage adds to the last; no positivity needed |
| PFP | — | Partial fixed point | The limit if the iteration converges, else empty |
| R | — | Relation variable | The relation being defined inductively |
| x̄, t̄ | — | Tuple notation | Sequences of variables and of terms |
| Rⁱ | — | Stage | The i-th approximation of the fixed point |
| Π¹₁ | — | Pi-one-one | Analytical class of the inductive relations over ℕ |
| TC, E | — | Transitive closure, edge | The standard example predicate and its base relation |
| u, v, x, y, z | — | Individual variables | Vertices in the transitive-closure example |
| L^ω_∞ω | — | Infinitary finite-variable logic | Upper bound on LFP without order |
| < | — | Strict containment | FO < LFP in the stated hierarchy |
Metatheory. Gurevich and Shelah (1986) proved LFP = IFP on finite structures, so the positivity requirement costs nothing there. Vardi (1982) and Immerman (1986) independently proved that LFP captures polynomial time on ordered finite structures, and that PFP captures PSPACE; Abiteboul and Vianu (1989) showed the two logics coincide exactly when P = PSPACE, so separating the logics would separate the classes. Without a linear order the capture fails: every LFP formula is equivalent to one of the finite-variable infinitary logic L^ω_∞ω (Kolaitis and Vardi), and parity of the universe is not, so LFP ⊊ P on unordered structures. Blass, Gurevich and Kozen (1985) proved a 0-1 law for fixed-point logic. Data complexity is polynomial and combined complexity EXPTIME-complete. Over ℕ the LFP-definable relations are exactly the Π¹₁ relations (Moschovakis). Monadic second-order logic and LFP are incomparable.
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. The dependence on order is not a technicality but the open problem of the field: whether any logic captures polynomial time on unordered finite structures is unresolved and was conjectured negative by Gurevich (1988), and LFP's inability to express the parity of the universe shows that the obvious candidate does not do it. Counting extensions such as LFP+C fail as well, by the Cai–Fürer–Immerman construction. LFP requires the relation variable to occur positively, so inductive definitions involving negation fall outside it; IFP admits them, but its stage sequence is no longer a fixpoint iteration of a monotone operator. Over infinite structures closure need not occur at ω, and LFP over ℕ reaches Π¹₁, far past anything recursively axiomatizable. Compactness fails, since reachability is definable, and satisfiability is undecidable, inherited from first-order logic.
© 2026 Lingenic LLC