
TL;DR
This paper demonstrates that the set of Diophantine equations provably unsolvable in Robinson's arithmetic Q is decidable, contrasting with the undecidability in stronger theories, through analysis of a specific class of equations.
Contribution
It introduces a novel approach to decide unsolvability of certain Diophantine equations within Q by analyzing a previously unexplored class of equations and axiomatizing Q's universal fragment.
Findings
Decidability of unsolvable Diophantine equations in Q
Analysis of a new class of Diophantine equations
Axiomatization of Q's universal fragment
Abstract
For any sufficiently strong theory of arithmetic, the set of Diophantine equations provably unsolvable in the theory is algorithmically undecidable, as a consequence of the MRDP theorem. In contrast, we show decidability of Diophantine equations provably unsolvable in Robinson's arithmetic Q. The argument hinges on an analysis of a particular class of equations, hitherto unexplored in Diophantine literature. We also axiomatize the universal fragment of Q in the process.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
