Inmathematical logic,fixed-point logics are extensions of classical predicate logic that have been introduced to express recursion. Their development has been motivated bydescriptive complexity theory and their relationship todatabase query languages, in particular toDatalog.

Least fixed-point logic was first studied systematically byYiannis N. Moschovakis in 1974,^[1] and it was introduced to computer scientists in 1979, whenAlfred Aho andJeffrey Ullman suggested fixed-point logic as an expressive database query language.^[2]

For arelational signatureX, FO[PFP](X) is the set of formulas formed fromX usingfirst-order connectives and predicates,second-order variables as well as a partial fixed point operator${\displaystyle \mathrm{PFP}}$ used to form formulas of the form${\displaystyle [{\mathrm{PFP}}_{\overrightarrow{x},P}\phi ]\overrightarrow{t}}$, where${\displaystyle P}$ is a second-order variable,${\displaystyle \overrightarrow{x}}$ a tuple of first-order variables,${\displaystyle \overrightarrow{t}}$ a tuple of terms and the lengths of${\displaystyle \overrightarrow{x}}$ and${\displaystyle \overrightarrow{t}}$ coincide with the arity of${\displaystyle P}$.

Letk be an integer,${\displaystyle x,y}$ be vectors ofk variables,P be a second-order variable of arityk, and letφ be an FO(PFP,X) function usingx andP as variables. We can iteratively define${\displaystyle (P_i{)}_{i\in N}}$ such that${\displaystyle P_0(x)=false}$ and${\displaystyle P_i(x)=\phi (P_{i-1},x)}$ (meaningφ with${\displaystyle P_{i-1}}$ substituted for the second-order variableP). Then, either there is a fixed point, or the list of${\displaystyle (P_i)}$s is cyclic.^[3]

${\displaystyle [{\mathrm{PFP}}_{P,x}\phi (y)]}$ is defined as the value of the fixed point of${\displaystyle (P_i)}$ ony if there is a fixed point, else as false.^[4] SincePs are properties of arityk, 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 inPSPACE.^[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 ofP (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 isP, then${\displaystyle P_i(x)}$ always implies${\displaystyle P_{i+1}(x)}$).

Due to monotonicity, we only add vectors to the truth table ofP, 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 byImmerman^[7] andVardi,^[8] shows that FO(LFP,X) characterisesP on all ordered structures.

The expressivity of least-fixed point logic coincides exactly with the expressivity of the database querying languageDatalog, showing that, on ordered structures, 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 \mathrm{IFP}({\varphi }_{P,x})}$ as${\displaystyle \mathrm{PFP}({\psi }_{P,x})}$ where${\displaystyle \psi (P,x)=\varphi (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 thearity 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 onlytransitive closures to be expressed directly.

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

TC is defined as follows: Letk be a positive integer and${\displaystyle u,v,x,y}$ be vectors ofk variables. Then${\displaystyle \mathsf{T}\mathsf{C}({\varphi }_{u,v})(x,y)}$ is true if there existn vectors of variables${\displaystyle (z_i)}$ such that${\displaystyle z_1=x,z_n=y}$, and for all,${\displaystyle \varphi (z_i,z_{i+1})}$ is true. Here,φ is a formula written in FO(TC) and${\displaystyle \varphi (x,y)}$ means that the variablesu andv are replaced byx andy.

Over ordered structures, FO[TC] characterises the complexity classNL.^[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 \mathrm{DTC}({\varphi }_{u,v})}$, we know that for allu, there exists at most onev such that${\displaystyle \varphi (u,v)}$.

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

Over ordered structures, FO[DTC] characterises the complexity classL.^[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{F}\mathsf{O}[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{F}\mathsf{O}[t(n)]}$.

In this section we will write${\displaystyle (\mathrm{\forall }xP)Q}$ to mean${\displaystyle (\mathrm{\forall }x(P\Rightarrow Q))}$ and${\displaystyle (\mathrm{\exists }xP)Q}$ to mean${\displaystyle (\mathrm{\exists }x(P\wedge Q))}$. We first need to define quantifier blocks (QB), a quantifier block is a list${\displaystyle (Q_1{x}_1,{\varphi }_1)...(Q_k{x}_k,{\varphi }_k)}$ where the${\displaystyle {\varphi }_i}$s are quantifier-free FO-formulae and${\displaystyle Q_i}$s are either${\displaystyle \mathrm{\forall }}$ or${\displaystyle \mathrm{\exists }}$. IfQ is a quantifiers block then we will call${\displaystyle [Q{]}^{t(n)}}$ the iteration operator, which is defined asQ written${\displaystyle t(n)}$ time. One should pay attention that here there are${\displaystyle k\ast t(n)}$ quantifiers in the list, but onlyk variables and each of those variable are used${\displaystyle t(n)}$ times.^[14]

We can now define${\displaystyle \mathsf{F}\mathsf{O}[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{F}\mathsf{O}[(\log n{)}^i]}$ is equal to FO-uniformACⁱ, and in fact${\displaystyle \mathsf{F}\mathsf{O}[t(n)]}$ is FO-uniform AC of depth${\displaystyle t(n)}$.^[15]
• ${\displaystyle \mathsf{F}\mathsf{O}[(\log n{)}^{O(1)}]}$ is equal to NC.^[16]
• ${\displaystyle \mathsf{F}\mathsf{O}[n^{O(1)}]}$ is equal toPTIME. It is also another way to write FO(IFP).^[17]
• ${\displaystyle \mathsf{F}\mathsf{O}[2^{n^{O(1)}}]}$ is equal toPSPACE. 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.

• Descriptive complexity
• Database theory
• Predicate logic

• Articles with short description
• Short description is different from Wikidata