Complexity of Model Enumeration in function free, equality free, First Order Logic with only Unary Predicates?

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_{iin I}P_i(x)landbigwedge_{jin 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 $Isubseteq A_x$, let $psi_I$ denote the sentence obtained from $psi(x)$ by replacing all occurrences of $alphain I$ with $top$, and all occurrences of $alphain A_xsmallsetminus I$ with $bot$. Then we define $$phi^*=bigvee_{Isubseteq A_x}Bigl[(psi_I)^*landexists x,Bigl(bigwedge_{alphain I}alpha(x)landbigwedge_{alphain A_xsmallsetminus I}negalpha(x)Bigr)Bigr].$$

The soundness of this translation follows from the tautologies $$bigwedge_{alphain I}alpha(x)landbigwedge_{alphain A_xsmallsetminus I}negalpha(x)to(psi(x)leftrightarrowpsi_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 $kle 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)landexists 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 $Mcolon[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_{iin I}P_i(x)landbigwedge_{inotin 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_phisubseteqmathcal P([2^k])$ such that $$Mmodelsphiiffmathrm{Im}(M)in T_phi,$$ and the number of models of $phi$ of size $n$ is $$sum_{Ein T_phi}bigl|{Mcolon[n]to Emid Mtext{ is onto}}bigr| =sum_{Ein T_phi}|E|!,S(n,|E|) =sum_{Ein 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.

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.