<p>Answering your second question, the logic you mean is known as Monadic FO or Monadic Predicate Calculus. It is known the logic is equivalent to FO1 (as  Emil Jeřábek suggested) by some very old works by Behmann and Loewenheim.</p>
<p>Regarding the first question, I do not know what is the complexity of model enumeration, but satisfiability checking is NExpTime-complete (check &quot;The Classical Decision Problem&quot; book), while the satisfiability problem for FO1 is NP-complete. Hence, even if the model enumeration is in P for 2-variable logic (a superset of FO1) it does not imply that the same bound holds for MFO, since the translation from MFO to FO1 might require an exponential blowup in the size of an input formula.</p>

CC BY-SA 4.0
2020-07-23T14:41:45.947Z
actually the reduction of monadic predicate calculus to FO1 is enough to know that model enumeration for this can be done in polynomial time. As FO1 is a subset of FO2, for which model counting is in P
SagarM
CC BY-SA 4.0
2020-07-23T14:56:14.047Z
But note that translation from Monadic FO to FO1 can be exponential (Sat for FO1 is known to be NP-complete). So I'm not sure if the P upper bound for model counting holds.
Bartosz Bednarczyk
CC BY-SA 4.0
2020-07-23T15:56:47.007Z
That intrigues me again. I am sorry I am Physicist trying to understand CS. In simple words my problems is that I have a FOL theory with only unary predicates and arbitrary number of variables, and then I have $n$ domain elements. Now, we know that for an FO2 theory with $n$ domain elements the model count can be done in some time which is only a polynomial of $n$. Now what would be a similar result for FOL with unary predicates and arbitrary number of variables ? For reference https://homes.cs.washington.edu/~suciu/file40_paper.pdf  proves the statement about $FO2$ model counting
SagarM
CC BY-SA 4.0
2020-07-23T15:59:41.483Z
Your statement "Sat for FO1 is known to be NP-complete" contradicts my understanding of the model counting result. If SAT for FO1 takes exponential time in domain elements then definitely the model counting for FO2 cannot be done in polynomial time.
SagarM
CC BY-SA 4.0
2020-07-23T17:31:55.030Z
In the satisfiability problem, you take as an input a formula and ask if it is satisfiable. The satisfiability problem for FO1 is NP-complete, i.e. it can be solved in non-deterministic polynomial time in the size of the input formula.  Analogously, satisfiability for MFO is NExp-complete, thus it can be solved in non-deterministic exponential time in the size of the input formula. So you do yet have a model to measure it, you are asking if it exists. I hope that what I wrote is clear for you. If not, please ask.
Bartosz Bednarczyk
CC BY-SA 4.0
2020-07-23T17:35:11.583Z
You wrote that "is only polynomial in n". Is the formula part of your input? If yes, then the naive algorithm gives you ExpTime upper bound, since the translation from MFO to FO1 might require exp blowup. If not, then you get PTime algorithm for free (i.e. from the fact that MFO = FO1 in terms of expressive power).
Bartosz Bednarczyk
CC BY-SA 4.0
2020-07-23T20:58:07.090Z
thanks alot, I have learnt alot from this. If you would allow me one last question, Do you know of any applications where monadic predicate calculus is used with many variables and translating to FO1 is prohibitive ? Many thanks :D
SagarM
CC BY-SA 4.0
2020-07-24T05:59:27.267Z
I don't know. It could be that in some practical applications you do not need to translate the formula into fo1 and you reason on it directly to get speedup. But I really don't have any evidences and Im not a big fun of practical applications of logic
Bartosz Bednarczyk
CC BY-SA 4.0
2020-07-23T14:13:30.190Z
2020-07-24T07:14:38.007Z
2020-07-24T07:14:38.007Z
Bartosz Bednarczyk
<p>Reading the discussion below the other answer made me realize that it’s not immediately obvious what is the complexity of translation of FO sentences in this language to equivalent FO1 sentences. While the quoted fact that satisfiability of these sentences is NEXP-complete (whereas satisfiability of FO1 sentences is in NP) implies that any such translation has an <em>at least exponential</em> blow-up, common methods establishing the collapse of FO to FO1 only give a <em>doubly exponential</em> upper bound: any sentence is equivalent to a boolean combination of sentences of the form <span class="math-container">$\exists x\,\bigl(\bigwedge_{i\in I}P_i(x)\land\bigwedge_{j\in J}\neg P_j(x)\bigr)$</span>; there are <span class="math-container">$2^n$</span> such existential sentences, hence their boolean combinations may have size <span class="math-container">$\approx2^{2^n}$</span>.</p>
<p>So, let me show that one <em>can</em> perform the translation in time <span class="math-container">$2^{O(n)}$</span> after all. I will work more generally with any FO language without equality using at most unary symbols (relations and functions, including constants).</p>
<p>Given an FO sentence <span class="math-container">$\phi$</span>, we first rewrite it so that no variable is quantified more than once, and then we construct an equivalent FO1 sentence <span class="math-container">$\phi^*$</span> by induction on the complexity of <span class="math-container">$\phi$</span>:</p>
<ul>
<li><p>If <span class="math-container">$\phi$</span> is quantifier-free, <span class="math-container">$\phi^*=\phi$</span>.</p>
</li>
<li><p>If <span class="math-container">$\phi$</span> is a boolean combination of <span class="math-container">$\phi_0,\dots,\phi_{n-1}$</span>, we make <span class="math-container">$\phi^*$</span> the corresponding boolean combination of <span class="math-container">$\phi_0^*,\dots,\phi_{n-1}^*$</span>.</p>
</li>
<li><p>If <span class="math-container">$\phi=\exists x\,\psi(x)$</span>, let <span class="math-container">$A_x$</span> be the set of all atomic subformulas of <span class="math-container">$\psi$</span> that contain <span class="math-container">$x$</span> (and therefore no other variable). For each <span class="math-container">$I\subseteq A_x$</span>, let <span class="math-container">$\psi_I$</span> denote the sentence obtained from <span class="math-container">$\psi(x)$</span> by replacing all occurrences of <span class="math-container">$\alpha\in I$</span> with <span class="math-container">$\top$</span>, and all occurrences of <span class="math-container">$\alpha\in A_x\smallsetminus I$</span> with <span class="math-container">$\bot$</span>. Then we define
<span class="math-container">$$\phi^*=\bigvee_{I\subseteq A_x}\Bigl[(\psi_I)^*\land\exists x\,\Bigl(\bigwedge_{\alpha\in I}\alpha(x)\land\bigwedge_{\alpha\in A_x\smallsetminus I}\neg\alpha(x)\Bigr)\Bigr].$$</span></p>
</li>
</ul>
<p>The soundness of this translation follows from the tautologies
<span class="math-container">$$\bigwedge_{\alpha\in I}\alpha(x)\land\bigwedge_{\alpha\in A_x\smallsetminus I}\neg\alpha(x)\to(\psi(x)\leftrightarrow\psi_I).$$</span></p>
<p>Let <span class="math-container">$n=|\phi|$</span>. Since we expanded each quantifier to a disjunction of <span class="math-container">$2^n$</span> formulas, the size of the formula is roughly multiplied by <span class="math-container">$2^n$</span> for each quantifier, giving a total size about <span class="math-container">$2^{n^2}$</span>. But counting more precisely, the expansion of <span class="math-container">$\exists x$</span> multiplied the size by <span class="math-container">$2^{|A_x|}$</span>; since each element of <span class="math-container">$A_x$</span> is an atomic subformula of the original formula, and distinct quantifiers correspond to disjoint sets <span class="math-container">$A_x$</span> by our assumption on quantified variables, the overall multiplicative factor is only <span class="math-container">$2^{\sum_x|A_x|}\le2^n$</span>, thus <span class="math-container">$|\phi^*|=2^{O(n)}$</span>, and it is easy to see that it is computable in time polynomial in <span class="math-container">$|\phi^*|$</span>.</p>
<p>One can also show using a similar argument that given an FO sentence <em>with</em> equality in a language with unary predicates and constants, we can compute in time <span class="math-container">$2^{O(n)}$</span> an equivalent sentence that is a boolean combination of sentences of the form <span class="math-container">$\exists^{\ge k}x\,\theta(x)$</span>, where <span class="math-container">$\theta$</span> is a conjunction of atomic and negated atomic formulas, and <span class="math-container">$k\le n$</span>.</p>
<hr />
<p>Concerning the model enumeration problem: I assume the problem is, given a sentence <span class="math-container">$\phi$</span> and a number <span class="math-container">$n$</span> in unary, count the number of models of <span class="math-container">$\phi$</span> with domain <span class="math-container">$[n]$</span>, but it is not clear to me if you want <span class="math-container">$\phi$</span> to be fixed, or to be part of the input.</p>
<p>If <span class="math-container">$\phi$</span> is <em>part of the input</em>, the problem is in PSPACE (more precisely, FPSPACE) by the brute force enumeration algorithm (this works for arbitrary FO languages). Conversely, it is PSPACE-hard even if <span class="math-container">$n=2$</span> is fixed, and the language consists of a single unary predicate: indeed, a QBF
<span class="math-container">$$Q_0p_0\,Q_1p_1\,\dots\,Q_mp_m\,\theta(p_0,\dots,p_m)$$</span>
is true iff the sentence
<span class="math-container">$$\exists x\,P(x)\land\exists x\,\neg P(x)\land Q_0x_0\,Q_1x_1\,\dots\,Q_mx_m\,\theta(P(x_0),\dots,P(x_m))$$</span>
has a model (of size <span class="math-container">$2$</span>).</p>
<p>If <span class="math-container">$\phi$</span> <em>is fixed</em>, the enumeration problem is solvable in polynomial time, and even in <span class="math-container">$\mathrm{TC}^0$</span>: in fact, the number of models of size <span class="math-container">$n$</span> is
<span class="math-container">$$\sum_{i=0}^Kc_ii^n$$</span>
for some integer constants <span class="math-container">$K$</span> and <span class="math-container">$c_0,\dots,c_K$</span> determined by <span class="math-container">$\phi$</span>. To see this, a model with <span class="math-container">$k$</span> unary predicates on domain <span class="math-container">$[n]$</span> can be identified with a mapping <span class="math-container">$M\colon[n]\to[2^k]$</span>, assigning to each element the bitstring stating which unary predicates it satisfies. The truth of a sentence <span class="math-container">$\exists x\,\bigl(\bigwedge_{i\in I}P_i(x)\land\bigwedge_{i\notin I}\neg P_i(x)\bigr)$</span> in <span class="math-container">$M$</span> is then determined by the presence of the corresponding bitstring in <span class="math-container">$\mathrm{Im}(M)$</span>. Thus, there is a set <span class="math-container">$T_\phi\subseteq\mathcal P([2^k])$</span> such that
<span class="math-container">$$M\models\phi\iff\mathrm{Im}(M)\in T_\phi,$$</span>
and the number of models of <span class="math-container">$\phi$</span> of size <span class="math-container">$n$</span> is
<span class="math-container">$$\sum_{E\in T_\phi}\bigl|\{M\colon[n]\to E\mid M\text{ is onto}\}\bigr|
=\sum_{E\in T_\phi}|E|!\,S(n,|E|)
=\sum_{E\in T_\phi}\sum_{i=0}^{|E|}\binom{|E|}i(-1)^{|E|-i}i^n$$</span>
where <span class="math-container">$S(n,k)$</span> are Stirling numbers of the second kind.</p>

