First-order formulas with exponentially large models 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$.
 A: 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). 
A: Consider $2n$ one-place predicate symbols $B_{1,0}, \ldots, B_{n,0}$ and $B_{1,1}, \ldots, B_{n,1}$. The intended meaning of $B_{i,j}(x)$ is ``the binary string $x$ has a bit of value $j$ in position $i$. For convenience bits are numbered from right to left.
There exists a string made of $n$ zerores: 


*

*$(\exists x) \bigwedge_{i=1}^n B_{i,0}(x)$
Each bit of every string contains either a zero or a one but not both:


*$(\forall x)(\bigwedge_{i=1}^n B_{i,0}(x) \leftrightarrow \neg B_{i,1}(x))$
Define 
$$
\varphi_{k}(x) \equiv 
\begin{cases}
B_{1,0}(x) & \text{if } k = 1 \\
B_{k,0}(x) \wedge \bigwedge_{i=1}^{k-1} B_{i,1}(x) & \text{if } 1 < k \leq n 
\end{cases}
$$
The formula $\varphi_{k}(x)$ should be read as ``the $k$-th bit of the string $x$ is 0 and all the bits to its right are 1".
Define 
$$
\zeta_{k}(x) \equiv 
\begin{cases}
B_{1,1}(x) & \text{if } k = 1 \\
B_{k,1}(x) \wedge \bigwedge_{i=1}^{k-1} B_{i,0}(x) & \text{if } 1 < k \leq n 
\end{cases}
$$
The formula $\zeta_{k}(x)$ should be read as ``the $k$-th bit of the string $x$ is 1 and all the bits to its right are 0".
Define 
$$
\psi_{s,t}(x,y) \equiv 
\begin{cases}
\bigwedge_{i=s}^{t} B_{i,0}(x)\leftrightarrow B_{i,0}(y) & \text{if } s \leq t \\
\top & \text{otherwise}
\end{cases}
$$
The formula $\psi_{s,t}(x,y)$ should be read as ``the bits from position $s$ to position $t$ included of the strings $x$ and $y$ coincide".
For every binary string $x$ there exists the binary string $y = x +1$: 


*$\bigwedge_{k=1}^n (\forall x)(\varphi_{k}(x) \to (\exists y)\zeta_{k}(x) \wedge \psi_{k+1,n}(x,y) )$
The conjunction of formulas 1, 2, and 3 should force a model to contain all $2^n$ binary strings of bits. 
Maybe this construction can be ``nested" forcing models to be sets of binary strings each one of length  ${2^n}$ but right now I don't know how to keep a polynomially sized vocabulary.
