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̄)

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
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.