# 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) Oct 25, 2015 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)? Oct 26, 2015 at 14:41
• Ok I converted the comment into a short answer. P.S: thanks for the paper :-) Oct 26, 2015 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. Oct 26, 2015 at 17:00
• @MarzioDeBiasi: Why did you delete the answer? Except for the minor dualization problem, it was correct. Oct 26, 2015 at 18:08

## 1 Answer

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 > 0$ constants) for the Monadic Predicate Calculus satisfiablility were established in:

• The linked papers actually suggest the problem is coNEXP-complete. The NEXP-completeness results are for satisfiability rather than validity. Oct 26, 2015 at 15:54
• @EmilJeřábek: thanks! fixed and undeleted Oct 26, 2015 at 19:03