On decidability of monadic logic of order over the naturals
expanded by unary predicates


We deal with the decidability of monadic second-order theory of the
natural numbers expanded by unary predicates. Elgot and Rabin found
many interesting unary predicates P such that the monadic theory of
{Nat, <, P} is decidable. Their results and techniques have been
extended over the years.  A class of effectively profinitely
ultimately periodic (e.p.u.p.) predicates was introduced. Many
examples of e.p.u.p. predicates were provided, and it was shown by
Carton and Thomas, that if P is an e.p.u.p. predicate then the monadic
theory of {Nat, <, P} is decidable.

We show that this is a necessary condition.

Theorem:  The monadic second-order theory  of {Nat, <, P} is
decidable if and only if  P is effectively profinitely ultimately
periodic.