Complexity of validity problem for Monadic First Order Logic?
According to:

Leo Bachmair, Harald Ganzinger, Uwe Waldmann: Set Constraints are the Monadic Class. LICS 1993: 75-83

the problem of checking if a formula of the Monadic Predicate Calculus is satisfiable is NEXPTIME-complete. So your problem (formula validity) is coNEXPTIME-complete.

As cited in the paper, the $NTIME(c^{n / \log n })$ upper and lower bounds  (using different $c &gt; 0$ constants) for the Monadic Predicate Calculus satisfiablility were established in:

Harry R. Lewis: Complexity Results for Classes of Quantificational Formulas. J. Comput. Syst. Sci. 21(3): 317-353 (1980) [pdf download]