Descriptive complexity relates the realms of logic and complexity theory.

Fagin’s theorem1 states the following:

A class $\mathcal{C}$ of finite structures is definable by a sentence of existential second-order logic if and only if it is decidable by a non-deterministic machine running in polynomial time.

i.e. $\mathsf{ESO} = \mathsf{NP}$

In other words, a problem lies in NP iff it can be described by a formula with a pattern in $E_i^* (ae)^*$ (monadic existential second-order formula) for some arity $i$2.

The Büchi-Elgot-Trakhtenbrot theorem3 establishes that

A language (set of words) $L$ is regular if and only if it is definable in monadic second-order logic (i.e. the set of its structures $K_L$ is definable in $MSOL$).

(note a formal language defines a decision problem over satisfiability of inputs)

The Cook-Levin theorem states that boolean satisfiability (SAT) is NP-complete.

References

  1. N. Immerman, “Second-Order Logic and Fagin’s Theorem,” in Descriptive Complexity, New York, NY: Springer New York, 1999, pp. 113–124. doi: 10.1007/978-1-4612-0539-5_8

  2. Bannach, M., Chudigiewitsch, F., & Tantau, T. (2023). Existential second-order logic over graphs: Parameterized complexity. arXiv preprint arXiv:2310.01134. https://arxiv.org/abs/2310.01134 

  3. J. A. Makowsky, Lecture Notes, Topic: “Lecture 3: Disjoint unions and concatenation, Finite Automata, Regular Languages, The Büchi-Elgot-Trakhtenbrot Theorem.” 236331, Technion, Fall 2018. https://janos.cs.technion.ac.il/COURSES/236331-18/Lec-3.pdf