Hacker Newsnew | past | comments | ask | show | jobs | submitlogin

Does anyone have an intuition for why Presburger arithmetic is decidable, but once you introduce x, it is not? If + can be rewritten as repeated succ, (which is decidable) and x can be rewritten as repeated +, then it seems logical that x should be decidable, but as any undergraduate CS student knows, Peano arithmetic is undecidable. What is so special about x exactly?


Its probably worth pointing out that the system with only multiplication and no addition is also decidable (Skolem arithmetic). Things get interesting when you have both multiplication and addition defined and the reason for that is basically the fundamental theorem of arithmetic which gives you unique prime factorisation and directly the Gödel encoding (writing out statements about integers as integers).

The fundamental theorem of arithmetic says for any non-zero natural number x there is a unique finite sequence of integers a_i such that x = 2^a_0 . 3^a_1 . 5^a_3 ... p_n^a_n and that given x the sequence a_i is computable (similarly given a_i you can easily construct their x).

This basically gives you a (bijective) mapping between integers and tuples of integers x <-> (a_0, a_1, ... a_n) which lets you build up more complicated structures and eventually construct the sentence you need for an incompleteness theorem (if you're as smart as Gödel).


That’s a great explanation, thank you!


> but as any undergraduate CS student knows, Peano arithmetic is undecidable

We went to very different universities it seems. Neither Peano arithmetic nor decidability were ever mentioned


It's a variable number of addition operations.


Isn’t + a variable number of succ’s? Why does x break decidability, but + does not? It seems to me you should be able to define a second order Presburger system with + replacing succ, and x replacing + to restore decidability. Or is there some issue with countability or assumption that is broken?




Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: