This question 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 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.

  • 1
    $\begingroup$ 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$. $\endgroup$ – Emil Jeřábek Jul 22 '20 at 18:21
  • $\begingroup$ @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 $\endgroup$ – SagarM Jul 23 '20 at 14:43

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.

  • $\begingroup$ 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 $\endgroup$ – SagarM Jul 23 '20 at 14:41
  • 1
    $\begingroup$ 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. $\endgroup$ – Bartosz Bednarczyk Jul 23 '20 at 14:56
  • $\begingroup$ 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 homes.cs.washington.edu/~suciu/file40_paper.pdf proves the statement about $FO2$ model counting $\endgroup$ – SagarM Jul 23 '20 at 15:56
  • $\begingroup$ 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. $\endgroup$ – SagarM Jul 23 '20 at 15:59
  • 1
    $\begingroup$ 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 $\endgroup$ – Bartosz Bednarczyk Jul 24 '20 at 5:59

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.

  • $\begingroup$ What's FPSPACE? $\endgroup$ – Bartosz Bednarczyk Jul 30 '20 at 12:15
  • 1
    $\begingroup$ 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.) $\endgroup$ – Emil Jeřábek Jul 30 '20 at 12:32
  • $\begingroup$ Thanks a lot :) $\endgroup$ – Bartosz Bednarczyk Jul 30 '20 at 14:25

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.