Skip to main content
1 of 7
Emil Jeřábek
  • 47.5k
  • 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 therem: 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.

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