Diophantine equations in fragments in arithmetic (Q1112811)

\textit{J. C. Shepherdson} [The rule of induction in the free variable arithmetic based on \(+\) and \(\cdot\), Proc. Symp. Clermont-Ferrand 1961; Theory of models, Proc. 1963 Int. Symp. Berkeley, 342-358 (1965; Zbl 0154.262); Bull. Acad. Pol. Sci., Sér. Sci. Math. Astron. Phys. 12, 79- 86 (1964; Zbl 0132.247)] investigated several fragments of arithmetic with open induction. Using non-standard models he established the independence of some simple diophantine equations: E.g., each of \(nx+m=ny\) \((0<m<n)\), \(3x+2=y^ 2\), \(x^ 2+x+1=2y\), \((x+1)^ 2=2(y+1)^ 2\), \((x+1)^ 3+(y+1)^ 3=(z+1)^ 3\) is independent of the open induction fragment with the symbols 0, N (successor), V (predecessor), \(+\), and \(\cdot\); the irrationality of \(\sqrt{2}\) and Fermat's equations with exponents \(n\geq 3\) are also independent of the stronger system where the function \(\dot-\) is added. \textit{A. J. Wilkie} [Logic Colloq. '77, Wrocław 1977, Stud. Logic Found. Math. 96, 285-296 (1978; Zbl 0449.03076)] gave a model-theoretic characterization of polynomials having a zero in a ring belonging to a model of this system. \textit{L. van den Dries} [Lect. Notes Math. 834, 346-362 (1980; Zbl 0454.03034)] showed that Wilkie's characterization is decidable in the special case of polynomials in two variables. In the following we use elementary proof-theoretic means in order to characterize diophantine formulae - i.e., open formulae built up from polynomial equations - which are provable in several fragments of arithmetic, including the systems studied by Shepherdson. The main idea of these characterizations consists in a translation of the derivability relation into a number-theoretic relation.