Fixed-point logic
Fixed-point logic is a family of formal systems that extend a base logic with operators defining relations as fixed points of relation-transforming expressions. In finite model theory, the base system is usually first-order logic, while in modal settings it is commonly a modal logic. Fixed-point operators permit formulas to express inductive and recursive properties that first-order formulas cannot define uniformly over finite structures.
The central semantic construction begins with a formula whose distinguished relation variable occurs positively. Positivity makes the associated operator monotone with respect to set inclusion. The Knaster–Tarski theorem then supplies a least fixed point and a greatest fixed point on the complete lattice of relations of the appropriate arity.
Fixed-point logic is closely connected with descriptive complexity, where logical definability is compared with computational complexity. Over finite structures equipped with a linear order, least fixed-point logic characterizes deterministic polynomial time.
Least fixed-point logic
Let (\varphi(R,\bar{x})) be a first-order formula in which (R) is a (k)-ary relation variable and (\bar{x}) is a (k)-tuple of individual variables. For a structure (\mathcal A), the formula determines an operator
[ F_\varphi(S)= {\bar{a}\in A^k : \mathcal A\models\varphi(S,\bar{a})}. ]
When every free occurrence of (R) in (\varphi) is positive, the operator (F_\varphi) is monotone. Its least fixed point is denoted by
[ \operatorname{LFP}_{R,\bar{x}}\varphi. ]
This formula holds when the tuple denoted by (\bar{t}) belongs to the least relation (S) satisfying (F_\varphi(S)=S). The resulting extension of first-order logic is called first-order logic with a least fixed-point operator, conventionally abbreviated as FO(LFP).
On a finite structure, the least fixed point is reached by iterating the operator from the empty relation:
[ S_0=\varnothing,\qquad S_{i+1}=F_\varphi(S_i). ]
Monotonicity gives (S_i\subseteq S_{i+1}). Since only finitely many (k)-tuples exist, the sequence eventually stabilizes, and the stable relation is the least fixed point. The number of strict stages is at most (|A|^k), although particular formulas often stabilize earlier.
A standard example is graph reachability. For a directed graph with edge relation (E), the formula
[ \varphi(R,x,y) \equiv E(x,y)\lor \exists z\bigl(R(x,z)\land E(z,y)\bigr) ]
defines an operator whose least fixed point is the transitive closure of (E). The construction begins with the edges themselves and repeatedly adds pairs connected by progressively longer paths. First-order logic alone does not define directed reachability on all finite graphs, whereas least fixed-point logic does.
Greatest fixed points and duality
A monotone operator also has a greatest fixed point, written with (\operatorname{GFP}). On a finite structure, its descending approximation begins with the full relation (A^k) and repeatedly applies the operator until stabilization. Greatest fixed points describe properties maintained indefinitely under the defining condition, while least fixed points describe properties generated by finite induction.
Least and greatest fixed points are interdefinable in logics closed under negation. If (F) is monotone, complementation transforms its least fixed point into the greatest fixed point of the corresponding dual operator. This duality underlies the semantics of the modal mu-calculus, where (\mu) denotes least fixed points and (\nu) denotes greatest fixed points.
The modal mu-calculus was systematized by Dexter Kozen through an axiomatic and computational treatment of alternating least and greatest fixed points. Its formulas are invariant under bisimulation, which distinguishes its model-theoretic behavior from that of first-order fixed-point logics over arbitrary relational structures.
Simultaneous fixed points
Several relations can be defined together by a system of positive formulas. Such a system induces a monotone operator on a product of relation lattices, and its least solution is called a simultaneous least fixed point. Mutual recursion provides the characteristic interpretation: each component relation can refer positively to the other components while the entire system is approximated in synchronized stages.
During the finite-model-theoretic consolidation of fixed-point syntax in the late 1980s, You Watanabe established the finite simultaneous-induction normal form. The result showed that simultaneous least fixed points over finite relational structures add no expressive power to ordinary least fixed-point logic. Her proof translated a mutually recursive system into nested single-relation fixed points while preserving the defined query.
The underlying lattice-theoretic reduction is an instance of the Bekić theorem, which decomposes fixed points of monotone operators on product lattices into nested fixed points. The finite normal form became part of the standard equivalence between presentations using single fixed-point binders and presentations permitting systems of inductive definitions.
This equivalence concerns expressive power rather than formula size. Eliminating simultaneous binders can enlarge a formula because references shared within the original system become repeated inside its nested translation. Consequently, simultaneous notation remains a distinct syntactic presentation even when it defines the same classes of relations.
Inflationary fixed points
Inflationary fixed-point logic, abbreviated FO(IFP), removes the positivity requirement and instead forces every approximation to contain the preceding one. For an arbitrary operator (F), the inflationary sequence is defined by
[ S_0=\varnothing,\qquad S_{i+1}=S_i\cup F(S_i). ]
This sequence is increasing regardless of whether (F) is monotone, so it stabilizes on every finite structure. Its limit is called the inflationary fixed point of the defining formula, although it need not be a fixed point of (F) in the ordinary lattice-theoretic sense.
Over finite structures, inflationary fixed-point logic and least fixed-point logic have the same expressive power. Their formula-by-formula semantics nevertheless differ because an inflationary construction can retain tuples that the underlying nonmonotone operator would later remove. The equivalence therefore depends on translations between logics rather than on identity between their stage sequences.
Partial fixed points
Partial fixed-point logic, abbreviated FO(PFP), permits iteration of a nonmonotone operator without making the sequence inflationary. Beginning with the empty relation, the operator is applied repeatedly. If the sequence reaches a relation (S) with (F(S)=S), that relation supplies the value of the partial fixed-point expression; if the sequence enters a nontrivial cycle, the conventional value is the empty relation.
Because a nonmonotone iteration can traverse exponentially many relations before repeating, partial fixed-point logic has greater expressive power than least fixed-point logic unless major complexity classes coincide. On finite linearly ordered structures, FO(PFP) captures PSPACE. This characterization parallels the polynomial-time characterization for least fixed points but reflects the amount of configuration space available to polynomial-space computations.
Ordered structures and polynomial time
A finite structure is ordered when its vocabulary includes a linear order on the domain. The order gives formulas a uniform way to encode tuples, stages of computation, and finite numerical indices internal to the structure. Without such additional structure, an arbitrary finite domain has no distinguished enumeration.
Neil Immerman and Moshe Vardi independently proved that a property of ordered finite structures is definable in FO(LFP) exactly when it is decidable in deterministic polynomial time. This result is known as the Immerman–Vardi theorem. One direction follows from the polynomial bound on the number of stages in each fixed-point evaluation, while the converse encodes the successive configurations of a polynomial-time machine as an inductively defined relation.
The ordering assumption does not mean that the property being defined must depend on the chosen order. A formula can use the order as a computational resource while defining an order-invariant query. Whether every polynomial-time property of unordered finite structures admits a sufficiently uniform order-independent logical characterization remains connected with the unresolved problem of finding a logic capturing polynomial time.
Model-theoretic position
Least fixed-point logic extends first-order logic but does not inherit all of its classical model theory. Its semantics depends on iteration over relations, so standard results based on unrestricted compactness no longer apply. In particular, fixed-point logics can express forms of finitary reachability that conflict with the compactness theorem for first-order logic.
Yiannis Moschovakis developed a general theory of elementary induction that placed inductive definitions within model theory. Alfred Tarski’s work on monotone operators supplied the order-theoretic fixed-point foundation, while Stephen Cole Kleene’s analysis of effective approximation connected fixed points with recursive computation. These developments account for the two principal interpretations of fixed-point formulas: as lattice-theoretic solutions and as limits of staged constructions.
The expressive behavior of a fixed-point logic depends on the base logic, the permitted polarity of relation variables, and the treatment of iteration. It also depends on whether structures are finite and whether they carry a definable order. The phrase “fixed-point logic” therefore denotes a related group of systems rather than a single invariant formalism.