The separated fragment of First-Order Logic (FOL) is the sublanguage of FOL in which no atomic sub-formula $A(\ldots,x,\ldots,y,\ldots)$ is such that $x$ is bound by and existential quantifier and $y$ is bound by a universal quantifier.
Such fragment is defined and shown decidable in this paper. The authors prove that the fragment has the finite model property, giving also a bound to the size of models which is exponential in the size of the formula.
My question is to find an example of a sentence of the separated fragment with $n$ bound variables whose models are at least of size, say, $2^n$.
Best Answer
Consider the language with $n$ unary predicates $\{P_1,\dots,P_n\}$. Let $\varphi_i(x,y)$ be the formula $$\lnot (P_i(x)\leftrightarrow P_i(y)) \land \bigwedge_{j\neq i} (P_j(x)\leftrightarrow P_j(y)).$$ This formula asserts that $x$ and $y$ disagree on the truth of $P_i$ but agree on the truth of each other $P_j$. Now consider the sentence $\psi$: $$(\exists z\,(z = z)) \land \bigwedge_{i=1}^n \forall x\, \exists y\, \varphi_i(x,y).$$
For any model $M$ of $\psi$ and any subset $X\subseteq \{1,\dots,n\}$, $M$ must contain an element satisfying $P_i$ for all $i\in X$ and $\lnot P_i$ for all $i\notin X$. Indeed, $M$ is nonempty, and starting from any element, you can find elements satisfying any given set of the $P_i$ by applying the clauses $\forall x\, \exists y\, \varphi_i(x,y)$ one at a time to find an element which disagrees about the truth value of a single $P_i$. So $|M| \geq 2^n$.
The length of $\varphi_i$ is $O(n)$, and the length of $\psi$ is $O(n^2)$. So letting $\ell$ be the length of $\psi$, the size of $M$ is $O(2^\ell)$.
This answers the question you asked (though I prefer to measure the complexity of a formula by its length, instead of the number of bound variables). But the bound given in the paper (Theorem 17) is $n$-fold exponential in the length of the formula, where $n$ is the number of alternations of quantifier blocks in prenex normal form. This means $O(2^{2^{\dots ^\ell}})$ where the tower of exponentials has height $n$. I expect coming up with a family of sentences exhibiting that this bound is tight would be much more difficult. And it seems the authors think it might not be tight. They write "Our current upper bound on the size of small models is non-elementary in the length of the formula" (emphasis mine).