We investigate the decidability of the monadic second-order (MSO) theory of the structure
❬N; <, P1, … , Pk❭,
for various unary predicates
P1, …, Pk ⊆ N.
We focus in particular on 'arithmetic' predicates arising
in the study of linear recurrence sequences, such as fixed-base powers
Powk = {kn : n ∈ N},
k-th powers Nk =
{nk : n ∈ N},
and the set of terms of the Fibonacci sequence Fib =
{0, 1, 2, 3, 5, 8, 13, …}
(and similarly for other linear recurrence sequences having a single,
non-repeated, dominant characteristic root).
We obtain several new unconditional and conditional decidability results, a
select sample of which are the following:
∙ The MSO theory of
❬N; <, Pow2, Fib❭ is
decidable;
∙ The MSO theory of
❬N; <, Pow2, Pow3, Pow6❭
is decidable;
∙ The MSO theory of
❬N; <, Pow2, Pow3, Pow5❭
is decidable assuming Schanuel's conjecture;
∙ The MSO theory of
❬N; <, Pow4, N2❭ is
decidable;
∙ The MSO theory of
❬N; <, Pow2, N2❭ is
Turing-equivalent to the MSO theory of
❬N; <, S❭, where S is
the predicate corresponding to the binary expansion of
√2. (As the binary expansion of √2 is widely
believed to be normal, the corresponding MSO theory is
in turn expected to be decidable.)
These results are obtained by exploiting and combining techniques from
dynamical systems, number theory, and automata theory.
Proceedings of LICS 24, 2024. 17 pages.
Distinguished Paper Award.
PDF
© 2023 Valérie Berthé, Toghrul Karimov, Joris
Nieuwveld, Joël Ouaknine, Mihir Vahanwala, and James Worrell.