Logic, Decidability and Numeration Systems

The theorem of Büchi-Bruyère states that a subset of N^d is b-recognizable if and only if it is b-definable. As a corollary, the first-order theory of (N,+,V_b) is decidable (where V_b(n) is the largest power of the base b dividing n). This classical result is a powerful tool in order to show that many properties of b-automatic sequences are decidable. The first part of my lecture will be devoted to presenting this result and its applications to b-automatic sequences. Then I will move to b-regular sequences, which can be viewed as a generalization of b-automatic sequences to integer-valued sequences. I will explain how first-order logic can be used to show that many enumeration problems of b-automatic sequences give rise to corresponding b-regular sequences. Finally, I will consider more general frameworks than integer bases and (try to) give a state of the art of the research in this domain.