Class Description

FO(LFP): First-order with least fixed point

FO(LFP) is the set of boolean queries definable with first-order fixed-point formulae where the partial fixed point is limited to be monotone, which means that if the second order variable is ${\displaystyle P}$, then ${\displaystyle P_{i}(x)}$ always implies ${\displaystyle P_{i+1}(x)}$.

We can obtain the monotony by restricting the formula ${\displaystyle \phi }$ to have only positive occurrences of ${\displaystyle P}$ (i.e. there is an even number of negations before every occurrence of ${\displaystyle P}$). We can also describe LFP(${\displaystyle \phi _{P,x}}$) as syntactic sugar of PFP(${\displaystyle \psi _{P,x}}$) where ${\displaystyle \psi (P,x)=\phi (P,x)\vee P(x)}$.

Thanks to monotonicity we only add and never remove vectors to the truth table of ${\displaystyle P}$, and since there is only ${\displaystyle n^{k}}$ possible vectors we always find a fixed point before ${\displaystyle n^{k}}$ iterations. Hence it was shown in [Imm82] that FO(LFP)=P. This definition is equivalent to FO(${\displaystyle n^{O(1)}}$).

Linked From

FO[${\displaystyle t(n)}$]: Iterated First-Order logic

Let ${\displaystyle t(n)}$ be a function from integers to integers.${\displaystyle (\forall xP)Q}$ abbreviates ${\displaystyle (\forall x(P\Rightarrow Q))}$ and ${\displaystyle (\exists xP)Q}$ abbreviates ${\displaystyle (\exists x(P\wedge Q))}$.

A quantifier block is a list ${\displaystyle (Q_{1}x_{1}.\phi _{1})...(Q_{k}x_{k}.\phi _{k})}$ where the ${\displaystyle \phi _{i}}$s are quantifier free FO-formulae and each ${\displaystyle Q_{i}}$s is either ${\displaystyle \forall }$ or ${\displaystyle \exists }$.If ${\displaystyle Q}$ is a quantifier block then ${\displaystyle [Q]^{t(n)}}$ is the block consisting of ${\displaystyle t(n)}$ iterated copies of ${\displaystyle Q}$. Note that there are ${\displaystyle k*t(n)}$ quantifiers in the list, but only k variables; each variable is used ${\displaystyle t(n)}$ times.

FO[${\displaystyle t(n)}$] consists of the FO-formulae with quantifier blocks that are iterated ${\displaystyle \Theta (t(n))}$ times.

In Descriptive complexity we can see that :

• FO[${\displaystyle (\log n)^{i}}$] is equal to fo-uniform ACⁱ, and in fact FO[${\displaystyle t(n)}$] is fo-uniform AC of depth ${\displaystyle t(n)}$
• FO[${\displaystyle (\log n)^{O(1)}}$] is equal to NC
• FO[${\displaystyle n^{O(1)}}$] is equal to P and FO(LFP)
• FO[${\displaystyle 2^{n^{O(1)}}}$] is equal to PSPACE and FO(PFP)

More about...

SO[LFP]: Second-Order logic with least fixed point

SO[LFP] is to SO what FO[LFP] is to FO. The LFP operator can now also take second-order variable as argument.

In Descriptive complexity we can see that SO[LFP] is equal to EXPTIME.

More about...