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 \forall ,\exists }$ being ${\displaystyle \land }$ and ${\displaystyle \lor }$ 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.^[1] First-order logic in a signature with only the order relation corresponds to the set of star-free languages.^[8][9]

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).^[10]

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.^[11]

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.^[12][13]

As of 2022, 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.^[14]

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.^[15]

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

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.^[4][16]

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

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.^[17]

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.^[18]

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.^[19]

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.^[20]

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 \phi =\exists {\overline {X_{1}^{i}}}\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 \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 {HO}}_{0}^{i}={\mathsf {NTIME}}(\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 \exists {\mathsf {SO}}={\mathsf {HO}}_{0}^{2}={\mathsf {NTIME}}(n^{O(1)})={\color {Blue}{\mathsf {NP}}}}$, which is exactly Fagin's theorem. Using oracle machines in the polynomial hierarchy, ${\displaystyle {\mathsf {HO}}_{j}^{i}={\color {Blue}{\mathsf {NTIME}}}(\exp _{2}^{i-2}(n^{O(1)})^{\Sigma _{j}^{\mathsf {P}}})}$