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
, 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(
).
Linked From
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...
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...