14 Descriptive complexity
Descriptive complexity characterizes complexity classes by the logics that define their problems, after Immerman and Fagin. Once a class is captured by a logic, a lower bound becomes a question of what the logic can express. The development lives in Complexitylib.DescriptiveComplexity. The following are formalized:
finite structures over finite vocabularies, their isomorphisms, and injective homomorphisms and substructure inclusions between them;
first-order logic with de Bruijn variables, substitution, and invariance under isomorphism;
Boolean queries, order independence, and first-order definability;
second-order logic, its \(\exists \mathsf{SO}\) fragment, and invariance under isomorphism;
a bit-string encoding of structures and the language a query induces;
a computable first-order model checker, proved correct, with no bound on its running time;
universe-preserving (dimension-1) first-order reductions and their quantifier-free restriction, both of which are preorders.
No capture theorem is formalized yet, and the link from logic to machines stops at the definition of the language of a query: there is no decoder, no running-time bound, and no machine construction. The main planned result is Fagin’s theorem \(\mathsf{NP} = \exists \mathsf{SO}\). Later planned results are \(\mathsf{FO} \subseteq \mathsf{AC^0}\) and the Immerman–Vardi theorem.
Conventions.
A structure has universe \(\mathrm{Fin}(n)\) with \(n \ge 2\) (Immerman’s Proviso 1.15). Queries are properties of structures with \(\mathrm{Prop}\)-valued relations. The encoding and the model checker take decidable structures, whose relations are \(\mathrm{Bool}\)-valued and which coerce to ordinary structures. The canonical order on \(\mathrm{Fin}(n)\) is available as meta-level helpers, but the first- and second-order syntax is unordered, so formulas cannot mention it. Order independence is therefore a theorem about the existing logics rather than a restriction imposed on them.
14.1 Vocabularies and finite structures
A vocabulary has \(r\) relation symbols, indexed by \(\mathrm{Fin}(r)\), each with an arity in \(\mathbb {N}\), and \(c\) constant symbols, indexed by \(\mathrm{Fin}(c)\). It is relational if \(c = 0\). The graph vocabulary has one binary relation symbol and no constants.
A finite structure \(\mathcal{A}\) over \(V\) consists of:
a size \(n \ge 2\) and the universe \(\mathrm{Fin}(n)\);
for each relation symbol of arity \(k\), a \(\mathrm{Prop}\)-valued relation on \(k\)-tuples, that is, on maps \(\mathrm{Fin}(k) \to \mathrm{Fin}(n)\);
for each constant symbol, an element.
A decidable structure has the same data, with \(\mathrm{Bool}\)-valued relations, and coerces to a structure in which a relation holds where its value is \(\mathrm{true}\). The canonical order \(\le \), the successor relation (\(b = a + 1\)), the minimum \(0\), and the maximum \(n - 1\) of \(\mathrm{Fin}(n)\) are defined for every structure as meta-level helpers. They are not part of the structure, and no formula can mention them.
An isomorphism \(\mathcal{A} \cong \mathcal{B}\) is a pair of mutually inverse maps between the universes whose forward map preserves and reflects every relation and preserves constants. Isomorphisms have identities, inverses, and composites. An embedding is an injective map that preserves and reflects every relation and preserves constants, as in model theory; its image is a substructure of \(\mathcal{B}\) isomorphic to \(\mathcal{A}\). Embeddings have identities and composites, and every isomorphism is one. An injective homomorphism only preserves relations, so \(\mathcal{B}\) may relate images of unrelated elements; every embedding is one. All three notions carry their maps as data.
If \(\mathcal{A} \cong \mathcal{B}\), then \(|\mathcal{A}| = |\mathcal{B}|\).
Both maps are injections between \(\mathrm{Fin}\) types, so the pigeonhole principle applies in each direction.
14.2 First-order logic
Terms with \(k\) free variables are de Bruijn variables \(x_i\) (\(i {\lt} k\)) or constant symbols. Formulas are built from relation atoms, equality, \(\neg \), \(\wedge \), \(\vee \), \(\exists \), and \(\forall \). A quantifier binds variable \(0\) and shifts the others. Sentences are formulas with no free variables. Quantifier rank (the quantifier nesting depth) and size (the number of nodes) are defined by structural recursion.
An environment for \(k\) free variables is a map \(\mathrm{Fin}(k) \to \mathrm{Fin}(|\mathcal{A}|)\). Extending it by an element puts that element at index \(0\) and shifts the others. Satisfaction \(\mathcal{A}, \sigma \models \varphi \) is Tarskian, and quantifiers range over \(\mathrm{Fin}(|\mathcal{A}|)\). \(\mathcal{A} \models \varphi \) means satisfaction of a sentence under the empty environment.
Let \(f : \mathcal{A} \cong \mathcal{B}\). For every term \(t\) and environment \(\sigma \), the value of \(t\) in \(\mathcal{B}\) under \(f \circ \sigma \) is the image under \(f\) of its value in \(\mathcal{A}\) under \(\sigma \). For every formula \(\varphi \) and environment \(\sigma \), \(\mathcal{A}, \sigma \models \varphi \) iff \(\mathcal{B}, f \circ \sigma \models \varphi \).
Terms are variables or constants, and \(f\) preserves constants. For formulas, induct on \(\varphi \). Quantifier cases move witnesses along \(f\) and \(f^{-1}\).
Simultaneous substitution \(\varphi [\rho ]\) takes a formula with \(m\) free variables and terms \(\rho (0), \dots , \rho (m-1)\) with \(n\) free variables, and replaces each \(x_k\) by \(\rho (k)\), giving a formula with \(n\) free variables. Under a binder, the substitution is lifted: variable \(0\) stays, and every other image is shifted up one de Bruijn index.
For every structure \(\mathcal{A}\), environment \(\sigma \), substitution \(\rho \), and formula \(\varphi \), \(\mathcal{A}, \sigma \models \varphi [\rho ]\) iff \(\mathcal{A}, (k \mapsto \rho (k)^{\mathcal{A},\sigma }) \models \varphi \). Substitution preserves quantifier rank exactly.
Induct on \(\varphi \), generalizing over the number of free variables, and use a lemma evaluating lifted substitutions.
14.3 Boolean queries and definability
A Boolean query over \(V\) is a property of finite \(V\)-structures. It is order-independent if isomorphic structures agree on it, that is, if it is invariant under isomorphism. Complement, intersection, and union are defined pointwise.
Order-independent queries are closed under complement, intersection, and union.
Immediate from the definitions.
For every sentence \(\varphi \), the query \(\mathcal{A} \mapsto (\mathcal{A} \models \varphi )\) is order-independent (Immerman, Proposition 1.16).
Specialize isomorphism invariance to the empty environment. As a worked check, cycle3_fo_indistinguishable applies this to two explicitly isomorphic directed 3-cycles, which therefore satisfy the same sentences.
\(Q\) is first-order definable if some sentence \(\varphi \) satisfies \(Q(\mathcal{A}) \iff \mathcal{A} \models \varphi \) for every \(\mathcal{A}\).
Every first-order definable query is order-independent. First-order definable queries are closed under complement, intersection, and union.
Use the defining sentence, and \(\neg \), \(\wedge \), \(\vee \) for the closure properties.
14.4 Second-order logic
Second-order formulas extend first-order formulas with two constructs: applications of relation variables, and second-order quantifiers \(\exists R\), \(\forall R\) over a fresh relation of a given arity. Relation variables are de Bruijn-indexed by a context listing their arities, innermost first. A second-order sentence has an empty relation context and no free element variables. First-order formulas embed into second-order formulas over any relation context. Size counts nodes.
A relation environment assigns to each relation variable in the context a \(\mathrm{Prop}\)-valued relation of its arity on the universe. Extending it puts the new relation at index \(0\). Satisfaction is defined under an element environment and a relation environment, and second-order quantifiers range over all \(\mathrm{Prop}\)-valued relations of the quantified arity on the universe. \(\mathcal{A} \models \varphi \) for a second-order sentence means satisfaction under the empty environments.
A formula is an FO matrix if it has no second-order quantifiers, though it may apply relation variables and use first-order quantifiers. It is in \(\exists \mathsf{SO}\) form if it is a possibly empty block of second-order existential quantifiers followed by an FO matrix.
\(Q\) is second-order definable if some second-order sentence \(\varphi \) satisfies \(Q(\mathcal{A}) \iff \mathcal{A} \models \varphi \) for every \(\mathcal{A}\).
For every relation environment \(\rho \), the embedding of a first-order formula holds at \((\sigma , \rho )\) exactly when the original holds at \(\sigma \). In particular, a structure models the embedding of a sentence iff it models the sentence. The embedding is an FO matrix, hence in \(\exists \mathsf{SO}\) form with an empty quantifier block. Consequently every first-order definable query is second-order definable.
Induct on the first-order formula.
Along \(f : \mathcal{A} \cong \mathcal{B}\), a second-order formula holds at \((\sigma , \rho )\) iff it holds at \((f \circ \sigma , f_*\rho )\), where \(f_*\rho \) transports each relation along \(f\): \((f_*\rho )(R)(\bar b) = \rho (R)(f^{-1} \circ \bar b)\). In particular, isomorphic structures satisfy the same second-order sentences.
Induct on the formula. For second-order quantifiers, push relations forward along \(f\) and pull them back along \(f^{-1}\).
Every second-order definable query is order-independent. In particular, so is every query defined by a sentence in \(\exists \mathsf{SO}\) form. Second-order definable queries are closed under complement, intersection, and union.
Specialize to the empty environments, and use \(\neg \), \(\wedge \), \(\vee \) for the closure properties.
14.5 Encodings and model checking
A decidable structure of size \(n\) is encoded, computably, as the concatenation of three blocks:
the size in unary, \(1^n 0\);
for each relation symbol in index order, its truth table, listed over a computable enumeration of all tuples of its arity;
for each constant symbol in index order, a one-hot block of length \(n\) whose bit \(i\) is \(1\) exactly when the constant is \(i\).
The encoding depends on the canonical order of \(\mathrm{Fin}(n)\).
The enumeration of \(k\)-tuples has length \(n^k\) and contains every \(k\)-tuple, so a truth table of arity \(k\) has length \(n^k\). A one-hot block has length \(n\). The encoding has length \(n + 1 + \sum _R n^{\mathrm{ar}(R)} + c \cdot n\), where \(c\) is the number of constants, and for a relational vocabulary it is the unary block followed by the truth tables alone. The size \(n\) is recoverable as the length of the leading block of ones, and a one-hot constant block determines its element.
Induct on the arity, then sum block lengths.
The language of \(Q\) is \(\{ \mathrm{enc}(\mathcal{A}) : \mathcal{A} \text{ decidable}, Q(\mathcal{A})\} \), where \(Q\) is applied to the structure that \(\mathcal{A}\) coerces to. By definition every string in it is an encoding, and the encoding of a decidable structure satisfying \(Q\) lies in it. This is the bridge from queries to the machine-model languages.
A computable parser \(\mathrm{dec} : \{ 0,1\} ^* \to V\text{-structures} \cup \{ \bot \} \). It reads the unary size and then the fixed-length relation and constant blocks, and returns \(\bot \) on malformed input, including a size below \(2\) and a constant block that is not one-hot.
\(\mathrm{dec}(\mathrm{enc}(\mathcal{A})) = \mathcal{A}\), up to extensional equality of relations. Hence \(\mathrm{enc}\) is injective, and \(x \in \mathrm{queryLanguage}(Q)\) iff \(\mathrm{dec}(x) = \mathcal{A} \neq \bot \) and \(Q(\mathcal{A})\).
Recover the size with encodeStruct_card, then split the remainder by the known block lengths.
A computable \(\mathrm{Bool}\)-valued evaluator for first-order formulas on decidable structures. Atoms look up the \(\mathrm{Bool}\)-valued relations, and quantifiers become any and all over the list of universe elements. The sentence form runs it under the empty environment.
For every decidable structure \(\mathcal{A}\), formula \(\varphi \), and environment \(\sigma \), \(\mathrm{evalB}(\mathcal{A}, \sigma , \varphi ) = \mathrm{true}\) iff \(\mathcal{A}, \sigma \models \varphi \), and likewise for sentences under the empty environment. Hence \(\mathcal{A} \models \varphi \) is decidable for every decidable structure \(\mathcal{A}\) and sentence \(\varphi \). This is correctness only: no bound on the evaluator’s running time and no machine implementation are formalized.
Induct on \(\varphi \).
For every first-order sentence \(\varphi \), the language of the query \(\mathcal{A} \mapsto (\mathcal{A} \models \varphi )\) is in \(\mathsf{P}\).
Parse the input, then run the model checker. With \(\varphi \) fixed, it makes \(O(n^{\mathrm{qr}(\varphi )})\) recursive calls, each reading truth-table and constant bits at computable offsets. The same recursion with one logarithmic-size counter per quantifier would give the stronger bound \(\mathsf{FO} \subseteq \mathsf{L}\).
14.6 First-order reductions
A dimension-1 interpretation \(I : V \to W\) consists of a \(V\)-formula with \(\mathrm{ar}(R)\) free variables for each relation symbol \(R\) of \(W\), and a source constant for each constant of \(W\). Applying \(I\) to a \(V\)-structure gives a \(W\)-structure on the same universe, in which \(R\) holds exactly where its defining formula does. Formulas translate backwards along \(I\), from \(W\) to \(V\): a target atom becomes its defining formula with the translated argument terms substituted, and a target constant becomes its source constant. Interpretations \(U \to V\) and \(V \to W\) compose to one \(U \to W\) by translating the outer defining formulas. The identity interpretation defines each relation by its own atom and sends each constant to itself.
For every \(V\)-structure \(\mathcal{A}\), environment \(\sigma \), and \(W\)-formula \(\varphi \), \(I(\mathcal{A}), \sigma \models \varphi \) iff \(\mathcal{A}, \sigma \models I^*\varphi \), and a translated term takes the same value in \(\mathcal{A}\) as the original term in \(I(\mathcal{A})\). Composition of interpretations acts as composition of the structure maps, \((I_2 \circ I_1)(\mathcal{A}) = I_2(I_1(\mathcal{A}))\), and the identity interpretation acts as the identity.
Induct on \(\varphi \). At a relation atom, substitute the translated argument terms into the defining formula. The composition law follows by applying the transport theorem to each defining formula.
For queries \(Q_1\) over \(V\) and \(Q_2\) over \(W\), \(Q_1 \le _{\mathsf{FO}} Q_2\) if some dimension-1 interpretation \(I : V \to W\) has \(Q_1(\mathcal{A}) \iff Q_2(I(\mathcal{A}))\) for all \(V\)-structures \(\mathcal{A}\). An interpretation is quantifier-free if every defining formula has quantifier rank \(0\). \(Q_1\) first-order projection reduces to \(Q_2\) if such an \(I\) can be chosen quantifier-free. This condition is coarser than Immerman’s projective form, in which each target bit depends on a single source bit.
First-order reducibility and first-order projection reducibility are reflexive and transitive, across vocabularies. Every projection is a reduction, and a reduction from \(Q_1\) to \(Q_2\) is, through the same interpretation, also a reduction from \(\overline{Q_1}\) to \(\overline{Q_2}\). The identity interpretation is quantifier-free, translation along a quantifier-free interpretation preserves the quantifier rank of every formula, and composites of quantifier-free interpretations are quantifier-free.
Use the identity interpretation and composition, with the composition law of the transport theorem. Translation along a quantifier-free interpretation replaces each atom by a quantifier-free formula with terms substituted, and substitution preserves quantifier rank, so quantifier rank is preserved and composites stay quantifier-free.
If \(Q_1 \le _{\mathsf{FO}} Q_2\) and \(Q_2\) is first-order definable, then so is \(Q_1\). In particular, this holds when \(Q_1\) first-order projection reduces to \(Q_2\).
Translate the sentence defining \(Q_2\) backwards along the interpretation. A projection is a reduction.
A dimension-\(k\) interpretation defines the target universe as a definable subset of \(\mathrm{dom}^k\). Each target relation of arity \(a\) is defined by a formula with \(a k\) free variables. This requires a codec \(\mathrm{Fin}(n^k) \simeq (\mathrm{Fin}(k) \to \mathrm{Fin}(n))\) and a way to assemble environments for the \(a k\) variables.
The transport theorem holds for dimension-\(k\) interpretations. They compose (dimensions multiply), so dimension-\(k\) reducibility is a preorder that contains dimension-1 reducibility.
Replace each target variable by a block of \(k\) source variables and relativize quantifiers to the definable universe.
If \(Q_1 \le _{\mathsf{FO}} Q_2\), then the language of \(Q_1\) polynomial-time many-one reduces to the language of \(Q_2\).
Decode the input. Compute each target truth table by model-checking the defining formulas, and re-encode. Send malformed inputs to a fixed non-encoding, such as the empty string: every encoding has length at least \(n + 1 \ge 3\).
14.7 Capturing complexity classes
First-order logic extended with atoms for the canonical order \(\le \), successor, minimum, and maximum of \(\mathrm{Fin}(n)\). These atoms are interpreted by the existing meta-level helpers. The existing unordered syntax and its unrestricted invariance theorem stay unchanged. Ordered sentences are preserved only by maps that respect the canonical order, and they need not define order-independent queries.
Let \(\varphi \) be a second-order sentence in \(\exists \mathsf{SO}\) form that defines \(Q\). Then the language of \(Q\) is in \(\mathsf{NP}\).
The certificate is the truth tables of the quantified relations, of polynomial total length \(\sum _j n^{k_j}\). The verifier model-checks the FO matrix under the resulting relation environment, extending evalB to relation variables.
Let \(Q\) be order-independent with language in \(\mathsf{NP}\). Then some second-order sentence in \(\exists \mathsf{SO}\) form defines \(Q\).
Existentially quantify a linear order together with a computation tableau of an \(n^k\)-time verifier, indexed by \(k\)-tuples. First-order-check the tableau’s initial row (the encoding of the structure under the guessed order), its local transition windows, and acceptance. Order independence makes the guessed order harmless.
An order-independent query has its language in \(\mathsf{NP}\) if and only if it is definable by an \(\exists \mathsf{SO}\) sentence.
Combine the two inclusions. Order independence of \(\exists \mathsf{SO}\)-definable queries is already formalized.
For every first-order sentence \(\varphi \), consider the characteristic family of the language of \(\mathcal{A} \mapsto (\mathcal{A} \models \varphi )\): the Boolean function at input length \(N\) is the indicator of the language restricted to \(\{ 0,1\} ^N\). This family lies in \(\mathsf{AC^0}\).
The encoding length is strictly increasing in the universe size, so at most one size \(n\) has encodings of length \(N\). Build a circuit that checks the unary prefix and that each constant block is one-hot. Replace each quantifier by an unbounded fan-in gate of fan-in \(n\), and each atom by an input bit, or by an unbounded fan-in selection over the one-hot block when an argument is a constant. The depth is \(O(\lvert \varphi \rvert )\), a constant, and the size is polynomial in \(n\), hence in \(N\).
On ordered structures with a BIT predicate, the first-order definable queries are exactly those whose languages have \(\mathsf{DLOGTIME}\)-uniform \(\mathsf{AC^0}\) circuit families. This makes the previous theorem uniform and adds its converse.
One direction refines the circuit construction to a uniform one. For the other, describe the uniform circuit’s gates by first-order formulas over tuples and evaluate the circuit by a first-order formula of depth proportional to the circuit’s depth. Neither uniform \(\mathsf{AC^0}\) nor BIT is defined yet.
\(\mathsf{FO}(\mathrm{LFP})\) extends first-order logic with \([\mathrm{lfp}_{R,\bar x}\, \varphi ](\bar t)\) for \(\varphi \) positive in \(R\). It is interpreted as the least fixed point of the monotone operator that \(\varphi \) induces on relations of the arity of \(R\). That fixed point is reached after at most \(n^{\mathrm{ar}(R)}\) iterations.
On ordered structures, a query is \(\mathsf{FO}(\mathrm{LFP})\)-definable if and only if its language is in \(\mathsf{P}\).
\(\subseteq \): iterate each fixed point at most polynomially many times. \(\supseteq \): use the ordering to define the computation tableau of a polynomial-time machine by a least fixed point, as in the proof of Fagin’s theorem but without guessing.
14.8 Open directions
Immerman’s exact projective reductions (each target bit determined by one source bit under a quantifier-free guard) are not yet defined. Neither is a worked completeness result under first-order projections. Both are prerequisites for treating first-order projections as the reductions under which the standard \(\mathsf{AC^0}\)-, \(\mathsf{L}\)-, and \(\mathsf{NL}\)-complete problems are complete.