# Define infinite path with a finite relation in a graph with Least Fixed Point logic

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?

-

1
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$. – Arthur Fischer Jan 19 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 at 17:12

1
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. – Arthur Fischer Jan 20 at 6:15
{"extraction_info": {"found_math": true, "script_math_tex": 0, "script_math_asciimath": 0, "math_annotations": 0, "math_alttext": 0, "mathml": 0, "mathjax_tag": 0, "mathjax_inline_tex": 23, "mathjax_display_tex": 3, "mathjax_asciimath": 0, "img_math": 0, "codecogs_latex": 0, "wp_latex": 0, "mimetex.cgi": 0, "/images/math/codecogs": 0, "mathtex.cgi": 0}, "config": {"markdown_headings": true, "markdown_code": true, "boilerplate_config": {"ratio_threshold": 0.18, "absolute_threshold": 10, "end_threshold": 15, "enable": false}, "remove_buttons": true, "remove_image_figures": true, "remove_link_clusters": true, "table_config": {"min_rows": 2, "min_cols": 3, "format": "github"}, "remove_chinese": true, "remove_edit_buttons": true, "extract_latex": true}, "english_confidence": 0.949445903301239, "perplexity_flag": "head"}