The Cost of a Basic Logic Rule in Computer Reasoning

In the paper's words

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.

The abstract, verbatim, and its opening sentence is the claim. Every line below is quoted from the text.

Numbers it reports

1. 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$.

   from Abstract

2. The principal results, with their derivations, are: The Gödel–Gentzen translation of a representative propositional formula of size $9$ has size $22$, an overhead factor of $22/9 \approx 2.44$, derived in Section 4.1.

   from 1. Introduction

3. The Kripke counter-model space with $n = 10$ propositional variables exceeds the classical valuation space by a factor of $1.5^{10} \approx 57.7$ on a two-world chain and $2^{10} = 1024$ on a three-world chain, derived in Section 4.2.

   from 1. Introduction

4. Adding LEM instantiation for $5$ atoms to a proof search of branching factor $3$ and depth $12$ multiplies the search tree by $2^{5} = 32$, from $531{,}441$ to $17{,}006{,}112$ nodes, derived in Section 4.3.

   from 1. Introduction

5. The same work's deduction–detachment analysis — the classical equivalence $\Gamma, \varphi \vdash_{\mathrm{CL}} \psi \iff \Gamma \vdash_{\mathrm{CL}} \varphi \rightarrow \psi$, and its $n$-contractive generalization $\Gamma, \varphi \vdash_{\mathrm{FL}_{\mathrm{e}}^{n}} \psi \iff \Gamma \vdash_{\mathrm{FL}_{\mathrm{e}}^{n}} (1 \wedge \varphi)^{n} \rightarrow \psi$ [5, §3.1] — shows that even the basic move of reducing validity to theoremhood carries a formula-size price that depends on the logic, which is the same phenomenon our translation overhead measures.

   from 2. Background and Related Work

6. This is a concrete instance of our translation overhead: the compilation from ontological (classically reasoned) queries to executable database queries is exactly a double-negation-style content-preserving translation, and its size growth is the practical face of the factor computed in Section 4.1.

   from 2. Background and Related Work

How it is done

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

   from Abstract

2. Engineers who build systems that reason — proof assistants, automated theorem provers, ontology-based data access platforms, and LLM-based reasoning pipelines — must decide, usually without being told, whether their underlying logic admits the law of the excluded middle.

   from 1. Introduction

3. B] — and least-fixed-point construction is the canonical example of a constructive existence proof: the iteration $f^{n}(\bot)$ is the witness-producing procedure that a purely classical existence argument would lack.

   from 2. Background and Related Work

4. This paper's method is analytical modeling plus explicit arithmetic; no experiment, measurement, or software run was performed, and every number in Sections 4 and 5 is computed by hand from stated inputs.

   from 3. Methods

What would falsify it

1. A classical prover can close a goal $\exists x\, \varphi(x)$ by refuting $\neg \exists x\, \varphi(x)$ without ever producing an $x$; a constructive prover cannot, and must instead search for a witness.

   from 1. Introduction

2. At $n = 10$ atoms the same base tree would grow by $2^{10} = 1024$, to $531441 \times 1024 = 544195584$ nodes; the model therefore predicts that LEM-heavy proof searches become intractable in the atoms long before depth becomes the binding constraint.

   from 4.3 LEM branching in proof search

3. The empirical parallel of [3] would be falsified if structured reasoning frameworks retained their isolated accuracy inside production prompts; the study's own verification at $n = 100$ reports the degradation persisting [3, §12].

   from 6. Discussion

Where the claim stops

1. What the numbers do and do not establish.

   from 6. Discussion

2. It does not establish that these costs are the dominant costs in any deployed system, nor that they are tight: the LEM branching model of §4.3 counts only the instantiate-or-not choice and is explicitly a lower bound on the true multiplier, and the translation overhead of §4.1 is computed for one formula under a no-prior-simplification convention.

   from 6. Discussion

3. The factor $22/9 \approx 2.44$ assumes the translation is applied without simplifying double negations.

   from 6. Discussion

Where to read

1. Abstract241 words · 1 min
2. 1. Introduction717 words · 3 min
3. 2. Background and Related Work1,548 words · 7 min
4. 3. Methods628 words · 3 min
5. 4. Analysis1,407 words · 6 min
6. 5. Results275 words · 1 min
7. 6. Discussion564 words · 2 min
8. 7. Practical Implications and Engineering Pathways695 words · 3 min
9. 8. Conclusion199 words · 1 min
10. Provenance and AI Involvement240 words · 1 min