On decidable extensions of Presburger arithmetic: from A. Bertrand numeration sytems to Pisot numbers
Françoise Point · Journal of Symbolic Logic · 2000
Abstract We study extensions of Presburger arithmetic with a unary predicate R and we show that under certain conditions on R, R is sparse (a notion introduced by A. L. Semënov) and the theory of 〈ℕ, +, R〉 is decidable. We axiomatize this theory and we show that in a reasonable language, it admits quantifier elimination. We obtain similar results for the structure 〈ℚ, +, R〉.