Fixed-point logic

For a relational signature X, FO[PFP](X) is the set of formulas formed from X using first-order connectives and predicates, second-order variables as well as a partial fixed point operator ${\displaystyle \operatorname {PFP} }$ used to form formulas of the form ${\displaystyle [\operatorname {PFP} _{{\vec {x}},P}\varphi ]{\vec {t}}}$, where ${\displaystyle P}$ is a second-order variable, ${\displaystyle {\vec {x}}}$ a tuple of first-order variables, ${\displaystyle {\vec {t}}}$ a tuple of terms and the lengths of ${\displaystyle {\vec {x}}}$ and ${\displaystyle {\vec {t}}}$ coincide with the arity of ${\displaystyle P}$.

Let k be an integer, ${\displaystyle x,y}$ be vectors of k variables, P be a second-order variable of arity k, and let φ be an FO(PFP,X) function using x and P as variables. We can iteratively define ${\displaystyle (P_{i})_{i\in N}}$ such that ${\displaystyle P_{0}(x)=false}$ and ${\displaystyle P_{i}(x)=\varphi (P_{i-1},x)}$ (meaning φ with ${\displaystyle P_{i-1}}$ substituted for the second-order variable P). Then, either there is a fixed point, or the list of ${\displaystyle (P_{i})}$s is cyclic.[3]

${\displaystyle [\operatorname {PFP} _{P,x}\varphi (y)]}$ is defined as the value of the fixed point of ${\displaystyle (P_{i})}$ on y if there is a fixed point, else as false.[4] Since Ps are properties of arity k, there are at most ${\displaystyle 2^{n^{k}}}$ values for the ${\displaystyle P_{i}}$s, so with a polynomial-space counter we can check if there is a loop or not.[5]

It has been proven that on ordered finite structures, a property is expressible in FO(PFP,X) if and only if it lies in PSPACE.[6]

Since the iterated predicates involved in calculating the partial fixed point are not in general monotone, the fixed-point may not always exist. FO(LFP,X), least fixed-point logic, is the set of formulas in FO(PFP,X) where the partial fixed point is taken only over such formulas φ that only contain positive occurrences of P (that is, occurrences preceded by an even number of negations). This guarantees monotonicity of the fixed-point construction (That is, if the second order variable is P, then ${\displaystyle P_{i}(x)}$ always implies ${\displaystyle P_{i+1}(x)}$).

Due to monotonicity, we only add vectors to the truth table of P, and since there are only ${\displaystyle n^{k}}$ possible vectors we will always find a fixed point before ${\displaystyle n^{k}}$ iterations. The Immerman-Vardi theorem, shown independently by Immerman[7] and Vardi,[8] shows that FO(LFP,X) characterises P on all ordered structures.

The expressivity of least-fixed point logic coincides exactly with the expressivity of the database querying language Datalog, showing that Datalog can express exactly those queries executable in polynomial time.[9]

Another way to ensure the monotonicity of the fixed-point construction is by only adding new tuples to ${\displaystyle P}$ at every stage of iteration, without removing tuples for which ${\displaystyle P}$ no longer holds. Formally, we define ${\displaystyle \operatorname {IFP} (\phi _{P,x})}$ as ${\displaystyle \operatorname {PFP} (\psi _{P,x})}$ where ${\displaystyle \psi (P,x)=\phi (P,x)\vee P(x)}$.

This inflationary fixed-point agrees with the least-fixed point where the latter is defined. Although at first glance it seems as if inflationary fixed-point logic should be more expressive than least fixed-point logic since it supports a wider range of fixed-point arguments, in fact, every FO[IFP](X)-formula is equivalent to an FO[LFP](X)-formula.[10]

While all the fixed-point operators introduced so far iterated only on the definition of a single predicate, many computer programs are more naturally thought of as iterating over several predicates simultaneously. By either increasing the arity of the fixed-point operators or by nesting them, every simultaneous least, inflationary or partial fixed-point can in fact be expressed using the corresponding single-iteration constructions discussed above.[11]

Rather than allow induction over arbitrary predicates, transitive closure logic allows only transitive closures to be expressed directly.

FO[TC](X) is the set of formulas formed from X using first-order connectives and predicates, second-order variables as well as a transitive closure operator ${\displaystyle \operatorname {TC} }$ used to form formulas of the form ${\displaystyle [\operatorname {TC} _{{\vec {x}},{\vec {y}}}\varphi ]{\vec {s}}{\vec {t}}}$, where ${\displaystyle {\vec {x}}}$ and ${\displaystyle {\vec {y}}}$ are tuples of pairwise distinct first-order variables, ${\displaystyle {\vec {t}}}$ and ${\displaystyle {\vec {s}}}$ tuples of terms and the lengths of ${\displaystyle {\vec {x}}}$, ${\displaystyle {\vec {y}}}$, ${\displaystyle {\vec {s}}}$ and ${\displaystyle {\vec {t}}}$ coincide.

