{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R39",
  "content_hash": null,
  "slug": "asser-claim-monadic-rank-classification",
  "type": "claim",
  "title": "Every fixed monadic vocabulary needs at most one extra rank",
  "summary": "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.",
  "relevance": "For Asser's complement problem for first-order spectra, record asser-claim-monadic-rank-classification (“Every fixed monadic vocabulary needs at most one extra rank”) records a bound, answer, status fact, or structural consequence. The record states: For r unary predicates and rank q, the spectra have an exact generator classification.",
  "relevance_source": "recorded",
  "body": "Fix integers \\(r,q\\ge1\\). The \\(r\\) unary predicates determine \\(t=2^r\\) Boolean 1-types, or colors. Write \\(n_i\\) for the size of color class \\(i\\). Two finite structures agree on every sentence of quantifier rank at most \\(q\\) exactly when the vectors\n\\[\n(\\min(n_1,q),\\ldots,\\min(n_t,q))\n\\]\nagree. In the \\(q\\)-round Ehrenfeucht-Fraïssé game, the duplicator matches elements within corresponding colors. A disagreement below \\(q\\) is exposed by selecting all elements in the smaller class and one more in the larger class. De Rijke states this standard monadic equivalence criterion as Theorem 3.10. The generator collapse and counts below are derived here.\n\nEvery truncated vector is definable at rank \\(q\\). A coordinate \\(i<q\\) is expressed by requiring exactly \\(i\\) elements of that color. The coordinate \\(q\\) requires at least \\(q\\). Conjunction defines one vector, and disjunction selects any collection of vectors.\n\nSet \\(A=t(q-1)\\). A vector with every coordinate below \\(q\\) contributes one exact cardinality, and every singleton size from \\(1\\) through \\(A\\) occurs this way. A vector with at least one coordinate equal to \\(q\\) contributes a tail \\(\\{n:n\\ge s\\}\\), where \\(s\\) is the sum of its coordinates. Every tail start \\(s\\) from \\(q\\) through \\(tq\\) occurs. The rank-\\(q\\) spectra are therefore exactly the unions generated by\n\\[\n\\{n\\}\\quad(1\\le n\\le A),\n\\qquad\n\\{n:n\\ge s\\}\\quad(q\\le s\\le tq).\n\\]\n\nThere are \\(2^A\\) finite spectra. To count the cofinite spectra, use the largest missing positive integer \\(L\\), with \\(L=0\\) for the full set. The cases \\(0\\le L\\le A\\) contribute \\(2^A\\) spectra in total. Each of the \\(t-1\\) values \\(A+1\\le L\\le tq-1\\) permits an arbitrary subset of \\(\\{1,\\ldots,A\\}\\) and forces every size from \\(A+1\\) through \\(L\\) to be absent. Thus there are \\(t2^A\\) cofinite spectra and \\((t+1)2^A\\) spectra altogether.\n\nThe complement of a finite rank-\\(q\\) spectrum is an allowed cofinite spectrum. The complement of a cofinite rank-\\(q\\) spectrum is finite and has no element above \\(tq-1\\). At rank \\(q+1\\), exact singleton generators extend through \\(tq\\), so every such complement occurs. Exactly \\((t-1)2^A\\) spectra lack a same-rank complement. The bound is sharp: the rank-\\(q\\) spectrum\n\\[\n\\{1,\\ldots,A\\}\\cup\\{n:n\\ge tq\\}\n\\]\nhas complement \\(\\{A+1,\\ldots,tq-1\\}\\), which first becomes available at rank \\(q+1\\). For one unary predicate this interval is the singleton \\(\\{2q-1\\}\\).\n\nThis argument covers each fixed finite unary vocabulary. The unrestricted problem allows relations of higher arity and remains open.",
  "status": "supported",
  "evidence_grade": "self_reported",
  "scope": {
    "kind": "family",
    "statement": "all first-order sentences of quantifier rank at most q over equality and any fixed positive finite number r of unary predicates",
    "family": "monadic first-order logic stratified by vocabulary size and quantifier rank"
  },
  "reproduction": {
    "schema": "theoremdb-reproduction-v1",
    "readiness": "source_only",
    "kind": "claim",
    "citation": {
      "url": "https://doi.org/10.23638/LMCS-14(2:4)2018",
      "locator": "TheoremDB packet object asser-claim-monadic-rank-classification, proof paragraphs 1 through 6, checked by asser-artifact-monadic-spectrum-census"
    },
    "missing": [
      "source",
      "command",
      "runtime",
      "expected_output"
    ]
  },
  "formal_statement": null,
  "source": {
    "url": "https://doi.org/10.23638/LMCS-14(2:4)2018",
    "locator": "TheoremDB packet object asser-claim-monadic-rank-classification, proof paragraphs 1 through 6, checked by asser-artifact-monadic-spectrum-census"
  },
  "relations": [
    {
      "slug": "R38",
      "title": "Asser's complement problem remains open",
      "object_type": "claim",
      "relation": "informs",
      "direction": "outgoing"
    },
    {
      "slug": "R33",
      "title": "Exact bounded census for monadic spectra",
      "object_type": "artifact",
      "relation": "evidences",
      "direction": "incoming"
    },
    {
      "slug": "first-order-spectra-complement-closure",
      "title": "first order spectra complement closure",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}