The Church problem for expansions of \((\mathbb{N},<)\) by unary predicates (Q690498)

For a two-variable formula \(B(X,Y)\) of the monadic logic of order (MLO), Church's synthesis problem concerns the existence and construction of a finite-state operator \(Y=F(X)\) such that \(B(X,F(X))\) is universally valid over \((\mathbb N,<)\). In this version of the problem, \(B\) and \(F\) contain as a parameter a unary predicate \(P\). A large class of predicates \(P\) is exhibited such that Church's problem with parameter \(P\) is decidable. Those \(P\) are increasing recursive \(\omega\)-sequences of integers which are effectively sparse and effectively ultimately reducible (the latter notions, which are defined in the paper, are very natural).