arXiv · 2605.28408
A natural axiomatization of B\"uchi Arithmetic
Abstract
We investigate B\"uchi Arithmetic $\mathsf{BA}_k$ -- the elementary theory of the natural numbers equipped with addition and the function mapping a number $x$ to the greatest power of $k$ dividing $x$. $\mathsf{BA}_k$ is known to be decidable and to enjoy a few important properties, in particular, a first-order structure is automatic iff it is interpretable in $\mathsf{BA}_k$. We propose a natural axiomatization of this theory based on a comprehension schema restricted to bounded formulas, interpreting natural numbers as finite (multi)sets of powers of $k$ via their base-$k$ expansions. The completeness proof for this axiomatization proceeds through a formalization of the B\"uchi-Bruy\`ere Theorem on the equivalence of definability in B\"uchi Arithmetic and recognizability by finite automata.
Explore related subjects
Keep this discovery
Konstantin Kovalyov. 2026-05-27. A natural axiomatization of B\"uchi Arithmetic. https://arxiv.org/abs/2605.28408
Cite the original work for its findings. Save a collection to share your selection of sources.