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

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


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:

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

Comments (2)

  • +3 – 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  
  • +0 – @EmilJeábek: thanks! fixed and undeleted — Oct 26, 2015 at 19:03