A Constructive Proof of Rice's Theorem and the Halting Problem via Hilbert's Tenth Problem
This work offers a novel constructive perspective on foundational undecidability results, relevant to logicians and computer scientists interested in intuitionistic proofs.
The authors provide a constructive proof of Rice's theorem and the halting problem's undecidability using Hilbert's Tenth Problem, avoiding classical reasoning like diagonalization and the law of excluded middle. The proof is formalized in the Rocq proof assistant.
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.