7
$\begingroup$

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

$\endgroup$
  • 2
    $\begingroup$ NEXPTIME-complete ?!? (I don't have a .pdf version of the article, yet) $\endgroup$ – Marzio De Biasi Oct 25 '15 at 21:15
  • $\begingroup$ 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)? $\endgroup$ – Dustin Wehr Oct 26 '15 at 14:41
  • $\begingroup$ Ok I converted the comment into a short answer. P.S: thanks for the paper :-) $\endgroup$ – Marzio De Biasi Oct 26 '15 at 15:35
  • $\begingroup$ 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. $\endgroup$ – Marzio De Biasi Oct 26 '15 at 17:00
  • $\begingroup$ @MarzioDeBiasi: Why did you delete the answer? Except for the minor dualization problem, it was correct. $\endgroup$ – Emil Jeřábek Oct 26 '15 at 18:08
3
$\begingroup$

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]

$\endgroup$
  • 3
    $\begingroup$ The linked papers actually suggest the problem is coNEXP-complete. The NEXP-completeness results are for satisfiability rather than validity. $\endgroup$ – Emil Jeřábek Oct 26 '15 at 15:54
  • $\begingroup$ @EmilJeřábek: thanks! fixed and undeleted $\endgroup$ – Marzio De Biasi Oct 26 '15 at 19:03

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.