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)}${\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}}${\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.

A subset ${\displaystyle X\subseteq \mathbb {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 ${\displaystyle n=1}${\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}${\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.

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

Otherwise, an arithmetic theory with both ${\displaystyle V_{k}}${\displaystyle V_{k}} and ${\displaystyle V_{l}}${\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},+)}${\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]}

• Bès, Alexis. "A survey of Arithmetical Definability". Archived from the original on 2012年11月28日. Retrieved 27 June 2012.

• 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.

• Formal theories of arithmetic
• Logic in computer science
• Proof theory
• Model theory

• CS1 Russian-language sources (ru)