Understanding least-fixed point logic

Question

To better understand a paper I'm trying to get a brief understanding of least-fixed point logic. There are a few points where I am stuck.

If $G = (V,E)$ is a graph and

$$ \Phi(P) = \{(a,b) \mid G \models E(a,b) \lor P(a,b) \lor \exists z (E(a,z) \land P(z,b)) \}$$

is an operator on the binary relation $P$. I do not understand why the least fixed point $P^*$ of $P$ is the transitive closure of $E$. The example is taken from Finite Model Theory and Its Applications (p. 60).

When extending the first-order logic with the least-fixed pointer operator I do not understand why the relation symbol $S_i$ needs to be positive in the formula. Positive means that every occurence of $S_i$ in the formula is within an even number of negation symbols.

Does anyone have idea what is good to read for an intuitive understand of least-fixed pointer logic and its syntax and semantics?

Answer 1

If you are having trouble with the concept of least fixed point, I would recommend spending some time getting a background in more general order theory.

Davey and Priestley, Introduction to Lattices and Order is a good intro.

To see why the transitive closure is the least fixed point, imagine building up the closure from an empty set, applying the logical formula one step at a time. The least fixed point arrives when you can't add any new edges using the formula.

The requirement that the formula be positive ensures that the process is monotonic, i.e. that it grows at each step. If you had a negative subformula, you could have the case where on some steps the set of edges would decrease, and this could lead to a non-terminating oscillation up and down, rather than a convergence to the LFP.

Answer 2

Consider the boolean algebra formed from the powerset of a finite set $S$, ordered by set inclusion. Now, consider the operator $P$ defined by

$$ P(X) = \lnot X $$

Clearly $P$ is a non-positive operator.

1. Show that there are no fixed points $\mu P$ such that $P(\mu P) = \mu P$. As a result, you can conclude that $\mu X.\;P(X)$ cannot be well-defined.

2. Prove the Knaster-Tarksi theorem for yourself. That is, if you have a complete lattice $L$, and a monotone function $f : L \to L$, then the set of fixed points of $f$ forms a complete lattice. (As a consequence, $f$ has a least and greatest fixed point.) This proof is very short, but it's a bit of a head-scratcher the first time you see it, and the monotonicity of $f$ is critical to the argument.

3. Prove for yourself that any operator defined by an expression with a free variable $X$ which occurs only positively is monotone. So positive occurence is a syntactic condition which is sufficient to enforce monotonicity.

I find that there's no substitute for doing these proofs for yourself for really internalizing the intuition.

Answer 3

this is a very old post so you might have already encountered the answer as desired. Since I have been studying FO(LFP) for the past few months. I have some understanding of the answers you require.

To answer the requirement of positivity, the need comes from the fact that testing whether the formula captures a monotone operator or not is undecidable both in finite and infinite models. What do I mean by a formula capturing a monotone operator? Suppose you write out a FO$[\sigma$] formula with a free second order variable say $\phi(\vec{x},X)$, where $|\vec{x}|=ar(X)$, then we can define a corresponding operator $f_\phi$ : $\mathcal{P}(A^{ar(X)}) \mapsto \mathcal{P}(A^{ar(x)})$ where ar(X) is the arity of the second order variable and A is the domain of the $\sigma$-structure $\mathbb{A}$ and $\mathcal{P}(Z)$ is the power set of the set Z. And $f_\phi(Z) = \{\ \vec{a} \in A^{ar(X)}\ |\ \mathbb{A},\vec{a},Z \models \phi\ \} $. If this operator is monotone then we can easily capture the fixed point in both finite and infinite structure following the knaster tarski's fixed point theorem mentioned in the above answers. But, the problem is testing whether the formula written out of the form as above encodes a monotone operator or not is undecidable so we need to get the next best thing. Positivity in the second order free variable ensures the monotonicity requirement is met, its a standard structural induction to prove this phenomenon. Question is, is it enough?

To that, I have no solid answer yet, since I'm still reading. I can point to papers on this front. At least the one explaining ideas I mentioned here, are from the paper, Monotone vs Positive - Ajtai, Gurevich. It also further mentions another paper Fixed point extensions of first order logic by Gurevich and Shelah that states the fixed point operator when applied to the positive formula doesn't lose expressive power when compared with the application being done over arbitrary monotone formulas.