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?


1 Answer 1


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.)

  • $\begingroup$ Thanks. I understand the counterexample and the argument for relational vocabulary. I'm just a little confused because the quotation in the book continues: "To establish this result Ramsey proved his famous combinatorial theorem." If downwards preservation is all there is to it why would he need any combinatorics to prove such a "triviality"? $\endgroup$
    – abc
    Commented May 21, 2018 at 12:33
  • 2
    $\begingroup$ @Achilles The statement in "The Classical Decision Problem" is maybe a little imprecise. As Noah pointed out, it's easy to prove that the spectrum of a sentence in this class is finite or cofinite. What Ramsey used his theorem for was to give a decision procedure for which of these cases holds. $\endgroup$ Commented May 21, 2018 at 14:35

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .