# Complexity of validity problem for Monadic First Order Logic?

Monadic First Order Logic is FOL with no function symbols, and predicate symbols restricted to arity 1. For this question, let's say that the = symbol is also forbidden. I want to know the complexity of determining if a monadic FOL sentence is valid, ideally in the form of a completeness result (say, under some notion of reduction that the class NE is closed under).

According to this presentation, it was proved a century ago that if S is a satisfiable monadic FOL sentence, then S has a model of size at most $2^kr$, where $r$ is the number of variables and $k$ is the number of predicate symbols. From that it follows that the problem is in $NTIME(2^{n^2})$ and $SPACE(2^n)$: First, guess a (respectively, try every) structure of size $\leq 2^k r \leq 2^n n$. Then evaluate the sentence on that structure in the most straightforward deterministic way, by enumerating all the elements of the structure at every quantifier, and evaluating the quantifier-free parts of the sentence in polynomial time. That takes time $(2^n n)^r poly(n)$, which is in $O(2^{n^2})$. On the other side, it is easy to show that the problem is hard for $PSPACE$.

• NEXPTIME-complete ?!? (I don't have a .pdf version of the article, yet) – Marzio De Biasi Oct 25 '15 at 21:15
• Thanks @MarzioDeBiasi! NEXPTIME-complete is correct, and the problem is in NE. Here's the paper, which answers my question and many more on pages 5-6: cs.toronto.edu/~wehr/… Do you want to answer this question (for points or whatever... I'm new to this)? – Dustin Wehr Oct 26 '15 at 14:41
• Ok I converted the comment into a short answer. P.S: thanks for the paper :-) – Marzio De Biasi Oct 26 '15 at 15:35
• As noticed by @EmilJeřábek in the comment of my deleted answer, the linked paper (and the Lewis' one) are about satisfiability, but you ask for validity, i.e. true under every interpretation (I absolutely didn't pay attention to it), so the problem is coNEXP-complete. – Marzio De Biasi Oct 26 '15 at 17:00
• @MarzioDeBiasi: Why did you delete the answer? Except for the minor dualization problem, it was correct. – Emil Jeřábek Oct 26 '15 at 18:08

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