Decidability of diophantine equations in a theory adjacent to IOpen

Abstract

Hilbert’s 10th problem is the question whether there is an algorithm which, given a polynomial with integer coefficients, determines whether it has integer roots. It has been shown that no such algorithm exists as a consequence of the MRDP theorem. In other words: Diophantine satisfiability is undecidable for arithmetic. One can now ask whether the problem of Diophantine satisfiability is decidable for weaker theories of arithmetic. In this thesis we present a novel proof-theoretic approach for deciding Diophantine satisfiability problems. We work in a base arithmetical theory A in the language with successors, predecessors, addition and multiplication and use a result by Shepherdson to define a theory AB which is one axiom schema short of the theory of open induction over A. We show that Diophantine satisfiability of AB is decidable.