CC BY-SA 4.0
2020-07-30T12:15:27.063Z
What's FPSPACE?
Bartosz Bednarczyk
CC BY-SA 4.0
2020-07-30T12:32:25.477Z
The class of functions computable in polynomial space. (Usually, the output tape does not count towards the space bound, but here it doesn’t matter as the output has polynomially bounded length anyway.)
Emil Jeřábek
CC BY-SA 4.0
2020-07-30T14:25:31.933Z
Thanks a lot :)
Bartosz Bednarczyk
CC BY-SA 4.0
2020-07-24T13:14:10.727Z
2020-07-24T15:53:37.593Z
2020-07-24T15:53:37.593Z
Emil Jeřábek
<p>This <a href="https://cstheory.stackexchange.com/q/32895/52564">question</a> has inspired the following two questions.
Given a first order logic language, with only unary predicates, finite number of variables, <span class="math-container">$\forall$</span> and <span class="math-container">$\exists$</span> i.e no equality and functions.</p>
<ul>
<li>what is the complexity class of model enumeration in monadic first order logic ?</li>
<li>How expressive is this language, are there sentences in this language which cannot be expressed in function-free, equality free fragment of  <span class="math-container">$FO^{2}$</span>  ?</li>
</ul>
<p>I have asked a similar (but not the same) question <a href="https://math.stackexchange.com/a/3765728/142677">here</a> but after reading the linked question, I felt TCS-SE was probably a better choice for this question. And I did not delete it because it has an upvoted answer.</p>

