{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R36",
  "content_hash": null,
  "slug": "asser-attempt-naive-sentence-negation",
  "type": "attempt",
  "title": "Sentence negation does not complement the spectrum",
  "summary": "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}.",
  "relevance": "For Asser's complement problem for first-order spectra, record asser-attempt-naive-sentence-negation (“Sentence negation does not complement the spectrum”) documents a concrete method, search boundary, or failed route. The record states: 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}.",
  "relevance_source": "recorded",
  "body": "Take\n\\[\n\\varphi=(\\exists x\\,P(x))\\wedge(\\exists y\\,\\neg P(y)).\n\\]\nIt has a model exactly at sizes \\(n\\ge2\\), since the interpretation of \\(P\\) must be a nonempty proper subset. Its logical negation says that \\(P\\) is empty or contains the whole universe. At every positive size, one of those interpretations exists. Hence\n\\[\n\\operatorname{Spec}(\\varphi)=\\{n:n\\ge2\\},\\qquad\n\\operatorname{Spec}(\\neg\\varphi)=\\mathbb Z_{>0},\n\\]\nwhile\n\\[\n\\mathbb Z_{>0}\\setminus\\operatorname{Spec}(\\varphi)=\\{1\\}.\n\\]\nThe failed method is the direct replacement \\(\\varphi\\mapsto\\neg\\varphi\\). A spectrum existentially projects over all interpretations of the relation symbols at each size. Formula negation changes which structures satisfy the sentence and leaves that existential projection in place. Any complement construction must control existence across all structures of a cardinality.",
  "status": "failed",
  "evidence_grade": "self_reported",
  "scope": {
    "kind": "bounded",
    "statement": "the proposed rule Spec(not phi) equals the complement of Spec(phi), tested on one rank-one sentence over one unary predicate",
    "bounds": {
      "quantifier_rank": {
        "min": 1,
        "max": 1
      },
      "unary_predicates": {
        "min": 1,
        "max": 1
      },
      "counterexamples": {
        "min": 1,
        "max": 1
      }
    },
    "exhaustive": false
  },
  "reproduction": {
    "schema": "theoremdb-reproduction-v1",
    "readiness": "source_only",
    "kind": "attempt",
    "citation": {
      "url": "https://doi.org/10.23638/LMCS-14(2:4)2018",
      "locator": "TheoremDB packet object asser-attempt-naive-sentence-negation, displayed construction and three spectrum equations, also asserted by tools/first_order_spectra_complement_replay.py"
    },
    "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-attempt-naive-sentence-negation, displayed construction and three spectrum equations, also asserted by tools/first_order_spectra_complement_replay.py"
  },
  "relations": [
    {
      "slug": "R33",
      "title": "Exact bounded census for monadic spectra",
      "object_type": "artifact",
      "relation": "tests",
      "direction": "incoming"
    },
    {
      "slug": "R38",
      "title": "Asser's complement problem remains open",
      "object_type": "claim",
      "relation": "constrains",
      "direction": "outgoing"
    },
    {
      "slug": "first-order-spectra-complement-closure",
      "title": "first order spectra complement closure",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}