Timeline for Is the quantifier-free fragment of Robinson arithmetic essentially undecidable?
Current License: CC BY-SA 4.0
11 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jun 6, 2018 at 9:49 | comment | added | Mak Nazečić-Andrlon | Right, yes. I think I was thinking whether every consistent extension of the theory minus quantifiers is undecidable. I'll try to repair the question. | |
| Jun 6, 2018 at 9:42 | comment | added | Emil Jeřábek | ... but I think it is undecidable in the second reading, probably essentially undecidable. | |
| Jun 6, 2018 at 9:41 | comment | added | Emil Jeřábek | 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, ... | |
| Jun 6, 2018 at 9:20 | comment | added | Mak Nazečić-Andrlon | Right, it also holds for PA, even restricted to induction over $\Sigma_1$ formulas. So I take it that we can usually find strange models of $Q$ where things hold that shouldn't. | |
| Jun 6, 2018 at 9:14 | comment | added | Emil Jeřábek | 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$. | |
| Jun 6, 2018 at 8:57 | comment | added | Mak Nazečić-Andrlon | Ah, of course. I forgot the negative integers! | |
| Jun 6, 2018 at 8:18 | comment | added | Emil Jeřábek | 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. | |
| Jun 6, 2018 at 7:57 | comment | added | Emil Jeřábek | 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 . | |
| Jun 6, 2018 at 7:53 | comment | added | Emil Jeřábek | 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 . | |
| Jun 6, 2018 at 5:12 | review | First posts | |||
| Jun 6, 2018 at 5:38 | |||||
| Jun 6, 2018 at 5:09 | history | asked | Mak Nazečić-Andrlon | CC BY-SA 4.0 |