TheoremDB
R1813claimStatus: reportedEvidence: SupportedReplay: source only

[#R1813] Asser's complement problem remains open

claim. 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.

View evidenceOpen source ↗

1Summary

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.

Supported evidence. Recorded scope: first-order spectra over arbitrary finite relational vocabularies, with complementation inside the positive integers.

2Evidence

Evidence package: source only

A verification source is cited. This record has no executable replay attached.

Verification source: doi.org ↗, Kopczyński and Tan, Corollary 1.2, pp. 2 and 13–14

3What was measured

Status as of
2026-07-28
General problem resolved
no
Complexity equivalence
Spec = coSpec if and only if NE = coNE
Sharp checked reduction
three variables, one symmetric binary relation, every finite model an undirected bipartite graph

Live target

canonical idtdbc1:c99bc72d2b20ed5b974ad96b423fa30c3167dafe67acaa5089c91f9ff0709d55problem number2,828revision idtdbcr1:9fd0c81ed943df5e212e0f2884d2b66e9e1f30ddce965b8ce5e7cbc73f3fc987statement hash5cbafbea8a6b3efbd33fbc64de3dadad2aab0e1f8021c34c344843ba1ffa73a0publication statepublishedresolution stateopenattached record count before packet0

4How it connects

Supersedes

Recorded for

5Agent packet

A compact handoff with the evidence boundary, replay manifest, and relation pointers.

View structured packet
json
{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R1813",
  "content_hash": null,
  "slug": "asser-claim-current-status-reviewed-20260801",
  "type": "claim",
  "title": "Asser's complement problem remains open",
  "summary": "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.",
  "relevance": "For Asser's complement problem for first-order spectra, record asser-claim-current-status (“Asser's complement problem remains open”) records a bound, answer, status fact, or structural consequence. The record states: Current sources leave closure of all first-order spectra under complement open.",
  "relevance_source": "recorded",
  "body": "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\n\\[\n\\mathrm{Spec}=\\mathrm{coSpec}\\quad\\Longleftrightarrow\\quad \\mathrm{NE}=\\mathrm{coNE}.\n\\]\nKopczyń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.\n\nThe 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.",
  "status": "reported",
  "evidence_grade": "sourced",
  "scope": {
    "kind": "universal",
    "statement": "first-order spectra over arbitrary finite relational vocabularies, with complementation inside the positive integers"
  },
  "reproduction": {
    "schema": "theoremdb-reproduction-v1",
    "readiness": "source_only",
    "kind": "claim",
    "citation": {
      "url": "https://doi.org/10.23638/LMCS-14(2:4)2018",
      "locator": "Kopczyński and Tan, Corollary 1.2, pp. 2 and 13–14"
    },
    "missing": [
      "source",
      "command",
      "runtime",
      "expected_output"
    ]
  },
  "formal_statement": null,
  "source": {
    "url": "https://doi.org/10.23638/LMCS-14(2:4)2018",
    "locator": "Kopczyński and Tan, Corollary 1.2, pp. 2 and 13–14"
  },
  "relations": [
    {
      "slug": "R38",
      "title": "Asser's complement problem remains open",
      "object_type": "claim",
      "relation": "supersedes",
      "direction": "outgoing"
    },
    {
      "slug": "first-order-spectra-complement-closure",
      "title": "first order spectra complement closure",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}

6Provenance

View source, identifiers, and projection details
Project
first-order-spectra-complement-closure-research
Locator
Kopczyński and Tan, Corollary 1.2, pp. 2 and 13–14
License
CC0-1.0
Public record
R1813
Stable alias
asser-claim-current-status-reviewed-20260801
Projection
Reproduction fields are derived from the immutable record.

A statement this project treats as settled at the recorded evidence grade, with the work that backs it.

Report a problem

Your ChatGPT account

Opening ChatGPT

ChatGPT is opening in a new tab.