TC is defined as follows: Let k be a positive integer and ${\displaystyle u,v,x,y}$ be vectors of k variables. Then ${\displaystyle {\mathsf {TC}}(\phi _{u,v})(x,y)}$ is true if there exist n vectors of variables ${\displaystyle (z_{i})}$ such that ${\displaystyle z_{1}=x,z_{n}=y}$, and for all ${\displaystyle i<n}$, ${\displaystyle \phi (z_{i},z_{i+1})}$ is true. Here, φ is a formula written in FO(TC) and ${\displaystyle \phi (x,y)}$ means that the variables u and v are replaced by x and y.

Over ordered structures, FO[TC] characterises the complexity class NL.[12] This characterisation is a crucial part of Immerman's proof that NL is closed under complement (NL = co-NL).[13]

FO[DTC](X) is defined as FO(TC,X) where the transitive closure operator is deterministic. This means that when we apply ${\displaystyle \operatorname {DTC} (\phi _{u,v})}$, we know that for all u, there exists at most one v such that ${\displaystyle \phi (u,v)}$.

We can suppose that ${\displaystyle \operatorname {DTC} (\phi _{u,v})}$ is syntactic sugar for ${\displaystyle \operatorname {TC} (\psi _{u,v})}$ where ${\displaystyle \psi (u,v)=\phi (u,v)\wedge \forall x(x=v\vee \neg \phi (u,x))}$.

Over ordered structures, FO[DTC] characterises the complexity class L.[12]

The fixed-point operations that we defined so far iterate the inductive definitions of the predicates mentioned in the formula indefinitely, until a fixed point is reached. In implementations, it may be necessary to bound the number of iterations to limit the computation time. The resulting operators are also of interest from a theoretical point of view since they can also be used to characterise complexity classes.

We will define first-order with iteration, ${\displaystyle {\mathsf {FO}}[t(n)]}$; here ${\displaystyle t(n)}$ is a (class of) functions from integers to integers, and for different classes of functions ${\displaystyle t(n)}$ we will obtain different complexity classes ${\displaystyle {\mathsf {FO}}[t(n)]}$.

In this section we will write ${\displaystyle (\forall xP)Q}$ to mean ${\displaystyle (\forall x(P\Rightarrow Q))}$ and ${\displaystyle (\exists xP)Q}$ to mean ${\displaystyle (\exists x(P\wedge Q))}$. We first need to define quantifier blocks (QB), a quantifier block is a list ${\displaystyle (Q_{1}x_{1},\phi _{1})...(Q_{k}x_{k},\phi _{k})}$ where the ${\displaystyle \phi _{i}}$s are quantifier-free FO-formulae and ${\displaystyle Q_{i}}$s are either ${\displaystyle \forall }$ or ${\displaystyle \exists }$. If Q is a quantifiers block then we will call ${\displaystyle [Q]^{t(n)}}$ the iteration operator, which is defined as Q written ${\displaystyle t(n)}$ time. One should pay attention that here there are ${\displaystyle k*t(n)}$ quantifiers in the list, but only k variables and each of those variable are used ${\displaystyle t(n)}$ times.[14]

We can now define ${\displaystyle {\mathsf {FO}}[t(n)]}$ to be the FO-formulae with an iteration operator whose exponent is in the class ${\displaystyle t(n)}$, and we obtain the following equalities:

• ${\displaystyle {\mathsf {FO}}[(\log n)^{i}]}$ is equal to FO-uniform ACⁱ, and in fact ${\displaystyle {\mathsf {FO}}[t(n)]}$ is FO-uniform AC of depth ${\displaystyle t(n)}$.[15]
• ${\displaystyle {\mathsf {FO}}[(\log n)^{O(1)}]}$ is equal to NC.[16]
• ${\displaystyle {\mathsf {FO}}[n^{O(1)}]}$ is equal to PTIME. It is also another way to write FO(IFP).[17]
• ${\displaystyle {\mathsf {FO}}[2^{n^{O(1)}}]}$ is equal to PSPACE. It is also another way to write FO(PFP). [18]

• Ebbinghaus, Heinz-Dieter; Flum, Jörg (1999). Finite Model Theory. Perspectives in Mathematical Logic (2 ed.). Springer. doi:10.1007/978-3-662-03182-7. ISBN 978-3-662-03184-1.
• Neil, Immerman (1999). Descriptive complexity. Springer. ISBN 0-387-98600-6. OCLC 901297152.