Büchi arithmetic
# 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 Büchi 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 Büchi arithmetic.

## Büchi arithmetic and automata

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 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}$ can be defined in ${\text{FO}}(V_{k},+)$, the first-order theory of $V_{k}$ and $+$.

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

