# Büchi arithmetic

Büchi arithmetic of base k is the first-order theory of the natural numbers with addition and the function $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 Presburger arithmetic contains only the addition operation, $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 Presburger arithmetic.

## Büchi arithmetic and automaton

A subset $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$ this means that the set of integers of X in base k is accepted by an automaton. Similarly if $n>1$ there exists an automata that read firsts digit, then second digits, and so on, of n integers in base k, and accept the words if the n integers are in the relation X.

## Properties of Büchi arithmetic

Two numbers k and l are multiplicatively dependent if there exists integers n and m such that $k^n=l^m$.

If k and l are multiplicatively dependent then Büchi arithmetic of base k and l have the same expressivity. Indeed $V_l$ can be defined in $\text{FO}(V_k,+)$.

Else the theory with both $V_k$ and $V_l$ function is equivalent to Peano arithmetic the logic with addition and multiplication since multiplication is definable in $\text{FO}(V_k,V_l,+)$.

On the other hand by the Cobham–Semenov theorem, if a relation is definable in both k and l Büchi arithmetics it is definable in Presburger arithmetic.[1][2]

## References

1. ^ Cobham, Alan (1969). "On the base-dependence of sets of numbers recognizable by finite automata". Math. Systems Theory 3: 186–192. doi:10.1007/BF01746527.
2. ^ Semenov, A. L. (1977). "Presburgerness of predicates regular in two number systems". Sibirsk. Mat. Zh. (in Russian) 18: 403–418.