Class Description

FO(PFP): First-order with partial fixed point

FO(pfp) is the set of boolean queries definable with first-order formulae with a partial fixed point operator.

Let ${\displaystyle k}$ be an integer, ${\displaystyle x,y}$ vectors of ${\displaystyle k}$ variables, ${\displaystyle P}$ a second-order variable of arity ${\displaystyle k}$, and ${\displaystyle \phi }$ a FO(PFP) function using ${\displaystyle x}$ and ${\displaystyle P}$ as variables, then we can define iteratively ${\displaystyle (P_{i})_{i\in N}}$ such that ${\displaystyle P_{0}(x)=false}$ and ${\displaystyle P_{i}(x)=\phi (P_{i-1},x)}$ which means that the property ${\displaystyle P_{i}}$ is true on the input ${\displaystyle x}$ if ${\displaystyle \phi }$ is true on input ${\displaystyle x}$, and when the variable ${\displaystyle P}$ is replaced by ${\displaystyle P_{i-1}}$. Then, either there is a fixed point, or the list of ${\displaystyle (P_{i})}$ is looping.

PFP(${\displaystyle \phi _{P,x})(y)}$ is defined as the value of the fixed point of ${\displaystyle (P_{i})}$ on y if there is a fixed point, else as false.

Since ${\displaystyle P}$s are property of arity ${\displaystyle k}$, there is at most ${\displaystyle 2^{n^{k}}}$ values for the ${\displaystyle P_{i}}$s, so with a poly-space counter we can check if there is a loop or not.

It was proved in [Imm98] that FO(pfp) is equal to PSPACE.

Linked From

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)}}$).

More about...

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