<p>According to:</p>

<p><a href="http://ieeexplore.ieee.org/xpl/articleDetails.jsp?arnumber=287598" rel="noreferrer">Leo Bachmair, Harald Ganzinger, Uwe Waldmann: Set Constraints are the Monadic Class. LICS 1993: 75-83</a></p>

<p>the problem of checking if a formula of the Monadic Predicate Calculus is <em>satisfiable</em> is NEXPTIME-complete. So your problem (formula <em>validity</em>) is coNEXPTIME-complete.</p>

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

<p><a href="http://www.sciencedirect.com/science/article/pii/0022000080900276" rel="noreferrer">Harry R. Lewis: Complexity Results for Classes of Quantificational Formulas. J. Comput. Syst. Sci. 21(3): 317-353 (1980)</a> [<a href="http://www.sciencedirect.com/science/article/pii/0022000080900276/pdf?md5=4eb40650392277bc7a4fdcb33c29e115&amp;pid=1-s2.0-0022000080900276-main.pdf" rel="noreferrer">pdf download</a>]</p>

CC BY-SA 3.0
2015-10-26T15:54:12.270Z
The linked papers actually suggest the problem is coNEXP-complete. The NEXP-completeness results are for satisfiability rather than validity.
Emil Jeřábek
CC BY-SA 3.0
2015-10-26T19:03:51.113Z
@EmilJeřábek: thanks! fixed and undeleted
Marzio De Biasi
CC BY-SA 3.0
2015-10-26T15:34:49.330Z
2015-10-26T18:33:04.030Z
2015-10-26T18:33:04.030Z
Marzio De Biasi
<p>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 <a href="https://complexityzoo.uwaterloo.ca/Complexity_Zoo:N#ne">NE</a> is closed under).</p>

<p>According to <a href="http://imps.mcmaster.ca/courses/CAS-701-04/presentations/contributions/Wu-monadic-fol.pdf">this presentation</a>, 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$. </p>

CC BY-SA 3.0
2015-10-25T21:15:39.737Z
[NEXPTIME-complete](https://people.mpi-inf.mpg.de/~uwe/paper/LICS93-bibl.html) ?!? (I don't have a .pdf version of the article, yet)
Marzio De Biasi
CC BY-SA 3.0
2015-10-26T14:41:33.583Z
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: http://www.cs.toronto.edu/~wehr/Set%20Constraints%20are%20the%20Monadic%20Class.pdf
Do you want to answer this question (for points or whatever... I'm new to this)?
Dustin Wehr
CC BY-SA 3.0
2015-10-26T15:35:31.410Z
Ok I converted the comment into a short answer. P.S: thanks for the paper :-)
Marzio De Biasi
CC BY-SA 3.0
2015-10-26T17:00:50.707Z
As noticed by @EmilJeřábek in the comment of my deleted answer, the linked paper (and [the Lewis' one](http://www.sciencedirect.com/science/article/pii/0022000080900276)) 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
CC BY-SA 3.0
2015-10-26T18:08:31.323Z
@MarzioDeBiasi: Why did you delete the answer? Except for the minor dualization problem, it was correct.
Emil Jeřábek
CC BY-SA 3.0
2015-10-26T19:04:21.783Z
@EmilJeřábek: because I also didn't remember the current status about the large "ship cargos" EXP/NEXP/coNEXP ... :-) ... after a quick visit to the zoo I see strange things I didn't know like coNEXP \subseteq NEXP/poly :-D
Marzio De Biasi
<cc.complexity-theory><exp-time-algorithms><nexp>
Complexity of validity problem for Monadic First Order Logic?
Dustin Wehr
# Complexity of validity problem for Monadic First Order Logic?

(Asked by: username_0 on 2015-10-25)

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](https://complexityzoo.uwaterloo.ca/Complexity_Zoo:N#ne) is closed under).

According to [this presentation](http://imps.mcmaster.ca/courses/CAS-701-04/presentations/contributions/Wu-monadic-fol.pdf), 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$.

**Tags:** cc.complexity-theory, exp-time-algorithms, nexp

> **Comments:**
> **username_1**: [NEXPTIME-complete](https://people.mpi-inf.mpg.de/~uwe/paper/LICS93-bibl.html) ?!? (I don't have a .pdf version of the article, yet)  
> **username_0**: 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: http://www.cs.toronto.edu/~wehr/Set%20Constraints%20are%20the%20Monadic%20Class.pdf Do you want to answer this question (for points or whatever... I'm new to this)?  
> **username_1**: Ok I converted the comment into a short answer. P.S: thanks for the paper :-)  
> **username_1**: As noticed by @EmilJeřábek in the comment of my deleted answer, the linked paper (and [the Lewis' one](http://www.sciencedirect.com/science/article/pii/0022000080900276)) 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.  
> **username_2**: @MarzioDeBiasi: Why did you delete the answer? Except for the minor dualization problem, it was correct.  
> **username_1**: @EmilJeřábek: because I also didn't remember the current status about the large "ship cargos" EXP/NEXP/coNEXP ... :-) ... after a quick visit to the zoo I see strange things I didn't know like coNEXP \subseteq NEXP/poly :-D  

---

## 1 answers

### Answer by username_1 on 2015-10-26. Score: 5 | Accepted answer

According to:

[Leo Bachmair, Harald Ganzinger, Uwe Waldmann: Set Constraints are the Monadic Class. LICS 1993: 75-83](http://ieeexplore.ieee.org/xpl/articleDetails.jsp?arnumber=287598)

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)](http://www.sciencedirect.com/science/article/pii/0022000080900276) [[pdf download](http://www.sciencedirect.com/science/article/pii/0022000080900276/pdf?md5=4eb40650392277bc7a4fdcb33c29e115&pid=1-s2.0-0022000080900276-main.pdf)]

> **Comments:**
> **username_2**: The linked papers actually suggest the problem is coNEXP-complete. The NEXP-completeness results are for satisfiability rather than validity.  
> **username_1**: @EmilJeřábek: thanks! fixed and undeleted  

---

