Büchi arithmetic of base k is the first-order theory of the natural numbers with addition and the function V k ( x ) {\displaystyle V_{k}(x)} which is defined as the largest power of k dividing x, named in honor of the Swiss mathematician Julius Richard Büchi. The signature of Büchi arithmetic contains only the addition operation, V k {\displaystyle V_{k}} and equality, omitting the multiplication operation entirely. 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 automata A subset X ⊆ N n {\displaystyle X\subseteq \mathbb {N} ^{n}} is definable in Büchi arithmetic of base k if and only if it is k-recognisable. If n = 1 {\displaystyle n=1} this means that the set of integers of X in base k is accepted by an automaton. Similarly if n > 1 {\displaystyle n>1} there exists an automaton that reads the first digits, then the second digits, and so on, of n integers in base k, and accepts the words if the n integers are in the relation X.
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 V l {\displaystyle V_{l}} can be defined in FO ( V k , + ) {\displaystyle {\text{FO}}(V_{k},+)} , the first-order theory of V k {\displaystyle V_{k}} and + {\displaystyle +} . Otherwise, an arithmetic theory with both V k {\displaystyle V_{k}} and V l {\displaystyle V_{l}} functions is equivalent to Peano arithmetic, which has both addition and multiplication, since multiplication is definable in FO ( V k , V l , + ) {\displaystyle {\text{FO}}(V_{k},V_{l},+)} . 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.
References
Bès, Alexis. "A survey of Arithmetical Definability". Retrieved 27 June 2012.{{cite web}}: CS1 maint: deprecated archival service (link)
Further reading Bès, Alexis (1997). "Undecidable extensions of Büchi arithmetic and Cobham-Semënov theorem". J. Symb. Log. 62 (4): 1280–1296. CiteSeerX 10.1.1.2.1007. doi:10.2307/2275643. JSTOR 2275643. S2CID 31780865. Zbl 0896.03011. {{cite journal}}: Cite uses deprecated parameter |citeseerx= (help)