Finite Spectrum Problem

Finite Spectrum Problem

Definitions and mathematical statement

For a first-order sentence $\varphi$ in a finite vocabulary, define its finite spectrum by \[ \operatorname{Spec}(\varphi)=\{n\in{\mathbb{Z}}_{>0}:\exists\text{ a structure }\mathcal A, \ |\mathcal A|=n,\ \mathcal A\models\varphi\}. \] The question asks whether for every such sentence there is another first-order sentence $\psi$ with $\operatorname{Spec}(\psi)={\mathbb{Z}}_{>0}\setminus\operatorname{Spec}(\varphi)$. The new sentence may use a different finite vocabulary. This is complementation of the set of possible cardinalities; simply negating $\varphi$ does not do this, because structures of a fixed size can satisfy $\varphi$ and $\neg\varphi$ simultaneously in different interpretations.

Formulation and concept references: [S1].

Short English statement

Is the set of finite sizes excluded by a first-order sentence always exactly the set of finite sizes admitted by some other sentence?

Research attempt

Scope, source correction, and process.

This attempt by GPT-6 Astra Ultra was prepared on 27 September 2026. The inherited source entry is preserved, but its URL is the survey Fifty Years of the Spectrum Problem: Survey and New Results by Durand, Jones, Makowsky and More, not the title written in that entry. Its Theorem 5.5 and Corollary 5.6 describe the connection with nondeterministic exponential time. That connection is used at its stated strength.

We prove complement closure for a purely unary relational subclass, construct contrasting parity spectra using a binary relation, and expose the quantifier change that prevents direct negation from solving the problem. The first missing step is a uniform logical construction for the excluded cardinalities of unrestricted finite-vocabulary sentences.

Two existential statements need not be complementary.

For a fixed positive integer $n$, membership in the spectrum means \[ \exists\mathcal A\ (|\mathcal A|=n\ \wedge\ \mathcal A\models\varphi). \] Its negation is \[ \forall\mathcal A\ (|\mathcal A|=n\ \Longrightarrow\ \mathcal A\not\models\varphi). \tag{272.1} \] In contrast, membership in $\operatorname{Spec}(\neg\varphi)$ only asserts the existence of one $n$-element structure violating $\varphi$.

For example, in a vocabulary with one unary predicate $P$, take $\varphi=\forall x\,P(x)$. At every positive cardinality interpret $P$ as the whole universe to satisfy $\varphi$, and interpret $P$ as empty to satisfy $\neg\varphi$. Both spectra are all positive integers. The desired complement of the first is empty, realized instead by an inconsistent sentence.

The problem allows a new vocabulary, so this countertest does not refute complement closure. It only shows why replacing $\varphi$ by its syntactic negation is the wrong construction.

Finite spectra and cofinite spectra have complements.

For $a\ge1$, a sentence specifying exactly $a$ elements is \[ \exists x_1\cdots x_a\left( \bigwedge_{i<j}x_i\ne x_j\ \wedge\ \forall y\bigvee_{i=1}^a y=x_i\right). \] Finite disjunctions realize arbitrary finite sets of positive cardinalities. Negating such a cardinality sentence realizes its cofinite complement, because the truth of the sentence is independent of any freely interpreted relation.

This special use of negation is valid precisely because all structures of a fixed size agree on the pure cardinality assertion. The preceding unary-predicate example lacked that property.

A complete unary relational subcase.

Suppose the vocabulary consists of $s$ unary predicates and equality, with no function symbols or named constants. There are $2^s$ possible unary types, according to which predicates an element satisfies. Let $r\ge1$ be at least the quantifier rank of $\varphi$.

The truth of $\varphi$ depends only on the type counts truncated at $r$: \[ c_\tau\longmapsto \min(c_\tau,r). \tag{272.2} \] Here a value $r$ means at least $r$, not exactly $r$. One proof uses the usual $r$-round back-and-forth argument. Maintain a type-preserving bijection between the elements selected so far. If the next selected element was already selected, use its partner. Otherwise, when its type has fewer than $r$ elements, the corresponding type has exactly the same size in both structures; when it has at least $r$, fewer than $r$ rounds have been played and a fresh matching element remains available.

The resulting correspondence preserves equality and every unary atomic formula. Induction on the remaining quantifiers, with Boolean combinations handled directly, shows that the two structures satisfy the same sentences of quantifier rank at most $r$. This proves $272.2$ without assuming a bound on the total universe size.

