Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. Join them; it only takes a minute:

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

Least Fixed Point(LFP) logic (p. 37ff) is an extension of first order logic which enables the usage of the least fixed point of FO-definable operators. For example consider a graph $G=(V,E)$ and binary operator $T(x,y)$ defined by

$$ x = y \lor \lor T(x,y) \lor \exists z (Exz \land Tzy).$$

The operator "updates" a binary relation $R \subseteq V \times V$ to $T(R)$. Now if we consider multiple application of $T$ onto a relation $R$

$$T(T(\dots T(R) \dots))$$

the operator reaches a fixed point such that

$$T^n(R) = T^{n+1}(R).$$

Then $T^n$ is a fixed point. The fixed point which is minimal with respect to $\subseteq$ is the least fixed point. LFP allows FO-defined operators to define new relations. The least fixed point of $E$ and the operator above is the binary transtive closure relation $TC(E)$ of $E$.

Given a directed (possibly not finite) graph $G = (V,E,P)$ with an unary relation symbol $P$. We want to define a LFP-formula $\varphi(v) \models G$ iff there is an infinite path starting in $v$ such that $P$ occurs only finitely often.

If have several problems with this exercise. First of all I do not now how to define paths because it is possible to define relations on $V \times V$ but if an edge on infinite path would occur twice then a fixed point is imitatively reached even though the path is not finished. Second, I know that it is possible to define "finite" in a structure with a successor function $S$ with $LFP$ logic. But I don't think that such a function is definable. Is it a good approach to divide the properties or is it easier to use a more holistic approach? Any hints?

share|cite|improve this question
I have only passing acquaintance with LFPL, but my thought would be to try to model the following statement: there is a node $u$ reachable from $v$ and there is an infinite path starting at $u$ with no occurrences of $P$. – arjafi Jan 19 '13 at 16:14
Okay, the existence of a reachable node is similar to the transitive closure but how do I model an infinite path with a single formula without a set of formulas? – joachim Jan 19 '13 at 17:12
If I had a better feel for the logic I would say more, but unfortunately I don't. I'll try to think about this more, however. – arjafi Jan 20 '13 at 6:15

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Browse other questions tagged or ask your own question.