It is well known that Robinson arithmetic (Q) is undecidable, and in fact essentially undecidable. Matiyasevich's theorem implies that the quantifier-free fragment of Q is also undecidable. However, I'm unsure as to whether that fragment is essentially undecidable. Is every theory that interprets the quantifier-free fragment of Q undecidable as well?
$\begingroup$
$\endgroup$
9
-
3$\begingroup$ As far as I am aware, the quantifier-free fragment of $Q$ is not known to be undecidable. In particular, the more restricted fragment corresponding to unsolvability of Diophantine equations is decidable, see mathoverflow.net/a/194502 . $\endgroup$– Emil JeřábekCommented Jun 6, 2018 at 7:53
-
2$\begingroup$ The quantifier-free fragment is actually known not to be essentially undecidable. This follows from the result of Dyson, Jones, and Shepherdson quoted in mathoverflow.net/a/168412 . $\endgroup$– Emil JeřábekCommented Jun 6, 2018 at 7:57
-
1$\begingroup$ Hang on, my second comment is not correct. Dyson, Jones and Shepherdson give an (r.e.) extension of $Q$ whose universal fragment is decidable, but his does not imply it embeds in a fully decidable theory. $\endgroup$– Emil JeřábekCommented Jun 6, 2018 at 8:18
-
1$\begingroup$ I don’t think negative integers are the problem. The universal fragment of the theory of discretely ordered rings is also not known to be undecidable. The problem is one needs some consequences of Matiyasevich’s theorem to be provable in the theory, and this just does not work if the theory is too weak. It is nothing short of a miracle that it does work for theories as weak as $IE_1$. $\endgroup$– Emil JeřábekCommented Jun 6, 2018 at 9:14
-
1$\begingroup$ Now that I think about it, there is a confusion of terms (made worse by my comments). A statement like “the $\Gamma$-fragment of theory $T$ is decidable” is normally understood to mean “it is decidable if a given $\Gamma$-formula is provable in $T$”. But in principle, it could also be read as “it is decidable if a given formula is provable in the first-order theory axiomatized by $\Gamma$-formulas provable in $T$”, and this is I guess the intended meaning when speaking about essential undecidability. Now, the universal fragment of $Q$ is not known to be decidable under the first reading, ... $\endgroup$– Emil JeřábekCommented Jun 6, 2018 at 9:41
|
Show 4 more comments