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

• URL: http://arxiv.org/abs/2604.16477v1
• Date: Sat, 11 Apr 2026 20:45:58 GMT
• Title: A Constructive Proof of Rice's Theorem and the Halting Problem via Hilbert's Tenth Problem
• Abstract summary: Rice's theorem states that no non-trivial semantic property of programs is decidable.<n>We present a proof that is constructive relative to the undecidability of Hilbert's Tenth Problem (MRDP)<n>The argument is structured as two separate implications, never asserting a disjunction about solvability, and never examining P(bot)
• Score: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• 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.

Related papers

• The Semantic Elevation Operator and the Closure of the Undecidable Class under Preservation [0.0]
  Self-modifying systems require analysing not whether a property holds now, but whether it is preserved when the system rewrites itself.<n>We formalise this transition through a semantic elevation operator, which turns the static question "does x satisfy P?" into the dynamic question "is P preserved after x is transformed by?"<n>We prove that when is intensional, the elevated property remains undecidable even though it breaks the extensionality that Rice's theorem requires.
  arXiv  Detail & Related papers  (2026-09-10T09:56:17Z)
• Auditing an AI-Generated Mathematical Proof: A Correction to a Greedy Conditioning Lemma in Quantum Parallel Repetition [0.0]
  This note gives an explicit counterexample, identifies the intended continuation condition, and supplies a complete corrected proof.<n>It should not, however, be read as an independent verification of the main parallel-repetition theorem.
  arXiv  Detail & Related papers  (2026-08-03T15:12:46Z)
• Syntactic Systems Cannot See Semantic Invariants [0.0]
  Hetzl and Vierling asked whether two theories of induction, open induction and clause set cycles, are incomparable.<n>They proved one direction and left the other open.<n>The thing that separates the two theories is the order of two constants, and that order is a fact about numbers, not about symbols.
  arXiv  Detail & Related papers  (2026-06-15T20:34:13Z)
• Exact Structural Abstraction and Tractability Limits [0.0]
  Exact correctness depends only on the induced classes $s sim_R simation' iff mathrmAdm_R(s)$.<n>Decision, search, approximation, statistical, randomized horizon, and distributional guarantees all reduce to this same quotient-recovery problem.
  arXiv  Detail & Related papers  (2026-04-08T17:59:47Z)
• Aumann's theorem beyond ontology: quantum, postquantum, and indefinite causal order [0.0]
  We derive an operational version of Aumann's agreement theorem without assuming an objective state of the world.<n>This allows us to establish the theorem's validity in quantum theory and even in situations with indefinite causal order or involving hypothetical postquantum phenomena.<n>We comment on seemingly contradictory results in the literature and point to the one place where the theorem might fail: Wigner's friend-type situations.
  arXiv  Detail & Related papers  (2026-03-24T18:00:00Z)
• A Theory of $θ$-Expectations [2.1756081703276]
  We develop a framework for a class of differential equations where the driver is a pointwise geometry.<n>The system's tractability is predicated on a global existence of a unique and globally globally.<n> Lipschitz maximizer map for the driver function.
  arXiv  Detail & Related papers  (2025-07-27T16:56:01Z)
• Proving Theorems Recursively [80.42431358105482]
  We propose POETRY, which proves theorems in a level-by-level manner. Unlike previous step-by-step methods, POETRY searches for a sketch of the proof at each level. We observe a substantial increase in the maximum proof length found by POETRY, from 10 to 26.
  arXiv  Detail & Related papers  (2024-05-23T10:35:08Z)
• Some consequences of Sica's approach to Bell's inequalities [55.2480439325792]
  Louis Sica derived Bell's inequalities from the hypothesis that the time series of outcomes observed in one station does not change if the setting in the other station is changed. In this paper, Sica's approach is extended to series with non ideal efficiency and to the actual time structure of experimental data.
  arXiv  Detail & Related papers  (2024-03-05T13:59:52Z)
• Connecting classical finite exchangeability to quantum theory [45.76759085727843]
  Exchangeability is a fundamental concept in probability theory and statistics.<n>It allows to model situations where the order of observations does not matter.<n>It is well known that both theorems do not hold for finitely exchangeable sequences.
  arXiv  Detail & Related papers  (2023-06-06T17:15:19Z)
• Connes implies Tsirelson: a simple proof [91.3755431537592]
  We show that the Connes embedding problem implies the synchronous Tsirelson conjecture. We also give a different construction of Connes' algebra $mathcalRomega$ appearing in the Connes embedding problem.
  arXiv  Detail & Related papers  (2022-09-16T13:59:42Z)
• A possibilistic no-go theorem on the Wigner's friend paradox [0.0]
  We present a probability-free version of the Local Friendliness theorem. It builds upon Hardy's no-go theorem for local hidden variables.
  arXiv  Detail & Related papers  (2022-05-24T17:31:54Z)
• The Franke-Gorini-Kossakowski-Lindblad-Sudarshan (FGKLS) Equation for Two-Dimensional Systems [62.997667081978825]
  Open quantum systems can obey the Franke-Gorini-Kossakowski-Lindblad-Sudarshan (FGKLS) equation. We exhaustively study the case of a Hilbert space dimension of $2$.
  arXiv  Detail & Related papers  (2022-04-16T07:03:54Z)
• multiPRover: Generating Multiple Proofs for Improved Interpretability in Rule Reasoning [73.09791959325204]
  We focus on a type of linguistic formal reasoning where the goal is to reason over explicit knowledge in the form of natural language facts and rules. A recent work, named PRover, performs such reasoning by answering a question and also generating a proof graph that explains the answer. In our work, we address a new and challenging problem of generating multiple proof graphs for reasoning over natural language rule-bases.
  arXiv  Detail & Related papers  (2021-06-02T17:58:35Z)
• Hardness of Random Optimization Problems for Boolean Circuits, Low-Degree Polynomials, and Langevin Dynamics [78.46689176407936]
  We show that families of algorithms fail to produce nearly optimal solutions with high probability. For the case of Boolean circuits, our results improve the state-of-the-art bounds known in circuit complexity theory.
  arXiv  Detail & Related papers  (2020-04-25T05:45:59Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.