For a first-order sentence $\varphi$ the spectrum of $\varphi$ is the set of cardinalities of its finite models, i.e. $$\operatorname{spec}(\varphi):=\{n\in\mathbb{N} \mid \text{ There is a model } \mathfrak{A}\models\varphi \text{ with } |\mathfrak{A}|=n\}$$ In the Book "The Classical Decision Problem" by Börger, Grädel and Gurevich we find the statement
It was proved by Ramsey that the spectra of prenex sentences with prefix of form $\exists\dots\exists\forall\dots\forall$ are finite or cofinite.
Is there any reasonably easy/short proof of this result?
Unless I'm missing something, the statement is false in general.
Consider the language consisting of a single unary function symbol $\{f\}$, and the sentence $\varphi$ saying that $f$ partitions the domain into pairs:
$\varphi$ can be written as
$$\forall x\forall y[(f(x)=f(y)\implies x=y)\wedge (f(f(x))=x)\wedge (\neg f(x)=x)].$$
Any model of $\varphi$ can be partitioned into pairs, so spec$(\varphi)$ consists of the even numbers.
(Note that actually the injectivity clause in $\varphi$ is redundant, so we only need a single "$\forall$" to get a counterexample.)
However, the statement is true if we restrict attention to languages with no function symbols.
The key is a preservation theorem: that $\overline{\forall}$-sentences (that is, sentences whose prenex normal form contains only universal quantifiers) are preserved under taking substructures. This is basically immediate from the definition of $\models$ (although note that there are more complicated preservation results down the road).
Now we're interested in sentences "one level up," but the downwards preservation of universal sentences is still useful to us: it tells us that if $\overline{a}$ witnesses $$\varphi\equiv\exists\overline{x}\forall\overline{y}\psi(\overline{x},\overline{y})$$ in $\mathcal{M}$, then any substructure of $\mathcal{M}$ which contains $\overline{a}$ also satisfies $\varphi$.
Since we assumed that our language is relational, any subset of $\mathcal{M}$ is a substructure; so if spec$(\varphi)$ isn't finite, we get models of $\varphi$ of any finite cardinality at least the number of existential quantifiers in $\varphi$ (take a sufficiently large model and cut it down).
(In the above I've implicitly thought of constants as $0$-ary function symbols, so not present in the language. However, they pose no problem to the above argument: just make sure to include them along with the witnessing tuple. It's only function symbols with arity $>0$ which pose a problem.)