Descriptive complexity theory

Overview of characterisations of complexity classes

If we restrict ourselves to ordered structures with a successor relation and basic arithmetical predicates, then we get the following characterisations:

• First-order logic defines the class of logspace-uniform AC⁰, the languages recognized by polynomial-size circuits of bounded depth, which equals the languages recognized by a concurrent random access machine in constant time.
• First-order logic augmented with majority operators yield logspace-uniform TC⁰.
• First-order logic augmented with symmetric or deterministic transitive closure operators yield L, problems solvable in logarithmic space.
• First-order logic with a transitive closure operator yields NL, the problems solvable in nondeterministic logarithmic space.
• First-order logic with a least fixed point operator gives P, the problems solvable in deterministic polynomial time, but uniquely on ordered structures.
• Fagin's theorem: Existential second-order logic yields NP.
• Universal second-order logic (excluding existential second-order quantification) yields co-NP.
• Second-order logic corresponds to the polynomial hierarchy PH.
• Second-order logic with a transitive closure operator (commutative or not) yields PSPACE, the problems solvable in polynomial space.
• Second-order logic with a least fixed point operator gives EXPTIME, the problems solvable in exponential time.
• HO, the complexity class defined by higher-order logic, is equal to ELEMENTARY

Sub-polynomial time

FO without any operators

In circuit complexity, first-order logic with arbitrary predicates can be shown to be equal to AC⁰, the first class in the AC hierarchy. Indeed, there is a natural translation from FO's symbols to nodes of circuits, with ${\displaystyle \mathrm{\forall },\mathrm{\exists }}$ being ${\displaystyle \wedge }$ and ${\displaystyle \vee }$ of size n. First-order logic in a signature with arithmetical predicates characterises the restriction of the AC⁰ family of circuits to those constructible in alternating logarithmic time. First-order logic in a signature with only the order relation corresponds to the set of star-free languages.

Transitive closure logic

First-order logic gains substantially in expressive power when it is augmented with an operator that computes the transitive closure of a binary relation. The resulting transitive closure logic is known to characterise non-deterministic logarithmic space (NL) on ordered structures. This was used by Immerman to show that NL is closed under complement (i. e. that NL = co-NL).

When restricting the transitive closure operator to deterministic transitive closure, the resulting logic exactly characterises logarithmic space on ordered structures.

Second-order Krom formulae

On structures that have a successor function, NL can also be characterised by second-order Krom formulae.

SO-Krom is the set of Boolean queries definable with second-order formulae in conjunctive normal form such that the first-order quantifiers are universal and the quantifier-free part of the formula is in Krom form, which means that the first-order formula is a conjunction of disjunctions, and in each "disjunction" there are at most two variables. Every second-order Krom formula is equivalent to an existential second-order Krom formula.

SO-Krom characterises NL on structures with a successor function.

Polynomial time

On ordered structures, first-order least fixed-point logic captures PTIME:

First-order least fixed-point logic

FO[LFP] is the extension of first-order logic by a least fixed-point operator, which expresses the fixed-point of a monotone expression. This augments first-order logic with the ability to express recursion. The Immerman–Vardi theorem, shown independently by Immerman and Vardi, shows that FO[LFP] characterises PTIME on ordered structures.

As of 2025, it is still open whether there is a natural logic characterising PTIME on unordered structures.

The Abiteboul–Vianu theorem states that FO[LFP]=FO[PFP] on all structures if and only if FO[LFP]=FO[PFP]; hence if and only if P=PSPACE. This result has been extended to other fixpoints.

Second-order Horn formulae

In the presence of a successor function, PTIME can also be characterised by second-order Horn formulae.

SO-Horn is the set of Boolean queries definable with SO formulae in disjunctive normal form such that the first-order quantifiers are all universal and the quantifier-free part of the formula is in Horn form, which means that it is a big AND of OR, and in each "OR" every variable except possibly one are negated.

This class is equal to P on structures with a successor function.

Those formulae can be transformed to prenex formulas in existential second-order Horn logic.

Non-deterministic polynomial time

Fagin's theorem

Ronald Fagin's 1974 proof that the complexity class NP was characterised exactly by those classes of structures axiomatizable in existential second-order logic was the starting point of descriptive complexity theory.

Since the complement of an existential formula is a universal formula, it follows immediately that co-NP is characterized by universal second-order logic.

SO, unrestricted second-order logic, is equal to the Polynomial hierarchy PH. More precisely, we have the following generalisation of Fagin's theorem: The set of formulae in prenex normal form where existential and universal quantifiers of second order alternate k times characterise the kth level of the polynomial hierarchy.

