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).
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?