# Büchi arithmetic

Büchi arithmetic of base k is the first-order theory of the natural numbers with addition and the function ${\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, ${\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 automaton

A subset ${\displaystyle X\subseteq \mathbb {N} ^{n}}$ is definable in Büchi arithmetic of base k if and only if it is k-recognisable.

If ${\displaystyle n=1}$ this means that the set of integers of X in base k is accepted by an automaton. Similarly if ${\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 ${\displaystyle V_{l}}$ can be defined in ${\displaystyle {\text{FO}}(V_{k},+)}$, the first-order theory of ${\displaystyle V_{k}}$ and ${\displaystyle +}$.

Otherwise, an arithmetic theory with both ${\displaystyle V_{k}}$ and ${\displaystyle V_{l}}$ functions is equivalent to Peano arithmetic, which has both addition and multiplication, since multiplication is definable in ${\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.[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.