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 :

More about...