A Constructive Proof of Rice's Theorem and the Halting Problem via Hilbert's Tenth Problem

Jonathan Brossard

arxiv: 2604.16477 · v1 · submitted 2026-04-11 · 💻 cs.LO · cs.CR

A Constructive Proof of Rice's Theorem and the Halting Problem via Hilbert's Tenth Problem

Jonathan Brossard This is my paper

Pith reviewed 2026-05-10 15:15 UTC · model grok-4.3

classification 💻 cs.LO cs.CR

keywords Rice's theoremhalting problemHilbert's tenth problemconstructive mathematicsundecidabilityDiophantine equationsintuitionistic logicprogram properties

0 comments

The pith

Rice's theorem follows constructively from the undecidability of Hilbert's tenth problem using a two-witness construction.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper shows how to prove that no non-trivial property of programs is decidable by reducing it to the undecidability of solving Diophantine equations. This proof avoids any use of diagonalization or self-reference and works without assuming the law of excluded middle beyond the single assumption about Hilbert's tenth problem. It does this by linking each equation to two programs that act as opposite witnesses for the property only if the equation has a solution. A reader would care because this makes the classic undecidability results hold in a more restrictive logical setting, with the halting problem as a direct consequence.

Core claim

Given any non-trivial semantic property P of programs, the construction produces, for every Diophantine polynomial D, a pair of programs S0_D and S1_D. When D has a solution, one program satisfies P and the other does not. When D has no solution, both programs diverge in exactly the same way. Therefore, if there were a decider for P, its outputs on the pair would differ exactly when D is solvable, yielding a decider for Hilbert's tenth problem, which is assumed impossible. The proof never splits cases on whether the equation is solvable and never inspects the behavior of the always-diverging program.

What carries the argument

The two-witness construction that attaches to each Diophantine polynomial a pair of programs behaving as positive and negative witnesses for the property precisely when the polynomial is solvable.

Load-bearing premise

The programs attached to an unsolvable polynomial must be indistinguishable by any decider for the property, forcing both to diverge identically.

What would settle it

A computation showing that for some specific Diophantine equation without solutions, the corresponding S0 and S1 programs are distinguishable by a hypothetical property decider would falsify the construction.

Figures

Figures reproduced from arXiv: 2604.16477 by Jonathan Brossard.

**Figure 1.** Figure 1: Reduction directions. Classical proofs derive Rice’s theorem from the halting problem (left arrow). This paper reduces from MRDP (right arrows), with the halting problem as a corollary. 2. Preliminaries 2.1. Partial Functions and Convergence. We work in a standard model of partial computable functions. For a program e and input x, we write φe(x) ↓ if the computation converges, and φe(x) ↑ if it diverges. … view at source ↗

read the original abstract

Rice's theorem states that no non-trivial semantic property of programs is decidable. Classical proofs proceed by reduction from the halting problem, invoking the law of excluded middle (LEM) twice: once through diagonalization, and once through a case split on whether the always-diverging program bot satisfies the property in question. We present a proof that is constructive relative to the undecidability of Hilbert's Tenth Problem (MRDP): valid in intuitionistic logic, requiring neither diagonalization nor self-reference, and adding no classical reasoning beyond the MRDP assumption itself. The key idea is a two-witness construction. Given a non-trivial property P, we attach to each Diophantine polynomial D a pair of programs S^0_D, S^1_D that behave like the negative and positive witnesses for P when D is solvable, and both diverge identically when it is not. A hypothetical decider for P would therefore decide Diophantine solvability via the difference delta_D = DecideP(S^1_D) - DecideP(S^0_D) -- contradicting the MRDP theorem. The argument is structured as two separate implications, never asserting a disjunction about solvability, and never examining P(bot). The undecidability of the halting problem follows as an immediate corollary: a single application of Rice's theorem to the Terminates property. A formalization in the Rocq proof assistant confirms both results within a step-indexed model of computation, with the undecidability of Hilbert's Tenth Problem as the sole external axiom. Both Rice_Theorem and Halting_Problem are closed under the global context.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

