Büchi arithmetic explained
Büchi arithmetic of base k is the first-order theory of the natural numbers with addition and the function
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,
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
is definable in Büchi arithmetic of base
k if and only if it is
k-recognisable.
If
this means that the set of integers of
X in base
k is accepted by an
automaton. Similarly if
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
can be defined in
, the first-order theory of
and
.
Otherwise, an arithmetic theory with both
and
functions is equivalent to
Peano arithmetic, which has both addition and multiplication, since multiplication is definable in
.
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
- Web site: Bès. Alexis. A survey of Arithmetical Definability. 27 June 2012. https://archive.today/20121128154616/http://130.203.133.150/viewdoc/summary?doi=10.1.1.2.2136#. 2012-11-28. dead.
Further reading
- Bès . Alexis . Undecidable extensions of Büchi arithmetic and Cobham-Semënov theorem . 0896.03011 . J. Symb. Log. . 62 . 4 . 1280–1296 . 1997 . 10.2307/2275643 . 2275643 . 10.1.1.2.1007 . 31780865 .
Notes and References
- Alan . Cobham . On the base-dependence of sets of numbers recognizable by finite automata . Math. Systems Theory . 3 . 1969 . 2 . 186–192 . 10.1007/BF01746527 . 19792434 .
- A. L. . Semenov . Presburgerness of predicates regular in two number systems . Russian . Sibirsk. Mat. Zh. . 18 . 1977 . 403–418 .