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?