Büchi arithmetic of base k is the first-order theory of the natural numbers with addition and the function
Contents
Unlike Peano arithmetic, Büchi arithmetic is a decidable theory. This means it is possible to effectively determine, for any sentence in the language of Büchi arithmetic, whether that sentence is provable from the axioms of Büchi arithmetic.
Büchi arithmetic and automaton
A subset
If
Properties of Büchi arithmetic
If k and l are multiplicatively dependent, then the Büchi arithmetics of base k and l have the same expressivity. Indeed
Otherwise, an arithmetic theory with both
Further, by the Cobham–Semënov theorem, if a relation is definable in both k and l Büchi arithmetics, then it is definable in Presburger arithmetic.