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

If $T$ extends $I\Delta_0+\mathit{EXP}$, then by the formalized MRDP theorem, $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 theories that do not prove the MRDP theorem: in particular, Kaye showed that the conclusion holds for any 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, 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.

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