CC BY-SA 4.0
2020-07-22T18:21:50.477Z
The only sentences expressible in this language are boolean combinations of sentences of the form $\exists x\,\bigl(\bigwedge_{i\in I}P_i(x)\land\bigwedge_{i\notin I}\neg P_i(x)\bigr)$. So it even collapses to $FO^1$.
Emil Jeřábek
CC BY-SA 4.0
2020-07-23T14:43:54.000Z
@EmilJeřábek, you may put it as an answer and I will accept it, as you were first and your comment asnwers both my problems. As $FO^{1}$ is a subset of $FO2$ for which counting is in P
SagarM
<counting-complexity><first-order-logic>
Complexity of Model Enumeration in function free, equality free, First Order Logic with only Unary Predicates?
SagarM
# Complexity of Model Enumeration in function free, equality free, First Order Logic with only Unary Predicates?

(Asked by: username_0 on 2020-07-22)

This [question](https://cstheory.stackexchange.com/q/32895/52564) has inspired the following two questions.
Given a first order logic language, with only unary predicates, finite number of variables, $\forall$ and $\exists$ i.e no equality and functions.

* what is the complexity class of model enumeration in monadic first order logic ?
* How expressive is this language, are there sentences in this language which cannot be expressed in function-free, equality free fragment of $FO^{2}$ ?

I have asked a similar (but not the same) question [here](https://math.stackexchange.com/a/3765728/142677) but after reading the linked question, I felt TCS-SE was probably a better choice for this question. And I did not delete it because it has an upvoted answer.

**Tags:** counting-complexity, first-order-logic
> **Comments:**
> **username_1**: The only sentences expressible in this language are boolean combinations of sentences of the form $\exists x\,\bigl(\bigwedge_{i\in I}P_i(x)\land\bigwedge_{i\notin I}\neg P_i(x)\bigr)$. So it even collapses to $FO^1$.  
> **username_0**: @EmilJeřábek, you may put it as an answer and I will accept it, as you were first and your comment asnwers both my problems. As $FO^{1}$ is a subset of $FO2$ for which counting is in P  

---

## 2 answers

### Answer by username_2 on 2020-07-23. Score: 1 | Accepted answer

Answering your second question, the logic you mean is known as Monadic FO or Monadic Predicate Calculus. It is known the logic is equivalent to FO1 (as Emil Jeřábek suggested) by some very old works by Behmann and Loewenheim.

Regarding the first question, I do not know what is the complexity of model enumeration, but satisfiability checking is NExpTime-complete (check "The Classical Decision Problem" book), while the satisfiability problem for FO1 is NP-complete. Hence, even if the model enumeration is in P for 2-variable logic (a superset of FO1) it does not imply that the same bound holds for MFO, since the translation from MFO to FO1 might require an exponential blowup in the size of an input formula.

> **Comments:**
> **username_0**: actually the reduction of monadic predicate calculus to FO1 is enough to know that model enumeration for this can be done in polynomial time. As FO1 is a subset of FO2, for which model counting is in P  
> **username_2**: But note that translation from Monadic FO to FO1 can be exponential (Sat for FO1 is known to be NP-complete). So I'm not sure if the P upper bound for model counting holds.  
> **username_0**: That intrigues me again. I am sorry I am Physicist trying to understand CS. In simple words my problems is that I have a FOL theory with only unary predicates and arbitrary number of variables, and then I have $n$ domain elements. Now, we know that for an FO2 theory with $n$ domain elements the model count can be done in some time which is only a polynomial of $n$. Now what would be a similar result for FOL with unary predicates and arbitrary number of variables ? For reference https://homes.cs.washington.edu/~suciu/file40_paper.pdf  proves the statement about $FO2$ model counting  
> **username_0**: Your statement "Sat for FO1 is known to be NP-complete" contradicts my understanding of the model counting result. If SAT for FO1 takes exponential time in domain elements then definitely the model counting for FO2 cannot be done in polynomial time.  
> **username_2**: In the satisfiability problem, you take as an input a formula and ask if it is satisfiable. The satisfiability problem for FO1 is NP-complete, i.e. it can be solved in non-deterministic polynomial time in the size of the input formula.  Analogously, satisfiability for MFO is NExp-complete, thus it can be solved in non-deterministic exponential time in the size of the input formula. So you do yet have a model to measure it, you are asking if it exists. I hope that what I wrote is clear for you. If not, please ask.  
> **username_2**: You wrote that "is only polynomial in n". Is the formula part of your input? If yes, then the naive algorithm gives you ExpTime upper bound, since the translation from MFO to FO1 might require exp blowup. If not, then you get PTime algorithm for free (i.e. from the fact that MFO = FO1 in terms of expressive power).  
> **username_0**: thanks alot, I have learnt alot from this. If you would allow me one last question, Do you know of any applications where monadic predicate calculus is used with many variables and translating to FO1 is prohibitive ? Many thanks :D  
> **username_2**: I don't know. It could be that in some practical applications you do not need to translate the formula into fo1 and you reason on it directly to get speedup. But I really don't have any evidences and Im not a big fun of practical applications of logic  

---

### Answer by username_1 on 2020-07-24. Score: 2

Reading the discussion below the other answer made me realize that it’s not immediately obvious what is the complexity of translation of FO sentences in this language to equivalent FO1 sentences. While the quoted fact that satisfiability of these sentences is NEXP-complete (whereas satisfiability of FO1 sentences is in NP) implies that any such translation has an *at least exponential* blow-up, common methods establishing the collapse of FO to FO1 only give a *doubly exponential* upper bound: any sentence is equivalent to a boolean combination of sentences of the form $\exists x\,\bigl(\bigwedge\_{i\in I}P\_i(x)\land\bigwedge\_{j\in J}\neg P\_j(x)\bigr)$; there are $2^n$ such existential sentences, hence their boolean combinations may have size $\approx2^{2^n}$.

So, let me show that one *can* perform the translation in time $2^{O(n)}$ after all. I will work more generally with any FO language without equality using at most unary symbols (relations and functions, including constants).

Given an FO sentence $\phi$, we first rewrite it so that no variable is quantified more than once, and then we construct an equivalent FO1 sentence $\phi^\*$ by induction on the complexity of $\phi$:

* If $\phi$ is quantifier-free, $\phi^\*=\phi$.
* If $\phi$ is a boolean combination of $\phi\_0,\dots,\phi\_{n-1}$, we make $\phi^\*$ the corresponding boolean combination of $\phi\_0^\*,\dots,\phi\_{n-1}^\*$.
* If $\phi=\exists x\,\psi(x)$, let $A\_x$ be the set of all atomic subformulas of $\psi$ that contain $x$ (and therefore no other variable). For each $I\subseteq A\_x$, let $\psi\_I$ denote the sentence obtained from $\psi(x)$ by replacing all occurrences of $\alpha\in I$ with $\top$, and all occurrences of $\alpha\in A\_x\smallsetminus I$ with $\bot$. Then we define
  $$\phi^\*=\bigvee\_{I\subseteq A\_x}\Bigl[(\psi\_I)^\*\land\exists x\,\Bigl(\bigwedge\_{\alpha\in I}\alpha(x)\land\bigwedge\_{\alpha\in A\_x\smallsetminus I}\neg\alpha(x)\Bigr)\Bigr].$$

The soundness of this translation follows from the tautologies
$$\bigwedge\_{\alpha\in I}\alpha(x)\land\bigwedge\_{\alpha\in A\_x\smallsetminus I}\neg\alpha(x)\to(\psi(x)\leftrightarrow\psi\_I).$$

Let $n=|\phi|$. Since we expanded each quantifier to a disjunction of $2^n$ formulas, the size of the formula is roughly multiplied by $2^n$ for each quantifier, giving a total size about $2^{n^2}$. But counting more precisely, the expansion of $\exists x$ multiplied the size by $2^{|A\_x|}$; since each element of $A\_x$ is an atomic subformula of the original formula, and distinct quantifiers correspond to disjoint sets $A\_x$ by our assumption on quantified variables, the overall multiplicative factor is only $2^{\sum\_x|A\_x|}\le2^n$, thus $|\phi^\*|=2^{O(n)}$, and it is easy to see that it is computable in time polynomial in $|\phi^\*|$.

One can also show using a similar argument that given an FO sentence *with* equality in a language with unary predicates and constants, we can compute in time $2^{O(n)}$ an equivalent sentence that is a boolean combination of sentences of the form $\exists^{\ge k}x\,\theta(x)$, where $\theta$ is a conjunction of atomic and negated atomic formulas, and $k\le n$.

---

Concerning the model enumeration problem: I assume the problem is, given a sentence $\phi$ and a number $n$ in unary, count the number of models of $\phi$ with domain $[n]$, but it is not clear to me if you want $\phi$ to be fixed, or to be part of the input.

If $\phi$ is *part of the input*, the problem is in PSPACE (more precisely, FPSPACE) by the brute force enumeration algorithm (this works for arbitrary FO languages). Conversely, it is PSPACE-hard even if $n=2$ is fixed, and the language consists of a single unary predicate: indeed, a QBF
$$Q\_0p\_0\,Q\_1p\_1\,\dots\,Q\_mp\_m\,\theta(p\_0,\dots,p\_m)$$
is true iff the sentence
$$\exists x\,P(x)\land\exists x\,\neg P(x)\land Q\_0x\_0\,Q\_1x\_1\,\dots\,Q\_mx\_m\,\theta(P(x\_0),\dots,P(x\_m))$$
has a model (of size $2$).

If $\phi$ *is fixed*, the enumeration problem is solvable in polynomial time, and even in $\mathrm{TC}^0$: in fact, the number of models of size $n$ is
$$\sum\_{i=0}^Kc\_ii^n$$
for some integer constants $K$ and $c\_0,\dots,c\_K$ determined by $\phi$. To see this, a model with $k$ unary predicates on domain $[n]$ can be identified with a mapping $M\colon[n]\to[2^k]$, assigning to each element the bitstring stating which unary predicates it satisfies. The truth of a sentence $\exists x\,\bigl(\bigwedge\_{i\in I}P\_i(x)\land\bigwedge\_{i\notin I}\neg P\_i(x)\bigr)$ in $M$ is then determined by the presence of the corresponding bitstring in $\mathrm{Im}(M)$. Thus, there is a set $T\_\phi\subseteq\mathcal P([2^k])$ such that
$$M\models\phi\iff\mathrm{Im}(M)\in T\_\phi,$$
and the number of models of $\phi$ of size $n$ is
$$\sum\_{E\in T\_\phi}\bigl|\{M\colon[n]\to E\mid M\text{ is onto}\}\bigr|
=\sum\_{E\in T\_\phi}|E|!\,S(n,|E|)
=\sum\_{E\in T\_\phi}\sum\_{i=0}^{|E|}\binom{|E|}i(-1)^{|E|-i}i^n$$
where $S(n,k)$ are Stirling numbers of the second kind.

> **Comments:**
> **username_2**: What's FPSPACE?  
> **username_1**: The class of functions computable in polynomial space. (Usually, the output tape does not count towards the space bound, but here it doesn’t matter as the output has polynomially bounded length anyway.)  
> **username_2**: Thanks a lot :)  

---

