Skip to main content
3 of 7
added 693 characters in body
Emil Jeřábek
  • 47.4k
  • 4
  • 150
  • 209

If $T$ contains $I\Delta_0+\mathit{EXP}$ (or a strong theory like Peano arithmetic for that matter), then by the formalized MRDP theorem [1], $D_T$ is essentially the $\Pi^0_1$ fragment of $T$, which is of course undecidable if $T$ is consistent. Curiously, this holds even for some weaker theories that do not prove the MRDP theorem: in particular, Kaye [2] showed that $D_T$ is undecidable for any consistent extension of $IE_1$ (induction for bounded existential formulas).

On the other hand, it is a long-standing open problem whether $D_T$ is decidable for the theory of quantifier-free induction (IOpen); by results of Wilkie [3], this is equivalent to the same problem for the theory of $\mathbb Z$-rings.

Concerning Robinson arithmetic: the problem is not quite well defined here, as $Q$ does not prove the usual semiring axioms like distributivity, hence different terms representing the same polynomial may give different answer. Worse yet, the question only makes sense for integer polynomials, whereas the theory only has nonnegative integers, and its models cannot be extended with negatives in a coherent way. So, for definiteness, let me formulate it as $$D_T=\{(p,q):T\vdash\forall\bar x\,p(\bar x)\ne q(\bar x)\},$$ where $p$ and $q$ are terms representing polynomials with coefficients from $\mathbb N$ written as a sum of monomials, where the additions and multiplications are arbitrarily bracketed. Then one can show that $D_Q$ is decidable. The main reason is that $Q$ has a model with domain $\mathbb N\cup\{\infty\}$, where $x+\infty=\infty+x=x\cdot\infty=\infty\cdot x=\infty$, except that $\infty\cdot0=0$. It is easy to see that in this model, $p(\bar\infty)=\infty$ for any non-constant polynomial $p$, which means that $(p,q)\in D_Q$ only if at least one of the polynomials is constant, and this case is easy to deal with.

References:

[1] Haim Gaifman and Constantinos Dimitracopoulos, Fragments of Peano’s arithmetic and the MRDP theorem, in: Logic and Algorithmic, Monographie No. 30 de L'Enseignement Mathématique, Université de Genève, 1982, pp. 187–206.

[2] Richard Kaye, Hilbert's tenth problem for weak theories of arithmetic, Annals of Pure and Applied Logic 61 (1993), no. 1–2, pp. 63–73.

[3] Alex Wilkie, Some results and problems on weak systems of arithmetic, in: Angus Macintyre (ed.), Logic Colloquium ’77, North-Holland, 1978, pp. 285–296.

Emil Jeřábek
  • 47.4k
  • 4
  • 150
  • 209