Division by zero Emil Jeˇr´abek
Division by zero Emil Jeˇr´abek Institute of Mathematics of the Czech Academy of Sciences Zitn´a 25, 115 67 Praha 1, Czech Republic, email: ˇ jerabek@math.cas.cz September 24, 2016 To Albert Visser 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. Keywords: Robinson arithmetic, Diophantine equation, decidability, universal theory MSC: 03F30 1 Introduction The standard G¨odel–Church–Turing–Rosser undecidability theorem tells us that if T is any consistent theory extending Robinson’s arithmetic Q, the set of Π1 consequences of T is undecidable. Furthermore, the Matiyasevich–Robinson–Davis–Putnam theorem shows that every Π1 formula is equivalent to unsolvability of a certain Diophantine equation. Since the MRDP theorem can be formalized in I∆0 + EXP due to Gaifman and Dimitracopoulos [5], we see that if T extends I∆0 + EXP, it is undecidable whether a given Diophantine equation is provably unsolvable in T, or dually, whether it has a solution in a model of T. Surprisingly, Kaye [6, 7] proved that the same holds already for extensions of the weak theory IU − 1 (induction for parameter-free bounded universal formulas), despite that it likely does not formalize the MRDP theorem as such. One can check that Kaye’s methods also apply to extensions of Cook’s theory PV of polynomial-time functions (see e.g. Kraj´ıˇcek [8] for a definition). Going further down, decidability of solvability of Diophantine equations in models of the theory IOpen of quantifier-free induction has remained an intriguing open problem ever since it was posed by Shepherdson [12], see e.g. [13, 3, 10] for partial results. The purpose of this note is to show that solvability of Diophantine equations in models of Q is decidable, specifically NP-complete. Since Q does not include ring identities that allow the usual manipulations of polynomials, it may be ambiguous what exactly is meant by Diophantine equations, so let us first state the problem precisely. Definition 1.1 A Diophantine equation is a formula of the form t(~x) = u(~x), 1 where t and u are terms in the basic language of arithmetic LQ = h0, S, +, ·i. If T is a theory whose language contains LQ, the Diophantine satisfiability problem for T, denoted DT , consists of all Diophantine equations t = u satisfiable in a model of T (shortly: T-satisfiable). That is, DT = {ht, ui : T + ∃~x t(~x) = u(~x) is consistent}. The decidability of DQ is on the whole not so surprising, as Q has models with “black holes” (to use Albert Visser’s term) that can serve to equate nearly any pair of terms. It turns out however that while this argument yields a simple proof of decidability of Diophantine satisfiability for certain mild extensions of Q, it does not suffice for Q itself: it only provides a reduction to systems of equations of a special form (see Eq. (1) below) that we have to investigate in detail. We need to embed certain models in models of Q as a part of our main construction, and to facilitate this goal, we will explicitly axiomatize the universal consequences of Q, which could be of independent interest. See [1, 2] for related work.
0 件のコメント:
コメントを投稿