This paper gives a constructive proof of Rice's theorem by reducing it to MRDP undecidability with a two-witness program construction that avoids diagonalization and extra classical steps.

read the letter

The main point is a constructive version of Rice's theorem that reduces directly to the undecidability of Hilbert's Tenth Problem. For any non-trivial property P, the authors build, for each Diophantine polynomial D, a pair of programs S0_D and S1_D. When D has a solution these programs realize the positive and negative cases for P; when it has none, both diverge in the same way. Any decider for P then decides solvability of D by looking at the difference between the two answers, without ever splitting on whether a solution exists or examining the always-diverging program. The halting problem follows at once by taking P to be termination. The whole argument is split into two implications so it stays inside intuitionistic logic, and the only external assumption is MRDP undecidability itself. A Rocq formalization in a step-indexed model confirms the reduction and keeps both theorems closed under the context with no other axioms added. The construction is internally consistent and the formalization supplies real evidence that the program behaviors line up as claimed. The soft spots are limited. The step-indexed model has to be trusted to capture semantic equivalence correctly for the diverging cases, but the mechanical check reduces the risk. The result stays inside constructive computability and does not claim broader impact. This paper is for logicians and formal-methods researchers who want mechanized, constructive versions of classical undecidability theorems. A reader building libraries of computability results in a proof assistant would find the explicit two-witness reduction and the Rocq scripts useful. It shows clear engagement with the relevant literature on MRDP and Rice's theorem. I would send it to peer review.

Referee Report

0 major / 3 minor

Summary. The paper claims to provide a constructive (intuitionistic) proof of Rice's theorem—that no non-trivial semantic property of programs is decidable—relative to the undecidability of Hilbert's Tenth Problem (MRDP theorem), without diagonalization, self-reference, or additional classical reasoning. The key device is a two-witness construction: for each Diophantine polynomial D, programs S^0_D and S^1_D are attached such that they realize the negative and positive witnesses for a non-trivial property P precisely when D is solvable, and diverge identically (hence are equivalent under P) when D is unsolvable. A hypothetical decider for P then yields a decider for solvability via the difference delta_D, contradicting MRDP. The undecidability of the halting problem follows immediately by instantiating P as Terminates. The argument is formalized in Rocq using a step-indexed model of computation, with MRDP as the sole external axiom.

Significance. If the central claim holds, the result is significant because it supplies a machine-checked proof in Rocq that stays strictly within intuitionistic logic, relies only on the independent MRDP axiom, and avoids both diagonalization and any case analysis on solvability or on the behavior of the always-diverging program. The explicit two-witness reduction and the fact that both Rice_Theorem and Halting_Problem are closed under the global context constitute a clear technical advance in constructive computability.

minor comments (3)

[Abstract] Abstract: the claim that the proof is 'valid in intuitionistic logic' and 'adds no classical reasoning beyond the MRDP assumption' is central, yet the abstract gives no indication of how the step-indexed model ensures that the two programs S^0_D and S^1_D are observationally equivalent when D is unsolvable; a one-sentence pointer to the relevant Rocq lemma would help.
[Formalization] §4 (or the formalization section): while the two-witness construction is described at a high level, the manuscript does not explicitly record the lemma that delta_D = 1 exactly when D is solvable and delta_D = 0 when D is unsolvable; adding this as a numbered statement would make the reduction to MRDP fully transparent.
[Corollary] The paper correctly notes that the halting-problem corollary follows from a single application of Rice's theorem to Terminates, but it would be useful to state the precise instantiation of the two-witness programs for this case so that readers can see the reduction is uniform.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for the careful and accurate summary of our manuscript, which correctly identifies the central technical device (the two-witness construction) and the fact that the argument remains strictly intuitionistic once the MRDP axiom is assumed. The recommendation of minor revision is noted; we have prepared a revised version that incorporates the minor clarifications implied by the overall assessment.

