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;
canonical vocabulary extensions for strict order, BIT, addition, and multiplication, with atomic semantics and preservation of input formulas;
Boolean queries, order independence, and first-order definability;
second-order logic, its \(\exists \mathsf{SO}\) fragment, and invariance under isomorphism;
arity-preserving relation renaming and existential-prefix conjunction and disjunction, proving intersection and union closure for \(\exists \mathsf{SO}\);
Boolean relation witnesses, verified FO-matrix evaluation, and an executable checker for a supplied graph bipartition;
exact binary relation certificates and sound, complete existential-SO certificate checking with polynomial witness lengths on encoded inputs;
polynomial-time existential-SO certificate checking and Fagin’s upper direction \(\exists \mathsf{SO}\subseteq \mathsf{NP}\) for the existing machine class;
a bit-string encoding of structures and the language a query induces;
a correct computable first-order model checker, with polynomial-time machines computing each fixed sentence’s encoded verdict;
compilation of first-order model checking into unbounded Boolean formula trees, with table-input correctness, exact polynomial size, and depth independent of the universe size for each fixed source formula;
exact decoding, constant-depth encoding validation, and circuit families proving \(\mathsf{FO} \subseteq \mathsf{AC^0}\) for the induced binary languages;
arithmetic encoding addresses, polynomial-time input access, and recognition of valid encodings in the deterministic machine class \(\mathsf{P}\);
\(\mathsf{FO}\subseteq \mathsf{P}\) for the induced binary query languages, including rejection of malformed inputs;
universe-preserving (dimension-1) first-order reductions and their quantifier-free restriction, both of which are preorders;
polynomial-time encoded maps for those interpretations, giving machine many-one reductions and a structural NP-completeness criterion;
second-order transport through those reductions, preserving existential second-order prefix form, and existential SO definability;
full tagged tuple interpretations, with exact size, formula pullback, and composition up to isomorphism, including the original dimension-1 maps;
exact arithmetic encodings of tagged interpretations, including all relation and constant blocks; their machine time bound remains open;
invariant decision problems and a tagged reduction preorder, with downward closure of first-order definability;
a bipartite sentence equivalent to Boolean coloring, and the two-copy graph interpretation with its proved bipartition, as well as disjoint copies as a reduction preserving bipartiteness.
The nonuniform circuit inclusion uses the existing binary encoding and rejects malformed inputs at every length, including zero. Fixed-formula evaluation also has a bound against the machine polynomial-time predicate, as does existential-SO certificate checking. The latter yields \(\exists \mathsf{SO}\subseteq \mathsf{NP}\). Planned results include the converse direction of Fagin’s theorem, the Immerman–Vardi theorem, and the ordered \(\mathsf{FO}[\mathrm{BIT}]\) characterization of uniform \(\mathsf{AC^0}\).
The current expansion draws on Pierre Senellart and Anton Gnatenko, Descriptive Complexity in Lean: Completeness by First-Order Reductions (arXiv:2609.18261, 2026), especially its interpretation and definability interfaces. Their logically defined classes and our machine-defined classes require an explicit bridge. The implementation sequence and source comparison are recorded in docs/DescriptiveComplexity.md.
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 core syntax treats all relation symbols uniformly. Explicit numerical vocabulary extensions make canonical order, BIT, addition, and multiplication available as ordinary first-order atoms. Their definability predicate evaluates sentences only on canonical expansions of input structures; the resulting queries may depend on the input labeling. The existing isomorphism-invariance theorem concerns the entire vocabulary, including any added symbols, and does not assert independence from an auxiliary order.
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.
A quantifier block binds the first \(k\) variables of a formula; its environment places the \(k\) coordinates before the old variables. Terms can be shifted across an entire block. Finite conjunctions and disjunctions are iterated binary connectives, with truth and falsity as their respective empty cases.
Shifting a term across a block preserves its value. Existential and universal blocks quantify over all coordinate tuples; finite conjunction and disjunction mean that every, respectively some, indexed formula holds. These statements include zero-length blocks and empty index sets.
Induct on the block length or connective list. Extend and restrict tuples by their head and tail in the quantifier cases.
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.
A decision problem bundles a query with its isomorphism invariance. Logical definability supplies this law. Complement, intersection, and union inherit it. This is the interface of Senellart–Gnatenko, Section 3.1, restricted to our convention of at least two elements.
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.
A relation renaming maps de Bruijn indices between contexts while preserving each relation’s arity. Its lift fixes a newly bound relation and renames the older variables. Weakening shifts all free relation indices past a fresh binder. Formula renaming lifts beneath both kinds of SO quantifier, leaving element variables and vocabulary symbols unchanged. Pullback reads a target relation environment at the renamed source indices.
Satisfaction after renaming is satisfaction under the pulled-back relation environment, for arbitrary free element and relation assignments. Weakening ignores the new relation. Identity and composition hold as exact equalities of syntax, and renaming preserves size and preserves and reflects both FO matrices and existential SO prefix form. These statements include nullary relation variables and do not require an injective renaming.
Split relation indices into the fresh head and the older tail to prove the environment laws. Induct on formulas, using the lifted renaming under SO quantifiers. Arity preservation makes each renamed relation atom well-typed.
To conjoin or disjoin two existential SO formulas, move each leading existential relation quantifier outward, weakening the other operand past its binder. Once both prefixes have been removed, conjoin or disjoin the matrices. The total operation is also defined on arbitrary SO formulas; it moves only their leading existential SO quantifiers. This implements the existential prefix manipulation in Immerman, Section 7.1.
The resulting formulas have the usual conjunction and disjunction semantics under arbitrary free-variable environments. If both operands are in existential SO prefix form, so is the result. Each operation has size exactly \(|\varphi |+|\psi |+1\), with no duplication of either formula.
Induct over prefix merging. Weakening makes the other operand independent of the relation being quantified. Move the quantifier past the connective; for disjunction, an unused witness can be any relation, including the empty one. The sum of operand sizes decreases at each recursive step, since renaming preserves size and the step removes one quantifier. The final connective adds exactly one syntax node.
\(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.
A query is existential second-order definable if a sentence in \(\exists \mathsf{SO}\) prefix form defines it on every structure.
Every existential SO query is SO definable and invariant under isomorphism. Every FO-definable query is existential SO definable with an empty prefix. Existential SO definable queries are closed under intersection and union.
Forget the fragment certificate for the first claim, and embed the FO witness into SO for the second. Merge the existential witness prefixes for intersection and union, retaining the syntactic fragment certificate.
A graph is bipartite if a Boolean color assignment gives different colors to the endpoints of every directed edge. Symmetry and loop-freeness are not assumed. Its proposed sentence is \(\exists X\, \forall x\, \forall y\, (E(x,y)\to (X(x)\leftrightarrow \neg X(y)))\).
The sentence defines exactly the bipartite query. An edgeless graph satisfies it, and a graph with a self-loop does not.
A unary relation determines a Boolean color by its characteristic function; conversely, take the vertices with color true. The edge condition is exactly disagreement of the colors. This is the example in Senellart–Gnatenko, Section 2.1, proved against an independently stated coloring predicate.
Given a decidable graph and a Boolean color for each vertex, supply that color table to the two-universal-quantifier FO matrix of the bipartite sentence and evaluate the matrix.
The checker accepts exactly when every directed edge joins vertices of different colors. A graph is bipartite iff some Boolean coloring is accepted. On an encoded graph, the general binary certificate checker agrees with this checker when the certificate lists one color bit per vertex. Existence of an accepted certificate characterizes the ordinary bipartite-graph query language.
Apply matrix-evaluation correctness and the semantic characterization of the bipartite matrix. For Boolean values, the relation condition is precisely inequality of the two colors. Unary truth-table encoding lists colors in vertex order, and the prefix checker consumes exactly that table.
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.
Enumerate relation and constant-table sites in the encoder’s order. A site’s bit position is its index in this list plus \(n+1\) for the unary prefix. The full length is \(\ell _V(n)=n+1+\sum _R n^{\mathrm{ar}(R)}+cn\).
Every table site occurs exactly once in the enumeration, its position is below \(\ell _V(n)\), and reading that position in an encoded structure recovers exactly its table value. Moreover \(n{\lt}\ell _V(n)\), and \(\ell _V\) is strictly increasing. Thus a fixed input length corresponds to at most one universe size. Correct length, header bits, and table bits characterize the complete encoding.
Map the site list to its values to recover the existing truth-table encoder. Use completeness and cardinality of the tuple enumeration for uniqueness and lookup; list extensionality gives reconstruction. Every table-length term is monotone in \(n\), while the unary prefix is strictly increasing.
A tuple has the little-endian base-\(n\) index \(a_0+n a_1+\cdots +n^{k-1}a_{k-1}\). The address of a relation-table entry adds \(n+1\) for the header and the lengths of all earlier relation tables. A constant-table address adds the header, all relation-table lengths, \(cn\) for the preceding \(c\) constant blocks, and the chosen element’s value. Fixed-width tuple decoding repeatedly takes remainder and quotient by \(n\), recovering coordinates from an index in the same little-endian order.
For coordinates below \(n\), a \(k\)-tuple’s index is below \(n^k\) and selects that tuple in the encoder’s enumeration. The arithmetic relation and constant addresses equal their existing site positions exactly. Reading these addresses in a structure encoding recovers the relation bit or the indicated one-hot equality. The tuple index also recovers a bit from a standalone relation truth table. This includes nullary relations and empty tuples. For \(n{\gt}0\), every decoded coordinate is below \(n\), re-encoding recovers every index below \(n^k\), and scanning numeric indices reproduces the tuple enumeration.
Prove that indexing a flattened list uses the total length of preceding blocks plus the index inside the chosen block. Induct on tuple length for the base-\(n\) index, then apply the flattened-list rule to the relation and constant blocks. The site enumeration has no duplicates, so its inverse index is the same arithmetic position.
For a fixed vocabulary, relation symbol, and tuple arity, polynomial-time unary cardinality and coordinates give polynomial-time unary tuple indices, relation addresses, and constant addresses. Each fixed coordinate extracted from a polynomial-time unary tuple index is also polynomial-time. The full structure length and any fixed relation context’s certificate length are polynomial-time unary numbers. Parsing cardinality from the leading true run and testing the expected encoded length are polynomial-time. Relation and constant bit tests at these addresses are polynomial-time predicates on any supplied \(\mathsf{FP}\) string, with false at missing positions.
Each address and length is a fixed sum of products and fixed powers. Apply the unary arithmetic closure rules, then polynomial-time bit access. The prefix parser is the leading-run construction of Lemma 139.
At cardinality \(n\), require \(n\ge 2\), total length \(\ell _V(n)\), header bits \(1^n0\), and exactly one true bit in every constant block. Express the latter as: for each constant there is an \(a{\lt}n\) such that every \(b{\lt}n\) has block bit equal to the truth value of \(a=b\). Relation-table bits are unrestricted.
The validity conditions hold iff the string encodes a structure of the specified size. Applying them at the cardinality parsed from the unary prefix recognizes exactly the encoder’s image. The conditions are polynomial-time predicates, so \(\{ \mathrm{enc}(\mathcal A):\mathcal A\text{ is a decidable }V\text{-structure}\} \in \mathsf{P}\) for the library’s deterministic machine class. Successful decoding is likewise a polynomial-time predicate. No formula-evaluation time bound is asserted by this theorem.
The forward direction constructs the relations by reading their table bits and the constants from the unique marked values. The address equalities and encoding reconstruction theorem recover the whole string. The converse uses the encoder’s header and table-read theorems. Header and one-hot checks are bounded quantifiers over polynomial-time bit reads and arithmetic comparisons. Combine them with the length and minimum-size tests, parse the cardinality, and apply the polynomial-time decision-function theorem.
A computable parser \(\mathrm{dec} : \{ 0,1\} ^* \to V\text{-structures} \cup \{ \bot \} \). It checks the unary size and total length, reads relation bits and the first set bit in each constant block, and accepts only when re-encoding this candidate reproduces the entire input. It returns \(\bot \) on malformed input, including a size below \(2\), a constant block that is not one-hot, or trailing data.
\(\mathrm{dec}(\mathrm{enc}(\mathcal{A})) = \mathcal{A}\) exactly, with extensional equality of the relation and constant functions. Decoding returns \(\mathcal{A}\) iff its encoding equals the input; rejection is equivalent to being outside the encoder’s image. 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; position lookup recovers each relation bit and the unique set bit in every constant block. The candidate is therefore the original structure. The final re-encoding check proves the converse for arbitrary input strings.
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 node concerns semantic correctness; Theorem 1312 supplies the polynomial-time machine bound for fixed sentences on encoded structures.
Induct on \(\varphi \).
A Boolean relation environment assigns a Boolean table of the prescribed arity to every free relation variable. Interpret true bits as relation membership. Given an FO-matrix certificate, evaluate vocabulary atoms in the decidable structure, relation-variable atoms in these tables, and first-order quantifiers over the finite universe. Second-order quantifiers are excluded by the matrix certificate. Satisfaction with these inputs is decidable.
Boolean relation environments represent exactly the semantic environments, and representation commutes with extension. The matrix evaluator returns true iff the matrix is satisfied under the represented environment. On an embedded FO formula it agrees exactly with the original FO evaluator. Existential, or universal, quantification over semantic relation environments is equivalent to quantification over Boolean tables tested by the evaluator. These statements include empty contexts and nullary relation variables. This theorem concerns semantic environments; the following certificate layers supply their binary encodings. Theorem 1315 proves the machine polynomial-time bound on those encodings.
Boolean values are determined by whether they equal true. Classically, the characteristic function of each semantic relation gives its Boolean table. Induct on the matrix for evaluation correctness, using finite enumeration for first-order quantifiers. Represent every semantic environment by its Boolean tables to transport existential and universal quantification. This is the verification step of Immerman, Section 7.1, Proposition 7.6.
For a universe of size \(n\) and relation arities \(k_1,\ldots ,k_m\), concatenate the relation truth tables in context order, using the structure encoder’s tuple enumeration. The arities and \(n\) are external parameters, so no header is needed. The expected length is \(\sum _j n^{k_j}\). Direct reading supplies false for missing entries; the checked decoder accepts only the exact length.
Encoding bijects Boolean relation environments with strings of exactly \(\sum _j n^{k_j}\) bits. Both round trips hold, and rejection means precisely a length mismatch. Extending the context prepends the new table; a unary table lists its bits in vertex order. Nullary relations take one bit and the empty context takes none. The exact length is a polynomial in \(n\), monotone in \(n\).
Every table cell occurs in the site enumeration. Its length equals the cardinality of the site type, so there are no duplicates. Reading at the index of a cell and indexing a duplicate-free enumeration give the two inverse laws. Sum the individual table lengths; each is \(n^{k_j}\).
List the existential prefix’s arities from outermost to innermost. Consume one truth-table block at each relation quantifier, extending the Boolean relation environment. At the FO matrix, require an empty remaining certificate and run matrix evaluation. For an encoded input, first decode the structure and reject if decoding fails. These are computable functions.
For every existential-SO formula and supplied free environments, an accepted binary certificate exists iff the formula is satisfied. Every accepted certificate has exactly \(\sum _j n^{k_j}\) bits. For a sentence defining \(Q\),
Malformed structure encodings and incorrect certificate lengths are rejected. Theorem 1315 proves the checker’s polynomial machine running-time bound.
Induct along the existential prefix. A decoded table supplies a semantic relation; conversely, the characteristic function of a semantic witness supplies its encoded table. Matrix correctness closes the induction, and requiring no remaining bits gives the exact certificate length. Decode the structure to obtain the language characterization. The unary cardinality prefix gives \(n\le |x|\); monotonicity transfers the length polynomial from universe size to input length. This formalizes the certificate and semantic verification parts of Immerman, Proposition 7.6.
Decode the input string, evaluate the sentence on a successfully decoded structure, and return false if decoding fails.
The encoded evaluator returns true exactly on the induced query language, for every input string. On an encoded structure it agrees with the original structure-level evaluator. Theorem 1312 proves that a polynomial-time machine computes this verdict for each fixed sentence.
Split on decoding and combine its exact success characterization with correctness of sentence evaluation.
Given a cardinality \(n\), a bit string, and natural-number variable values, evaluate terms and formulas directly by arithmetic table access. A constant is the first marked position in its one-hot block, or \(n\) if no position is marked. First-order quantifiers range over \(0,\ldots ,n-1\). The functions are total, including on malformed strings; semantic correctness requires a valid structure encoding and variable values in its universe.
On \(\mathrm{enc}(\mathcal{A})\), supplied with \(\mathcal{A}\)’s cardinality and the numeric values of an environment, arithmetic term evaluation recovers the semantic element’s value. Arithmetic formula evaluation returns true exactly when the formula is satisfied. The sentence case uses the empty environment.
One-hot lookup recovers each constant. Induct on the formula, using the exact arithmetic read lemmas for relation atoms and the correspondence between bounded naturals and elements of \(\mathrm{Fin}(n)\) at quantifiers.
Fix the vocabulary and formula. If the supplied string is an \(\mathsf{FP}\) function of the input, and the cardinality and free-variable values can be written in unary in polynomial time, then term values have the same unary polynomial-time property and the formula’s one-bit verdict belongs to \(\mathsf{FP}\). No encoding-validity assumption is needed for this time bound.
Constants use bounded search over polynomial-time bit tests. Induct on the formula using predicate closure under Boolean connectives and bounded quantifiers. The environment at a quantifier prepends the loop index to the previous polynomial-time values. The formula is fixed, so the induction applies the machine closure rules only a fixed number of times.
For a formula with \(k\) free variables, scan the indices \(0,\ldots ,n^k-1\), decode each index into its \(k\) coordinates, and record the arithmetic evaluator’s verdict. This produces the relation table in the encoder’s order.
The table has exactly \(n^k\) bits. On an encoded structure it equals the canonical relation encoding of the formula’s Boolean evaluator. For a fixed formula, generating the whole table is in \(\mathsf{FP}\) whenever the supplied string is in \(\mathsf{FP}\) and \(n\) is a polynomial-time unary number.
Arithmetic tuple decoding reproduces the original enumeration, and evaluation correctness identifies each bit. The output length \(n^k\) is polynomial-time for fixed \(k\); each bit is a polynomial-time fixed-formula evaluation on polynomial-time coordinates. Apply the bitwise output construction.
For every fixed first-order sentence \(\varphi \), the language of the query \(\mathcal{A} \mapsto (\mathcal{A} \models \varphi )\) is in the existing machine class \(\mathsf{P}\), and its encoded Boolean evaluator has a one-bit verdict in \(\mathsf{FP}\). Consequently, \(\operatorname {FODefinable}(Q)\) implies \(\operatorname {queryLanguage}(Q)\in \mathsf{P}\). Malformed strings are rejected. These are data-complexity results; neither polynomial combined complexity nor logarithmic space is asserted.
Parse the unary cardinality and conjoin encoding validity with arithmetic sentence evaluation. This is a polynomial-time predicate and agrees with query-language membership on every string. Apply the machine decision-function bridge. The existing encoded evaluator computes the same Boolean verdict, so its one-bit output belongs to \(\mathsf{FP}\) as well. This is the standard fixed-formula model-checking argument used in Immerman’s descriptive complexity development, with encoding validation included.
Supply each free relation as its truth-table string. Matrix evaluation uses arithmetic structure reads and tuple indices into these relation tables. Each existential relation quantifier checks that at least \(n^k\) bits remain, takes the next \(n^k\) bits as its new table, and recurses on the rest. At the matrix, require that no certificate bits remain. All operations are total; structure validity is checked separately.
On an encoded structure and canonical encodings of free relation tables, arithmetic matrix evaluation agrees with satisfaction and with the existing Boolean matrix evaluator. Arithmetic prefix consumption gives exactly the existing certificate checker’s verdict, for every certificate, including short or trailing data. The statements allow arbitrary free element and relation environments.
Induct on the matrix, using arithmetic tuple lookup for relation-variable atoms. Induct along the existential prefix for certificate checking. Singleton relation decoding succeeds exactly when its block has the required length; its round trip identifies that block with the decoded relation’s truth table.
For a fixed matrix or existential-SO formula, arithmetic verification is a polynomial-time predicate whenever the supplied strings are in \(\mathsf{FP}\) and the cardinality and element values are polynomial-time unary numbers. In particular, for every fixed existential-SO sentence \(\varphi \), the function
belongs to \(\mathsf{FP}\). Its verdict includes structure validation and rejection of incorrect certificate lengths. The formula is a fixed parameter.
Induct on the matrix using polynomial-time table reads, Boolean operations, and bounded first-order quantifiers. Induct along the existential prefix using polynomial-time length tests and slicing. Conjoin arithmetic verification with structure validity at the parsed cardinality. Agreement with the original checker transfers this machine bound to its existing verdict function.
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.
Pull an SO formula back through a universe-preserving interpretation by replacing vocabulary atoms by their defining FO formulas. Translate constants and retain relation variables, relation arities and all quantifiers.
Satisfaction is preserved under arbitrary element and relation environments. A pulled-back formula is an FO matrix, respectively in existential SO prefix form, exactly when the original is. Consequently SO definability and existential SO definability are closed under the existing FO reductions.
Induct on the formula. The interpreted universe is unchanged, so the same relations witness second-order quantification. Translate a defining sentence to obtain reduction closure.
For positive \(t,d\), the target universe is \(\mathrm{Fin}(t)\times \mathrm{Fin}(n)^d\), presented on \(\mathrm{Fin}(t n^d)\). A relation of arity \(a\) has a defining formula with \(ad\) variables for each assignment of tags to its arguments. Target constants are tagged tuples of source constants. This full-product construction has no domain restriction or quotient; it follows Senellart–Gnatenko, Section 3.2.
The output has exactly \(t n^d\) elements. Input isomorphisms act coordinatewise on the output, so invariant queries remain invariant under pullback of structures. Each original dimension-1 interpretation is the one-tag, one-coordinate case up to isomorphism, hence gives the same answer for any invariant target query.
Decode tagged tuples, apply the input isomorphism to each coordinate, and encode again. Formula invariance proves relation preservation. For the old interpretation, decode the sole coordinate and use the substitution lemma.
Give each source vertex a left and right copy. An output edge exists from \((0,x)\) to \((1,y)\) exactly when the source has \(E(x,y)\); no other tag pair carries an edge.
The two-copy graph has exactly \(2n\) vertices and the stated edges. It is bipartite for every input graph. This is an interpretation example, not a reduction preserving the source’s bipartiteness.
Unfold the relation formula and color by the tag.
Pullback replaces each free target variable by a tag and a tuple of source terms. Equality compares tags and all coordinates. Quantifiers become finite tag choices followed by coordinate blocks. Composition pulls the outer relation formulas back along the inner interpretation and flattens the nested tuples. This is the tagged full-product case of Immerman, Definition 3.3; constants are source-constant tuples as allowed in its footnote.
Pullback preserves satisfaction under arbitrary assignments, including open formulas, and preserves FO definability of queries. A source structure models a translated sentence exactly when its interpreted structure models the original. This is Immerman, Proposition 3.5 and Remark 3.6, for the tagged full-product construction. Composing parameters \((t_1,d_1)\) and \((t_2,d_2)\) gives \((t_2 t_1^{d_2},d_2d_1)\) and a structure isomorphic to successive application. The identity interpretation is isomorphic to its input. Translating along a composite agrees semantically with successive translations.
Induct on the formula with arbitrary source coordinate terms. The tuple codec transfers quantifier witnesses. Flattening nested tags and coordinates is a bijection; the open-formula theorem proves preservation of relations, and constant coordinates compose directly. Isomorphism invariance proves the semantic law for composite sentence translations.
A tagged reduction \(P \leq Q\) supplies positive tag and dimension counts, a tagged interpretation \(I\), and \(P(\mathcal A)\iff Q(I(\mathcal A))\) for every source structure. Reducibility is existence of such a witness. Identities, composites, and complementary reductions are explicit witnesses. On one vocabulary this relation defines a preorder; the API also supports reductions across vocabularies.
Tagged reducibility is reflexive, transitive, and respects complement. It includes the original universe-preserving reductions between invariant problems. If \(P\) reduces to an FO-definable \(Q\), then \(P\) is FO-definable.
Target invariance identifies the composite interpreted structure with successive application. Negate the membership equivalence for complement; translate a defining sentence for downward closure. The old reduction is the one-tag, one-coordinate case up to isomorphism.
For a fixed \(c{\gt}0\), interpret a graph on \(\mathrm{Fin}(c)\times \mathrm{Fin}(n)\) with \(E((i,x),(j,y))\) iff \(i=j\) and \(E(x,y)\) in the source. This defines the union of \(c\) disjoint copies and a reduction of bipartiteness to itself.
The interpreted edges have the stated semantics. For every source graph, the disjoint union is bipartite exactly when the source is. The construction applies to directed graphs and permits loops; it is a semantic reduction example, with no hardness claim.
Extend a source coloring by ignoring tags. In the reverse direction, restrict a coloring to the copy with tag \(0\), which exists since \(c{\gt}0\).
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.
Evaluate the defining relation formulas to obtain a decidable target structure on the same universe, with constants copied from their designated source constants. The binary map decodes, interprets, and re-encodes, sending every malformed string to \([]\). A separate arithmetic generator writes the header, all target relation truth tables, and the designated one-hot constant blocks at a supplied cardinality, without validating the source string.
Computable interpretation represents the original structure map exactly. Both generators return \(\mathrm{enc}(I(\mathcal A))\) on \(\mathrm{enc}(\mathcal A)\). The raw generator has length \(\ell _W(n)\), including all target relation and constant blocks. On arbitrary input \(x\), the validated map’s length is at most \(\ell _W(|x|)\); malformed input produces \([]\). For every target query \(Q\),
Formula truth-table correctness identifies the relation blocks; arithmetic constant reads recover the designated one-hot blocks. Sum their exact lengths with the header. The unary prefix gives \(n\le |x|\), and encoded length is monotone. Split on decoding for language membership; the empty string is never a valid structure encoding.
Every fixed universe-preserving FO interpretation has its encoded map in \(\mathsf{FP}\). More generally, its arithmetic generator is polynomial-time when supplied a polynomial-time string and a polynomial-time unary cardinality.
Generate each target relation table by the formula table theorem, and each constant block by a bounded scan of source bits. Concatenate the fixed list of blocks and the header. Parse the source cardinality and guard this polynomial-time generator with encoding validity, returning \([]\) on failure. Correctness identifies this function with the decoder-based map.
If \(Q_1 \le _{\mathsf{FO}} Q_2\) under the existing universe-preserving API, then the language of \(Q_1\) polynomial-time many-one reduces to the language of \(Q_2\). The legacy quantifier-free restriction has the same consequence. Machine \(\mathsf{P}\) and \(\mathsf{NP}\) membership therefore transport backward along these structural reductions. The tagged tuple encoding bridge remains separate.
Use the interpretation’s encoded map as the reduction function. The structural carrying equivalence and exact language pullback give correctness on every string. Apply the existing machine-class closure theorems.
Suppose \(Q_2\) is existential-SO definable, \(\operatorname {queryLanguage}(Q_1)\) is NP-hard, and \(Q_1\le _{\mathsf{FO}}Q_2\) under the universe-preserving API. Then \(\operatorname {queryLanguage}(Q_2)\) is NP-complete for the existing machine definitions. The source hardness is an explicit hypothesis.
Fagin’s upper direction gives target membership in NP. The encoded reduction transports the supplied source hardness.
Evaluate the interpretation on decidable structures. An arithmetic generator extracts tags by division, coordinates by base expansion, selects a defining relation formula from the fixed finite tag cases, and packs source-constant tuples. The binary map decodes, interprets, and re-encodes; malformed inputs map to \([]\).
Arithmetic generation equals the encoding of the existing interpreted structure exactly. Its length is \(\ell _W(t n^d)\), including every relation and constant block. The binary map has the asserted valid-input behavior and rejects malformed encodings. Its polynomial-time machine bound remains open.
The product equivalence uses quotient and remainder; the tuple equivalence uses the same little-endian positional numeral as the encoder. These identities identify each generated relation and constant block.
14.7 Capturing complexity classes
Append a designated binary relation for canonical strict order on \(\mathrm{Fin}(n)\), retaining the input relations and constants. Order atoms use the existing first-order syntax. Satisfaction on canonical expansions can depend on the labeling of the original structure. Derived successor and endpoint formulas remain planned.
On \(\{ 0,\ldots ,n-1\} \), let \(\mathrm{BIT}(x,i)\) hold when bit \(i\) of \(x\) is one (counting from zero), \(\mathrm{ADD}(x,y,z)\) when \(x+y=z\) in \(\mathbb N\), and \(\mathrm{MUL}(x,y,z)\) when \(xy=z\) in \(\mathbb N\). The latter two are ternary relations restricted to the universe, without modular wraparound. Extend each input vocabulary by the selected predicates with these fixed semantics. Definability means agreement with a single sentence on every canonical expansion. The BIT profile adds only BIT; the arithmetic profile adds only ADD and MUL. These conventions follow Schweikardt and Schwentick, A note on the expressive power of linear orders, Section 2 (2011), https://lmcs.episciences.org/1008/pdf.
Forgetting the added symbols recovers the original structure. Translating an input formula into the extended vocabulary preserves satisfaction under every free-variable assignment, so FO definitions remain definitions after expansion. Each numerical atom holds exactly when its evaluated arguments satisfy the designated natural-number relation. The Boolean expansion agrees with the propositional expansion.
Split relation indices into input and numerical symbols. For input formulas, apply satisfaction transport through the interpretation that forgets the numerical symbols. Numerical atoms and Boolean expansion follow directly from their definitions.
Over finite initial segments, with the same additional input relations, \(\mathsf{FO}[\mathrm{BIT}]=\mathsf{FO}[\mathrm{ADD},\mathrm{MUL}]\). Each direction requires formulas independent of the universe size, together with a satisfaction-preserving translation. Canonical order is itself definable from BIT. This is a planned formalization of the equivalences in Schweikardt and Schwentick, A note on the expressive power of linear orders, Theorem 1.1 (2011), https://lmcs.episciences.org/1008/pdf.
Let \(\varphi \) be a second-order sentence in \(\exists \mathsf{SO}\) form that defines \(Q\). Then the language of \(Q\) is in the existing machine class \(\mathsf{NP}\), with every malformed structure encoding rejected.
The binary checker is polynomial-time, accepts some certificate exactly on the query language, and accepts only certificates of length at most \(p(|x|)=\sum _j|x|^{k_j}\). Apply the proved guess-and-verify NTM construction to this verifier and bound. This formalizes Immerman, Section 7.1, Proposition 7.6; the converse tableau construction is a separate theorem.
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.
At a fixed universe size \(n\), an input layout assigns wires to relation-table entries and one-hot constant blocks. There is a fixed finite numbering of all these sites, independent of the structure’s relation and constant values. Compile a formula under an assignment of its free variables as follows: relation atoms select a table entry by testing all argument values; equality tests whether both terms select the same value; negation uses De Morgan duality; Boolean connectives remain gates; and quantifiers become unbounded gates over the \(n\) possible values. The result is an AC0Formula.
Define \(P_\varphi \in \mathbb N[X]\) by \(P_{R(\bar t)}=1+(a+2)X^a\) for an \(a\)-ary relation, \(P_{t=u}=1+3X\), \(P_{\neg \varphi }=P_\varphi \), \(P_{\varphi \wedge \psi }=P_{\varphi \vee \psi }=1+P_\varphi +P_\psi \), and \(P_{Qx\, \varphi }=1+XP_\varphi \) for \(Q\in \{ \exists ,\forall \} \). This is the finite expansion used in Immerman, Section 5.4, Theorem 5.22.
The table layout has exactly \(\sum _i n^{a_i}+cn\) inputs, where \(a_i\) are relation arities and \(c\) is the number of constants. Every decidable structure supplies a valid table input. On any represented structure, the compiled formula evaluates to true exactly when the source formula is satisfied under the supplied assignment. Its tree size is exactly \(P_\varphi (n)\) and its depth is at most \(|\varphi |+1\), uniformly over layouts and assignments.
The numbering of input sites is chosen noncomputably; compilation from a given layout is computable. These statements concern fixed-size table inputs, not yet the library’s bit-string encoding with its unary prefix or a circuit family.
A constant selector reads its one-hot bit. In a relation atom exactly the tuple of argument values passes all selectors, so its input relation bit determines the answer. Induct on the source formula; finite conjunction and disjunction realize the quantifiers. Sum the child sizes for the polynomial identity and take their maximum depths plus one for each gate. De Morgan negation preserves both tree size and depth.
For \(N{\gt}0\), every unbounded formula \(F\) on \(N\) inputs has an equivalent single-output circuit over the unbounded AND/OR basis. Its size is exactly \(\operatorname {size}(F)\) and its depth is at most \(\operatorname {depth}(F)+1\). The statement includes constant leaves, signed literals, and empty connectives.
Realize each constant or literal by one output gate. Induct on formula size. For a nonempty connective, pack the child circuits in parallel, whose size is the sum of child sizes and whose depth is their maximum, then compose with one connective gate. Empty conjunctions and disjunctions use nullary AND and OR gates. The extra depth layer comes from counting leaf output gates.
Fix a universe size \(n\), a layout on \(N{\gt}0\) input wires, a formula \(\varphi \), and a free-variable assignment. There is a single circuit computing the expansion on every input, with size exactly \(P_\varphi (n)\) and depth at most \(|\varphi |+2\). On every represented structure it computes satisfaction of \(\varphi \) under that assignment. The circuit is selected from the formula, layout, and assignment alone, independently of the input table contents.
Apply the formula realization theorem to the finite quantifier expansion, then combine the exact size, depth, and satisfaction theorems. No claim about invalid encodings or uniform circuit generation is needed for this statement.
Assign each relation and constant-table wire its actual bit position in the full structure encoding. Present an encoded structure as a Boolean input vector of length \(\ell _V(n)\). This layout is computable.
The input vector’s list is exactly the original encoding. Every encoded structure represents its relation and constant tables under this layout. Therefore the expansion computes satisfaction on the actual encoding, including for open formulas. At each universe size there is one circuit on \(\ell _V(n)\) inputs computing the sentence expansion on every input, of size \(P_\varphi (n)\) and depth at most \(|\varphi |+2\). The following validator supplies rejection of malformed inputs.
Apply correctness of bit positions to obtain the representation predicate, then instantiate expansion correctness and circuit realization.
At length \(\ell _V(n)\), conjoin the test \(n\ge 2\), a signed-literal test for the unary header \(1^n0\), and a one-hot test for every constant block. A one-hot test is a disjunction over the \(n\) possible values, each given by a conjunction of \(n\) signed literals. Relation-table bits are unrestricted. Write \(E_V(X)=X+4+c(1+X(1+X))\) for its size polynomial, with \(c\) constant symbols. The validated expansion conjoins this validator with the sentence expansion; its size polynomial is \(V_\varphi =1+E_V+P_\varphi \).
The validator accepts precisely the encoder’s image at length \(\ell _V(n)\). It has size exactly \(E_V(n)\) and depth at most three. The validated sentence expansion accepts exactly the corresponding query language, including on malformed inputs, with size \(V_\varphi (n)\) and depth at most \(|\varphi |+4\). There is an actual circuit recognizing this language at the chosen length, with size \(V_\varphi (n)\) and depth at most \(|\varphi |+5\).
From passing tests, read every relation bit and the selected value in every constant block. Encoding reconstruction gives a structure with exactly the input encoding. Conversely, encoded structures pass all tests. Strict increase of encoded length identifies the universe size, allowing expansion correctness to compute the query. Sum the test sizes and bound their depths, then apply formula-to-circuit realization.
For each binary input length \(N\), define \(\mathrm{queryFamily}(Q)_N(x)=1\) exactly when the list of bits in \(x\) belongs to \(\mathrm{queryLanguage}(Q)\). This noncomputable characteristic family is defined for every query, including queries that are not decidable.
Every first-order definable query has its characteristic family in the existing nonuniform class \(\mathsf{AC^0}\). For a defining sentence \(\varphi \), at every positive input length \(N\) there is a circuit of size at most \(V_\varphi (N)\) and depth at most \(|\varphi |+5\). Its output agrees with the query family on every bit string. The family rejects the empty input.
The encoding length is strictly increasing in the universe size, so at most one size \(n\) has encodings of length \(N\). At that length, use the validated sentence circuit. At every other positive length use a constant-false circuit, and set the family’s empty-input output to false. Since \(n{\lt}N\) and \(V_\varphi \) has natural coefficients, \(V_\varphi (n)\le V_\varphi (N)\). Select the finite circuit witnesses to obtain a polynomial-size, constant-depth family. A definability witness identifies its language with the language of the query.
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.