MONADIC LOGICAL DEFINABILITY OF NONDETERMINISTIC LINEAR-TIME

We answer a question asked by J. F. Lynch by proving that existential monadic second-order logic with addition captures not only the class N TIME(n) but also the class NLIN (i.e., linear time on nondeterministic RAMs), so enlarging considerably the set of natural problems expressi ble in this logic, since most combinatorial NP-complete problems belon g to NLIN. Moreover, our result still holds if the first-order part of the formulas is required to be For AllThere Exists*, so improving th e recent similar result by J. F. Lynch about NTIME(n). In addition, we explicitly state that a graph problem is recognizable in nondetermini stic linear time O(n+e) (where n, and e are the numbers of vertices an d edges, respectively) if and only if it can be defined in existential second-order logic with unary functions and only one variable on the vertices-edges domain.