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
be an integer,
vectors of
variables,
a second-order variable of arity
, and
a FO(PFP) function using
and
as variables, then we can define iteratively
such that
and
which means that the property
is true on the input
if
is true on input
, and when the variable
is replaced by
. Then, either there is a fixed point, or the list of
is looping.
PFP(
is defined as the value of the fixed point of
on y if there is a fixed point, else as false.
Since
s are property of arity
, there is at most
values for the
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
, then
always implies
.
We can obtain the monotony by restricting the formula
to have only positive occurrences of
(i.e. there is an even number of negations before every occurrence of
). We can also describe LFP(
) as syntactic sugar of PFP(
) where
.
Thanks to monotonicity we only add and never remove vectors to the truth table of
, and since there is only
possible vectors we always find a fixed point before
iterations. Hence it was shown in [Imm82] that FO(LFP)=P. This definition is equivalent to FO(
).
More about...
FO[
]: Iterated First-Order logic
Let
be a function from integers to integers.
abbreviates
and
abbreviates
.
A quantifier block is a list
where the
s are quantifier free FO-formulae and each
s is either
or
.If
is a quantifier block then
is the block consisting of
iterated copies of
. Note that there are
quantifiers in the list, but only k variables; each variable is used
times.
FO[
] consists of the FO-formulae with quantifier blocks that are iterated
times.
In Descriptive complexity we can see that :
- FO[
] is equal to fo-uniform ACi, and in fact FO[
] is fo-uniform AC of depth 
- FO[
] is equal to NC - FO[
] is equal to P and FO(LFP) - FO[
] is equal to PSPACE and FO(PFP)
More about...