Now enumerate all vectors $t=(t_\tau)_\tau\in\{0,\ldots,r\}^{2^s}$, and evaluate $\varphi$ on a canonical structure having exactly $t_\tau$ elements of each type. If no coordinate equals $r$, this vector represents one possible cardinality $T=\sum_\tau t_\tau$. If at least one coordinate equals $r$, it represents every cardinality $n\ge T$: add the $n-T$ extra elements to one saturated type. Conversely every count vector with this truncation has cardinality at least $T$.

The empty universe is discarded because the spectrum is defined only on positive integers. Thus the spectrum is a finite union of singleton sets and tails. It is finite or cofinite, and the preceding cardinality formulas explicitly realize its complement. The procedure may be expensive as a function of the sentence; the problem asks for existence of a sentence, not a polynomial bound on the transformation.

Binary relations already escape the unary description.

Use a binary relation $R$ to describe the graph of a fixed-point-free involution: every element has exactly one $R$-successor, $R(x,y)$ implies $R(y,x)$, and $R(x,x)$ never holds. Its finite models are partitions into pairs, so its spectrum is exactly the positive even integers. Neither this spectrum nor its complement is finite or cofinite.

The complement is still a spectrum. Require instead an involution with exactly one fixed point, all other elements belonging to two-cycles. The finite universe then has size one plus an even number, and every positive odd size occurs. These constructions verify both directions, including the one-element case.

The example does not make the general problem easier: it shows that the unary finite/cofinite theorem cannot simply be extended to all relational vocabularies. Binary relations can organize unbounded global combinatorial structure even when the sentence has fixed length.

The time bound attached to binary cardinality input.

For a fixed relational sentence $\varphi$, membership of $n$ in its spectrum is decidable by finite search. Guess the interpretations of its relations on the universe $[n]$, then evaluate the fixed sentence. If the largest relation arity is $a$, the guessed relation tables have $O(n^a)$ bits. Brute-force evaluation of a fixed formula takes another fixed polynomial in $n$.

With $\ell=\lceil\log_2(n+1)\rceil$, this nondeterministic running time is $2^{O(\ell)}$. The constant in the exponent may depend on $\varphi$, which is fixed for its spectrum. Function symbols can be replaced by graph relations plus first-order totality and uniqueness axioms, preserving cardinalities; constants can similarly be encoded. Thus the same conclusion covers the full finite-vocabulary setting.

Write \[ \mathrm{NE}=\bigcup_{c\ge1}\operatorname{NTIME}(2^{c\ell}). \] The established converse coding theorem of Jones--Selman, stated in [S1], identifies spectra of binary-encoded positive integers with NE sets under the conventional integer-language encoding. Consequently complement closure of spectra is equivalent to $\mathrm{NE}=\mathrm{coNE}$.

This is NE, with a linear exponent in the input length, not an arbitrary change to $\operatorname{NTIME}(2^{\ell^c})$. The converse coding theorem is an external descriptive-complexity input; the elementary guessing argument above proves only the easy direction.

Why finite search does not provide the required sentence.

Enumerating all interpretations at size $n$ decides both membership and nonmembership, but the deterministic search can inspect $2^{n^{O(1)}}$ structures. Relative to the binary length $\ell$, this is doubly exponential rather than the NE certificate bound. Decidability of a set of integers is much weaker than being a first-order spectrum.

Likewise a finite model search for each excluded size does not create a witness structure for all excluded sizes through one fixed first-order sentence. Such a sentence cannot contain a separate arbitrary truth table for infinitely many cardinalities. The universal statement $272.1$ must be represented by an existential finite-model condition with fixed syntax, and that is precisely the missing complement construction.

Allowing a different finite vocabulary provides flexibility for this encoding, but does not permit infinitely many relation symbols or a formula whose length depends on the tested cardinality.

Verification and outcome.

Finite checks enumerate unary type-count vectors and verify the singleton-or-tail cardinality description. They also enumerate small involutions to check the even and odd constructions, and test the direct-negation counterexample at every small positive size. The quantifier-rank argument supplies the unbounded unary result; finite tests do not establish general complement closure.

UNRESOLVED. Complement closure is proved for purely unary relational sentences and explicit parity spectra. The binary-input complexity calculation exposes the exact NE complement question behind the unrestricted assertion. No general sentence construction or non-spectrum complement is produced.

Sources

• S1 A spectrum hierarchy. Submitted scholarly source, accessed 2026-08-31. https://arxiv.org/abs/0907.5495. Formulation source.