Unlike most other characterisations of complexity classes, Fagin's theorem and its generalisation do not presuppose a total ordering on the structures. This is because existential second-order logic is itself sufficiently expressive to refer to the possible total orders on a structure using second-order variables.

Beyond NP

Partial fixed point is PSPACE

The class of all problems computable in polynomial space, PSPACE, can be characterised by augmenting first-order logic with a more expressive partial fixed-point operator.

Partial fixed-point logic, FO[PFP], is the extension of first-order logic with a partial fixed-point operator, which expresses the fixed-point of a formula if there is one and returns 'false' otherwise.

Partial fixed-point logic characterises PSPACE on ordered structures.

Transitive closure is PSPACE

Second-order logic can be extended by a transitive closure operator in the same way as first-order logic, resulting in SO[TC]. The TC operator can now also take second-order variables as argument. SO[TC] characterises PSPACE. Since ordering can be referenced in second-order logic, this characterisation does not presuppose ordered structures.

Elementary functions

The time complexity class ELEMENTARY of elementary functions can be characterised by HO, the complexity class of structures that can be recognized by formulas of higher-order logic. Higher-order logic is an extension of first-order logic and second-order logic with higher-order quantifiers. There is a relation between the ${\displaystyle i}$th order and non-deterministic algorithms the time of which is bounded by ${\displaystyle i-1}$ levels of exponentials.

Definition

We define higher-order variables. A variable of order ${\displaystyle i>1}$ has an arity ${\displaystyle k}$ and represents any set of ${\displaystyle k}$-tuples of elements of order ${\displaystyle i-1}$. They are usually written in upper-case and with a natural number as exponent to indicate the order. Higher-order logic is the set of first-order formulae where we add quantification over higher-order variables; hence we will use the terms defined in the FO article without defining them again.

HO${\displaystyle {}^i}$ is the set of formulae with variables of order at most ${\displaystyle i}$. HO${\displaystyle {}_j^i}$ is the subset of formulae of the form ${\displaystyle \varphi =\mathrm{\exists }\overline{X_1^i}\mathrm{\forall }\overline{X_2^i}\dots Q\overline{X_j^i}\psi }$, where ${\displaystyle Q}$ is a quantifier and ${\displaystyle Q\overline{X^i}}$ means that ${\displaystyle \overline{X^i}}$ is a tuple of variable of order ${\displaystyle i}$ with the same quantification. So HO${\displaystyle {}_j^i}$ is the set of formulae with ${\displaystyle j}$ alternations of quantifiers of order ${\displaystyle i}$, beginning with ${\displaystyle \mathrm{\exists }}$, followed by a formula of order ${\displaystyle i-1}$.

Using the standard notation of the tetration, ${\displaystyle {\exp }_2^0(x)=x}$ and ${\displaystyle {\exp }_2^{i+1}(x)=2^{{\exp }_2^i(x)}}$. ${\displaystyle {\exp }_2^{i+1}(x)=2^{2^{2^{2^{\dots {}^{2^x}}}}}}$ with ${\displaystyle i}$ times ${\displaystyle 2}$

Normal form

Every formula of order ${\displaystyle i}$th is equivalent to a formula in prenex normal form, where we first write quantification over variable of ${\displaystyle i}$th order and then a formula of order ${\displaystyle i-1}$ in normal form.

Relation to complexity classes

HO is equal to the class ELEMENTARY of elementary functions. To be more precise, ${\displaystyle {\mathsf{H}\mathsf{O}}_0^i=\mathsf{N}\mathsf{T}\mathsf{I}\mathsf{M}\mathsf{E}({\exp }_2^{i-2}(n^{O(1)}))}$, meaning a tower of ${\displaystyle (i-2)}$ 2s, ending with ${\displaystyle n^c}$, where ${\displaystyle c}$ is a constant. A special case of this is that ${\displaystyle \mathrm{\exists }\mathsf{S}\mathsf{O}={\mathsf{H}\mathsf{O}}_0^2=\mathsf{N}\mathsf{T}\mathsf{I}\mathsf{M}\mathsf{E}(n^{O(1)})=\mathsf{N}\mathsf{P}}$, which is exactly Fagin's theorem. Using oracle machines in the polynomial hierarchy, ${\displaystyle {\mathsf{H}\mathsf{O}}_j^i=\mathsf{N}\mathsf{T}\mathsf{I}\mathsf{M}\mathsf{E}({\exp }_2^{i-2}(n^{O(1)}{)}^{{\mathrm{\Sigma }}_j^{\mathsf{P}}})}$