I am aware that compactness fails on finite models, but the common counter-example uses models of arbitrary big finite size. So if we bound the size what results can we get?

Assume we have an infinite set of sentences $\Sigma$, of a language of first order logic $\mathcal{L}$. If there is a natural number $n$ such that every finite $S\subset\Sigma$ has a model of size $\leq n$, then does $\Sigma$ have a finite model? How about a model of size $\leq n$?

If the language is finite or there is a $k$ such that every function has at most $k$ arguments and every relation is at most $k$-place, we have finite many structures of size $\leq n$ of $\mathcal{L}$, let's call them $N_1,\ldots,N_m$. If for every $i\leq m$ there exists a finite $S_i\subset\Sigma$ such that $N_i$ doesn't satisfy $S_i$, then $\bigcup_{i\leq m}S_i$ wouldn't have a model of size $\leq n$, and thus we get that one of the models satisfy every sentence of $\Sigma$. Is this argument correct? And what about the general case, where we don't restrict the language whatsoever and the structures are infinite many?


2 Answers 2


For the general case, without any restriction on the language, the Compactness theorem does hold for models having a specified finite size. To see this, argue as follows: suppose that every finite subtheory of $\Sigma$ has a model of finite size at most $n$. Let $\Sigma^+$ be the theory obtained by adding the axiom "there are at most $n$ elements." Notice that every finite subtheory of $\Sigma^+$ is satisfiable. Thus, by the ordinary Compactness theorem, $\Sigma^+$ is satisfiable. Hence, $\Sigma$ has a model of size at most $n$, as desired.


Your argument is correct. In fact, we can axiomatize any finite model, meaning that if ${\mathcal M}=(M,\dots)$ is a model (in a language of arbitrary size) then there is a set of sentences $\Sigma$ such that any model of $\Sigma$ is isomorphic to ${\mathcal M}$:

Say $M=\{a_1,\dots,a_n\}$.

First you say that the universe has size $|M|=n$, with a sentence $\tau$ such as "there are $x_1,\dots,x_n$ which are pairwise different and such that each $y$ is equal to one of them."

For each relational symbol $R$, consider the formula

"there are $x_1,\dots,x_n$ pairwise different and such that $\bigwedge_{R^{\mathcal M}(a_{i_1},\dots,a_{i_k})}R(x_{i_1},\dots,x_{i_k})$ and such that $\bigwedge_{R^{\mathcal M}(a_{i_1},\dots,a_{i_k})\mbox{ fails}}\lnot R(x_{i_1},\dots,x_{i_k})$",

where the first big conjunction ranges over all tuples of elements of $M$ that are in the interpretation of $R$, and the second runs over all tuples that are not in that interpretation. Given any model of this formula of size $n$, there is a bijection between this model and $M$ such that the interpretation of $R$ in this model is just the image under the bijection of the interpretation of $R$ in ${\mathcal M}$. Let $\phi_R$ be the formula such that the sentence we just wrote is $\exists \vec x\phi_R$.

Similarly, there is a sentence $\exists\vec x\psi_f$ describing completely each function $f^{\mathcal M}$, in the same sense as the sentence above completely describes $R^{\mathcal M}$.

$\Sigma$ consists of $\tau$, and the following formulas:

For any finitely many constant symbols $c_1,\dots,c_j$, any finitely many relational symbols $R_1,\dots,R_s$, and any finitely many function symbols $f_1,\dots,f_k$, say that $c_l^{\mathcal M}=a_{i_l}$ for each $l$, the sentence

"$\exists \vec x(\bigwedge_{a=1}^s\phi_{R_a}\land\bigwedge_{b=1}^k\psi_{f_b}\land \bigwedge_{l=1}^j c_l=x_{i_l})$".

Note that if the language is finite, $\Sigma$ is finite as well. But the theory just described uniquely characterizes ${\mathcal M}$ even if the language is infinite.

This result is usually presented as a consequence of Beth’s definability theorem or of Svenonius’s theorem, see for example W. Hodges, Model theory. Cambridge University Press, (1993), Chapter 10.

(I guess this says that there is no useful compactness result for finite models, since the only version that would hold would simply give us a model that we already knew we had.)

  • $\begingroup$ As a side note: I am co-author of a paper ("Defining non-empty small sets from families of finite sets"), where we explore the combinatorics of intersecting families in the context of definability (it is an interesting interplay of finite combinatorics and logic), and at some point we needed to mention what is essentially the result above. $\endgroup$ Dec 29, 2010 at 0:14

You must log in to answer this question.

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