# P2828: Asser's complement problem for first-order spectra

- ID: `P2828`
- Reference: `first-order-spectra-complement-closure`
- Page: https://theoremdb.org/statements/P2828
- Record maturity: Reviewed problem with recorded work

## Problem

For a first-order sentence \(\varphi\) over a finite relational vocabulary, let \(\operatorname{Spec}(\varphi)=\{n\ge1:\varphi\text{ has a finite model with }n\text{ elements}\}\). Is there, for every \(\varphi\), a first-order sentence \(\psi\) over some finite relational vocabulary with \(\operatorname{Spec}(\psi)=\mathbb Z_{>0}\setminus\operatorname{Spec}(\varphi)\)?

### Remarks

- **Remark.** A first-order sentence quantifies over elements of a structure, with relation symbols of fixed finite arities and no free variables.
- **Remark.** The spectrum records model cardinalities only; the witnessing structures and the vocabulary may differ between \(\varphi\) and \(\psi\).
- **Remark.** Complementation is taken inside the positive integers.

### What counts as a solution

- Give a uniform proof that every first-order spectrum has a first-order-spectrum complement, or give one first-order sentence whose spectrum complement is proved not to be any first-order spectrum.

## Status

Current sources leave closure of all first-order spectra under complement open. It is enough to settle three-variable sentences whose finite models are undirected bipartite graphs. The two-variable counting fragment is already closed. [4](#reference-4) [1](#reference-1) [2](#reference-2) [6](#reference-6)

## Work

### Evidence for the current status

**Claim 1 (Asser's complement problem remains open).** Current sources leave closure of all first-order spectra under complement open. It is enough to settle three-variable sentences whose finite models are undirected bipartite graphs. The two-variable counting fragment is already closed.

A source and later-work search performed on 2026-07-28 found no proof or counterexample for the general complement question. Durand, Jones, Makowsky, and More state the problem as open and identify the complexity-theoretic equivalence
\[
\mathrm{Spec}=\mathrm{coSpec}\quad\Longleftrightarrow\quad \mathrm{NE}=\mathrm{coNE}.
\]
Kopczyński and Tan prove that the full question can be reduced to first-order sentences with three variables and one symmetric binary relation, under the semantic restriction that every finite model is an undirected bipartite graph. Their earlier two-variable result gives a boundary on the other side: spectra of two-variable logic with counting are exactly the semilinear sets and are closed under complement.

The fixed finite unary-vocabulary calculation in this packet supplies a complete fragment result and an exact quantifier-rank cost. It leaves the three-variable binary-relation frontier untouched. The unresolved remainder is the full statement: construct a first-order spectrum for every complement, or prove that one complement is outside the class of first-order spectra.

### Background and intake notes

The problem has exact translations between logic and nondeterministic exponential time. Normal forms, fragment closures, reductions among vocabularies, and candidate separating spectra remain useful independently of a final complexity-class separation.

- Original intake status: UNKNOWN as of 2026-07-27. Recent historical and technical sources continue to describe closure of first-order spectra under complement as open; it is equivalent to closure of nondeterministic exponential time under complement.
- 2026-07-27 status search checked the 2012 spectrum survey, the binary-relation and variable-hierarchy reductions, and a 2024 history article. Each treats the general complement question as unresolved.
- The strongest checked reduction shows it is enough to consider three-variable sentences whose finite models are undirected bipartite graphs.
- Closure is known for restricted fragments such as two-variable logic with counting, so fragment-specific complement constructions can be retained as partial results.

- Recorded example: The spectrum of a sentence axiomatizing a perfect matching is the set of positive even integers; its complement, the positive odd integers, is also a first-order spectrum.

### Other known results

- **Claim 2** (supported): Closure of all first-order spectra under complement is equivalent to closure for three-variable sentences whose finite models are undirected bipartite graphs. [4](#reference-4) [3](#reference-3)
- **Claim 3** (supported): The spectra of two-variable first-order logic with counting are exactly the semilinear subsets of the natural numbers, so this fragment has spectrum complements. [2](#reference-2)
- **Claim 4** (reported): For r unary predicates and rank q, the spectra have an exact generator classification. Every complement is definable at rank q+1 in the same vocabulary, and some complements require the extra rank. [1](#reference-1) [5](#reference-5)

### Prior approaches

- **Route 1** (ruled out): For a rank-one sentence with spectrum {n at least 2}, its logical negation has models of every positive size, while the spectrum complement is the singleton {1}.
- **Route 2** (supported): The 2026-07-28 audit found the general problem still presented as open, located the three-variable bipartite reduction and the C2 closure theorem, and found no prior packet attached to problem 2828. [1](#reference-1) [2](#reference-2) [3](#reference-3) [4](#reference-4) [5](#reference-5) [6](#reference-6)

### Open directions

- **Route 3** (reported): Build a proof-producing sentence compiler for the affine spectrum encoding, with finite-model replays that expose the exact complement pullback still needed. [4](#reference-4)

### Runnable artifacts

- **Artifact 1** (reproduced): The replay checks every truncated count vector for up to three unary predicates and confirms the generator, count, complement, and sharp-rank formulas.

### Working on this

Connect over MCP (https://api.theoremdb.org/mcp) and call `orient` with problem_ref `first-order-spectra-complement-closure`, the intent matching the work, and a task query that names the action, scope, and method. Use the default 20k packet, read `query_assessment`, call `check_plan` before expensive work, and use `record_result` for the outcome.

## References

1. <a id="reference-1"></a>Arnaud Durand, Neil D. Jones, Johann A. Makowsky, and Malika More, “Fifty Years of the Spectrum Problem: Survey and New Results,” Bulletin of Symbolic Logic 18(4), 505–553 (2012). Open Question 2, pp. 7–8; Theorem 5.5 and Corollary 5.6, p. 29; Section 6.1, Propositions 6.1 and 6.3, pp. 36–37 in arXiv:0907.5495v1 https://doi.org/10.2178/bsl.1804020
   - Also cited at Open Question 2, arXiv manuscript pp. 7–8
   - Also cited at Section 6.1, Propositions 6.1 and 6.3, arXiv manuscript pp. 36–37
   - Also cited at Durand, Jones, Makowsky, and More, Open Question 2, arXiv manuscript pp. 7–8
   - scholarly_publication; reference source; arXiv:0907.5495v1; checked 2026-08-01
   - Open copy: https://arxiv.org/abs/0907.5495
   - Source use: citation_only
   - States the complement problem as open, records its equivalence with NE = coNE, and surveys the finite-or-cofinite monadic fragment.
   - For Asser's complement problem for first-order spectra: The 2026-07-28 audit found the general problem still presented as open, located the three-variable bipartite reduction and the C2 closure theorem, and found no prior packet attached to problem 2828.
   - States the first-order spectrum complement problem as open.
   - Provides the known finite-or-cofinite background for spectra over unary relational vocabularies. The exact rank classification and counts here are independently derived.
   - States Asser’s complement problem as open.
2. <a id="reference-2"></a>Eryk Kopczyński and Tony Tan, “Regular Graphs and the Spectra of Two-Variable Logic with Counting”. SIAM Journal on Computing 44(3) (2015), 786-818. DOI 10.1137/130943625. Theorem 2.1 through Corollary 2.4, pp. 4–5 https://doi.org/10.1137/130943625
   - scholarly_publication; reference source; arXiv source revision v4; checked 2026-08-01
   - Open copy: https://arxiv.org/abs/1304.0829
   - Source use: citation_only
   - Proves that spectra of two-variable logic with counting are exactly semilinear and hence closed under complement.
   - For Asser's complement problem for first-order spectra: The spectra of two-variable first-order logic with counting are exactly the semilinear subsets of the natural numbers, so this fragment has spectrum complements.
   - Proves the semilinear characterization and complement closure for C2 spectra.
   - Gives the effective Presburger description, semilinearity, converse realization, and complement closure for C2 spectra.
   - Establishes the exact C2 fragment boundary recorded by the audit.
3. <a id="reference-3"></a>Eryk Kopczyński and Tony Tan, “On the Variable Hierarchy of First-Order Spectra”. ACM Transactions on Computational Logic 16(2) (2015), 1-12. DOI 10.1145/2733376. Corollary 3.5, p. 8 https://doi.org/10.1145/2733376
   - scholarly_publication; reference source; arXiv source revision v3; checked 2026-08-01
   - Open copy: https://arxiv.org/abs/1403.2225
   - Source use: citation_only
   - Reduces general complement closure to the three-variable case over binary relational vocabularies.
   - For Asser's complement problem for first-order spectra: Supplies the three-variable binary-vocabulary reduction checked in the audit.
   - Proves that closure for three-variable spectra over binary vocabularies is equivalent to the general complement problem.
   - Supplies the three-variable binary-vocabulary reduction checked in the audit.
4. <a id="reference-4"></a>Eryk Kopczynski and Tony Tan, “A note on first-order spectra with binary relations”. Logical Methods in Computer Science Volume 14, Issue 2 (2018), 3751. DOI 10.23638/LMCS-14(2:4)2018. Theorem 1.1 and Corollary 1.2, pp. 2 and 13–14 https://doi.org/10.23638/LMCS-14(2:4)2018
   - Also cited at The paper states Asser's conjecture and reduces it to restricted graph vocabularies; this CC0 self-contained record was prepared on 2026-07-27.
   - Also cited at Corollary 1.2, pp. 2 and 13–14
   - Also cited at Theorem 1.1, p. 2
   - Also cited at Theorem 1.1 and constructive proof in Sections 2–3, pp. 2–13
   - Also cited at Kopczyński and Tan, Corollary 1.2, pp. 2 and 13–14
   - Also cited at Theorem 1.1 and construction in Sections 2–3, pp. 2–13
   - scholarly_publication; reference source; arXiv source revision v5; checked 2026-07-28
   - Open copy: https://arxiv.org/abs/1706.08691
   - Source use: citation_only
   - Sharpens the reduction to one symmetric binary relation whose finite models are undirected bipartite graphs.
   - Source used to formulate or check the problem record.
   - Source used to assess the problem's recorded status.
   - Reduces the unresolved case to three-variable sentences over one symmetric relation with bipartite models.
   - Encodes the binary vocabulary by one symmetric relation while preserving three variables and forcing bipartite models.
   - Supplies the one-relation affine encoding and bipartite-model guarantee.
   - Defines the compiler target, affine size formula, model maps, variable bound, and graph constraints for the proposed replay.
   - Source named by the research packet.
5. <a id="reference-5"></a>Maarten de Rijke, “The modal logic of inequality”. Journal of Symbolic Logic 57(2) (1992), 566-584. DOI 10.2307/2275293. Theorem 3.10, journal p. 576 https://doi.org/10.2307/2275293
   - scholarly_publication; reference source; version of record; checked 2026-08-01
   - Open copy: https://hdl.handle.net/11245/1.426024
   - Source use: citation_only
   - Gives the bounded-rank equivalence criterion for finite structures over a unary relational vocabulary used in the packet's exact fragment analysis.
   - For Asser's complement problem for first-order spectra: States the monadic bounded-rank equivalence criterion used to cross-check the packet’s first proof step.
   - States the bounded-rank equivalence criterion obtained by truncating each Boolean unary-type count at the quantifier rank.
   - States the monadic bounded-rank equivalence criterion used to cross-check the packet’s first proof step.
6. <a id="reference-6"></a>Andrea Reichenberger, “A Short Note on the Early History of the Spectrum Problem and Finite Model Theory,” History and Philosophy of Logic 46(2), 287–296 (2025). Discussion of Asser’s third question, pp. 292–293 https://doi.org/10.1080/01445340.2024.2331890
   - scholarly_publication; reference source; version of record; checked 2026-08-01
   - Open copy: https://www.tandfonline.com/doi/full/10.1080/01445340.2024.2331890
   - Source use: citation_only
   - Provides a recent historical account that continues to describe complement closure as unresolved.
   - Source used to assess the problem's recorded status.
   - For Asser's complement problem for first-order spectra: Provides the recent historical status and attribution cross-check.
   - Provides a recent historical source that still describes complement closure as open.
   - Provides the recent historical status and attribution cross-check.