- cc.complexity-theory exp-time-algorithms nexp
- Updated Mon, 20 Jun 2022 11:32:03 GMT

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$.

According to:

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:

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

External links referenced by this document:

- https://complexityzoo.uwaterloo.ca/Complexity_Zoo:N#ne
- http://ieeexplore.ieee.org/xpl/articleDetails.jsp?arnumber=287598
- http://imps.mcmaster.ca/courses/CAS-701-04/presentations/contributions/Wu-monadic-fol.pdf
- http://www.sciencedirect.com/science/article/pii/0022000080900276
- http://www.sciencedirect.com/science/article/pii/0022000080900276/pdf?md5=4eb40650392277bc7a4fdcb33c29e115&pid=1-s2.0-0022000080900276-main.pdf