{
  "id": "oai:papers.qnfo.org:the-excluded-middle-as-a-quantifiable-computational-boundary-translation-overhea",
  "slug": "the-excluded-middle-as-a-quantifiable-computational-boundary-translation-overhea",
  "title": "The Excluded Middle as a Quantifiable Computational Boundary: Translation Overhead, Model-Space Expansion, and Search Cost of Classical Reasoning",
  "authors": [
    "Rowan Brad Quni-Gudzinas"
  ],
  "abstract": "Engineers who build proof assistants, ontology-based query engines, and LLM reasoning pipelines must choose whether their logic admits the law of the excluded middle (LEM), the principle that every proposition φ satisfies φ vee ¬φ, yet no standard overhead budget exists for that choice. This paper makes the classical/constructive boundary quantitative. We model three costs of classical reasoning: the size overhead of the Gödel–Gentzen double-negation translation, the expansion of the counter-model search space when classical valuations are replaced by Kripke valuations, and the branching explosion when LEM instances are added to a proof search. For a representative propositional formula of size $9$, the translation has size $22$, an overhead factor of 22/9 ≈ 2.44; for $n = 10$ variables the constructive model space exceeds the classical one by a factor of 1.5¹0 ≈ 57.7 on a two-world Kripke chain and 2¹0 = 1024 on a three-world chain; for a proof search of branching factor $3$ and depth $12$ with $5$ atoms, LEM instantiation multiplies the search tree by 2⁵ = 32, from 531,441 to 17,006,112 nodes; and the fraction of Kripke valuations on a three-world chain satisfying all n LEM instances falls as 2^-n, to 1/1024 at $n = 10$. As a contrast case we derive the workload of a boundary-element benchmark (96 elements, 64 N) whose computation never crosses the boundary. The result changes how the classical/constructive choice should be priced: as a computable overhead budget, not a philosophical stance.",
  "abstract_markdown": "Engineers who build proof assistants, ontology-based query engines, and LLM reasoning pipelines must choose whether their logic admits the law of the excluded middle (LEM), the principle that every proposition $\\varphi$ satisfies $\\varphi \\vee \\neg\\varphi$, yet no standard overhead budget exists for that choice. This paper makes the classical/constructive boundary quantitative. We model three costs of classical reasoning: the size overhead of the Gödel–Gentzen double-negation translation, the expansion of the counter-model search space when classical valuations are replaced by Kripke valuations, and the branching explosion when LEM instances are added to a proof search. For a representative propositional formula of size $9$, the translation has size $22$, an overhead factor of $22/9 \\approx 2.44$; for $n = 10$ variables the constructive model space exceeds the classical one by a factor of $1.5^{10} \\approx 57.7$ on a two-world Kripke chain and $2^{10} = 1024$ on a three-world chain; for a proof search of branching factor $3$ and depth $12$ with $5$ atoms, LEM instantiation multiplies the search tree by $2^{5} = 32$, from $531{,}441$ to $17{,}006{,}112$ nodes; and the fraction of Kripke valuations on a three-world chain satisfying all $n$ LEM instances falls as $2^{-n}$, to $1/1024$ at $n = 10$. As a contrast case we derive the workload of a boundary-element benchmark (96 elements, 64 N) whose computation never crosses the boundary. The result changes how the classical/constructive choice should be priced: as a computable overhead budget, not a philosophical stance.",
  "date": "2026-11-11",
  "first_published": "2026-11-11",
  "last_revised": "2026-11-11T00:00:00Z",
  "modified": "2026-11-11T00:00:00Z",
  "version": "1.0.0",
  "version_count": 1,
  "language": "en",
  "keywords": [],
  "quality_tags": [
    "High-quality scholarly research",
    "open-access scholarly work",
    "versioned research publication"
  ],
  "quality_label": "High-quality scholarly research",
  "quality_basis": "QNFO publisher classification for open-access, versioned research with a public revision history and reader correction channel; this is not a claim of independent peer review.",
  "quality_evidence_url": "https://qnfo.org/about",
  "peer_review_status": "Not independently peer-reviewed",
  "resource_type": "ScholarlyArticle",
  "doi": null,
  "doi_url": null,
  "url": "https://papers.qnfo.org/papers/the-excluded-middle-as-a-quantifiable-computational-boundary-translation-overhea",
  "license_url": "https://legal.qnfo.org/",
  "license_spdx": null,
  "sha256": "9f27afc88d453f904ae5f52393396686331fb291e22b1962efe546ab66c1602e",
  "version_url": "https://papers.qnfo.org/papers/the-excluded-middle-as-a-quantifiable-computational-boundary-translation-overhea/v/1.0.0",
  "datacite": {
    "schemaVersion": "http://datacite.org/schema/kernel-4",
    "identifiers": [
      {
        "identifier": "https://papers.qnfo.org/papers/the-excluded-middle-as-a-quantifiable-computational-boundary-translation-overhea",
        "identifierType": "URL"
      }
    ],
    "creators": [
      {
        "name": "Rowan Brad Quni-Gudzinas",
        "nameType": "Personal",
        "nameIdentifiers": [
          {
            "nameIdentifier": "https://orcid.org/0009-0002-4317-5604",
            "nameIdentifierScheme": "ORCID",
            "schemeUri": "https://orcid.org"
          }
        ]
      }
    ],
    "titles": [
      {
        "title": "The Excluded Middle as a Quantifiable Computational Boundary: Translation Overhead, Model-Space Expansion, and Search Cost of Classical Reasoning"
      }
    ],
    "publisher": "QNFO",
    "publicationYear": "2026",
    "resourceType": {
      "resourceTypeGeneral": "Text",
      "resourceType": "ScholarlyArticle"
    },
    "subjects": [
      {
        "subject": "High-quality scholarly research",
        "subjectScheme": "QNFO publisher classification",
        "schemeUri": "https://qnfo.org/about"
      },
      {
        "subject": "open-access scholarly work",
        "subjectScheme": "QNFO publisher classification",
        "schemeUri": "https://qnfo.org/about"
      },
      {
        "subject": "versioned research publication",
        "subjectScheme": "QNFO publisher classification",
        "schemeUri": "https://qnfo.org/about"
      }
    ],
    "dates": [
      {
        "date": "2026-11-11",
        "dateType": "Issued"
      },
      {
        "date": "2026-11-11",
        "dateType": "Updated"
      }
    ],
    "language": "en",
    "version": "1.0.0",
    "rightsList": [
      {
        "rightsUri": "https://legal.qnfo.org/"
      }
    ],
    "descriptions": [
      {
        "description": "Engineers who build proof assistants, ontology-based query engines, and LLM reasoning pipelines must choose whether their logic admits the law of the excluded middle (LEM), the principle that every proposition φ satisfies φ vee ¬φ, yet no standard overhead budget exists for that choice. This paper makes the classical/constructive boundary quantitative. We model three costs of classical reasoning: the size overhead of the Gödel–Gentzen double-negation translation, the expansion of the counter-model search space when classical valuations are replaced by Kripke valuations, and the branching explosion when LEM instances are added to a proof search. For a representative propositional formula of size $9$, the translation has size $22$, an overhead factor of 22/9 ≈ 2.44; for $n = 10$ variables the constructive model space exceeds the classical one by a factor of 1.5¹0 ≈ 57.7 on a two-world Kripke chain and 2¹0 = 1024 on a three-world chain; for a proof search of branching factor $3$ and depth $12$ with $5$ atoms, LEM instantiation multiplies the search tree by 2⁵ = 32, from 531,441 to 17,006,112 nodes; and the fraction of Kripke valuations on a three-world chain satisfying all n LEM instances falls as 2^-n, to 1/1024 at $n = 10$. As a contrast case we derive the workload of a boundary-element benchmark (96 elements, 64 N) whose computation never crosses the boundary. The result changes how the classical/constructive choice should be priced: as a computable overhead budget, not a philosophical stance.",
        "descriptionType": "Abstract"
      },
      {
        "description": "Publisher quality classification: High-quality scholarly research. QNFO publisher classification for open-access, versioned research with a public revision history and reader correction channel; this is not a claim of independent peer review.",
        "descriptionType": "Other"
      },
      {
        "description": "Peer review status: Not independently peer-reviewed",
        "descriptionType": "Other"
      }
    ],
    "formats": [
      "text/html"
    ]
  }
}