Circularity Check

0 steps flagged

No significant circularity; derivation is self-contained via external axiom

full rationale

The paper reduces Rice's theorem to the undecidability of Hilbert's Tenth Problem (MRDP) using an independent two-witness construction: for each Diophantine polynomial D, programs S^0_D and S^1_D are defined so that they realize distinct witnesses for P precisely when D is solvable and diverge identically otherwise. A hypothetical decider for P then yields a decider for solvability via delta_D without case splits or LEM. This is a standard reduction, not a self-definition or fitted prediction. The Rocq formalization treats MRDP as the sole external axiom and verifies the argument remains intuitionistic. No self-citation is load-bearing, no ansatz is smuggled, and no step renames a known result as a derivation. The central claim therefore has independent content beyond its inputs.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The central claim rests on the undecidability of Hilbert's Tenth Problem as the sole external axiom and the correctness of the two-witness program construction in the step-indexed computational model.

axioms (1)

domain assumption Undecidability of Hilbert's Tenth Problem (MRDP theorem)
Used as the sole external axiom in the formalization; the proof adds no further classical reasoning.

pith-pipeline@v0.9.0 · 5592 in / 1312 out tokens · 92196 ms · 2026-05-10T15:15:13.049273+00:00 · methodology

discussion (0)

Reference graph

Works this paper leans on

2 extracted references · 2 canonical work pages · 1 internal anchor

[1]

Appel and David McAllester

doi:10.1145/504709.504712. [Bau06] Andrej Bauer. First steps in synthetic computability theory. Electronic Notes in Theoretical Computer Science, 155:5–31, 2006. doi:10.1016/j.entcs.2005.11.049. [Bee85] Michael Beeson. Foundations of Constructive Mathematics . Springer, 1985. doi:10.1007/ 978-3-642-68952-9 . [BGP21] Vasco Brattka, Guido Gherardi, and Arno...

work page doi:10.1145/504709.504712 2006
[2]

Considering The Satisfiability of Cubic Diophantine Equations

doi:10.1007/3-540-45699-6_8 . [Ric53] Henry Gordon Rice. Classes of recursively enumerable sets and their decision problems. Trans- actions of the American Mathematical Society , 74(2):358–366, 1953. doi:10.2307/1990888. [Rog67] Hartley Rogers. Theory of Recursive Functions and Effective Computability . McGraw-Hill, 1967. [Ros25] M. Rosko. Cubic incomplet...

work page internal anchor Pith review Pith/arXiv arXiv doi:10.1007/3-540-45699-6_8 1953

[1] [1]

Appel and David McAllester

doi:10.1145/504709.504712. [Bau06] Andrej Bauer. First steps in synthetic computability theory. Electronic Notes in Theoretical Computer Science, 155:5–31, 2006. doi:10.1016/j.entcs.2005.11.049. [Bee85] Michael Beeson. Foundations of Constructive Mathematics . Springer, 1985. doi:10.1007/ 978-3-642-68952-9 . [BGP21] Vasco Brattka, Guido Gherardi, and Arno...

work page doi:10.1145/504709.504712 2006

[2] [2]

Considering The Satisfiability of Cubic Diophantine Equations

doi:10.1007/3-540-45699-6_8 . [Ric53] Henry Gordon Rice. Classes of recursively enumerable sets and their decision problems. Trans- actions of the American Mathematical Society , 74(2):358–366, 1953. doi:10.2307/1990888. [Rog67] Hartley Rogers. Theory of Recursive Functions and Effective Computability . McGraw-Hill, 1967. [Ros25] M. Rosko. Cubic incomplet...

work page internal anchor Pith review Pith/arXiv arXiv doi:10.1007/3-540-45699-6_8 1953