2
$\begingroup$

As far as I understand, first-order arithmetic incorporates first-order logic. It is a fact that a first-order logic with at least two binary predicates is undecidable. Doesn't this imply immediately the undecidability of arithmetic?

$\endgroup$
  • 1
    $\begingroup$ Actually you only need one binary predicate for undecidability. However, as you add axioms, the set of provable sentences grows and may or may not become decidable depending on what axioms you add. $\endgroup$ – Rob Arthan Oct 27 '13 at 16:29
  • $\begingroup$ @RobArthan sorry, I meant two predicates including equality. The thing I still don't understand is how can it become decidable? See my comment to André Nicolas's answer. $\endgroup$ – level1807 Oct 27 '13 at 16:42
  • $\begingroup$ Actually, you don't even need equality for undecidability. Just one binary predicate (that is not necessarily equality) will do. $\endgroup$ – Rob Arthan Oct 28 '13 at 1:07
  • 1
    $\begingroup$ Indeed, it is also well known that these two sets (arithmetic truths versus firs-order validities) have different Turing (undecidability) degrees. In particular, there is no computable reduction reducing "arithemtic truths" to "first-order validities". If you want to take a deeper look at this I suggest you start looking at the artihmetical hierarchy (for instance, at wikipedia en.wikipedia.org/wiki/Arithmetical_hierarchy ) $\endgroup$ – boumol Oct 28 '13 at 11:11
2
$\begingroup$

Suppose you have two binary predicates $R$ and $S$. If you add the axiom $(\forall x)(\forall y)[R(x,y) \land S(x,y)]$, the resulting theory is complete and decidable. Basically, with that axiom $R$ and $S$ are always true, so you can replace them with "True" and ignore all quantifiers.

So, adding axioms to an undecidable system can result in a decidable system.

$\endgroup$
  • $\begingroup$ Yep, now I got it, something like this was on the tip of my tongue all the time, but yours is a great example! Thanks! $\endgroup$ – level1807 Oct 27 '13 at 17:17
1
$\begingroup$

One can make an argument along those lines, by making "incorporates" precise enough. However, note that the first-order theory of algebraically closed fields of characteristic $0$ is decidable, as is the theory of real-closed fields.

$\endgroup$
  • $\begingroup$ I guess, making "incorporates" precise enough is exactly what I need and what I have a problem doing. Another thought is that maybe arithmetic induces some new inference rules which can turn some of the undecidable formulas of FOL into decidable ones? Is that what prevents my implication? $\endgroup$ – level1807 Oct 27 '13 at 16:02
  • 1
    $\begingroup$ One could say that this happens with the theory of real-closed fields. The theory of rings, for example, is undecidable. $\endgroup$ – André Nicolas Oct 27 '13 at 16:12

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.