FO (complexity) - Iterating

Iterating

We will define first-order with iteration, 'FO'; here is a (class of) functions from integers to integers, and for different classes of functions we will obtain different complexity classes FO.

In this section we will write to mean and to mean . We first need to define quantifier blocks (QB), a quantifier block is a list where the s are quantifier-free FO-formulae and s are either or . If is a quantifiers block then we will call the iteration operator, which is defined as written time. One should pay attention that here there are quantifiers in the list, but only variables and each of those variable are used times.

We can now define FO to be the FO-formulae with an iteration operator whose exponent is in the class, and we obtain those equalities:

• 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 PTIME, it is also another way to write |FO(LFP).
• FO is equal to PSPACE, it is also another way to write FO(PFP).