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 :

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