Büchi arithmetic

From Wikipedia, the free encyclopedia
Jump to: navigation, search

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 Presburger 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 Presburger arithmetic.

Büchi arithmetic and automaton[edit]

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 automata that read firsts digit, then second digits, and so on, of n integers in base k, and accept the words if the n integers are in the relation X.

Properties of Büchi arithmetic[edit]

Two numbers k and l are multiplicatively dependent if there exists integers n and m such that k^n=l^m.

If k and l are multiplicatively dependent then Büchi arithmetic of base k and l have the same expressivity. Indeed V_l can be defined in \text{FO}(V_k,+).

Else the theory with both V_k and V_l function is equivalent to Peano arithmetic the logic with addition and multiplication since multiplication is definable in \text{FO}(V_k,V_l,+).

On the other hand by the Cobham–Semenov theorem, if a relation is definable in both k and l Büchi arithmetics it is definable in Presburger arithmetic.[1][2]


  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. 

Further reading[edit]

  • Bès, Alexis (1997). "Undecidable extensions of Büchi arithmetic and Cobham-Semënov theorem". J. Symb. Log. 62 (4): 1280–1296. doi:10.2307/2275643. Zbl 0896.03011.