Lindström's theorem

Remarks

The proof argues by contradiction with Ehrenfeucht–Fraïssé games. If an $\mathcal{L}$-sentence $\varphi$ is not first-order, then for each $n$ there are structures $\mathcal{A}_n \models \varphi$ and $\mathcal{B}_n \models \neg\varphi$ that satisfy the same first-order sentences of quantifier depth $n$. Compactness and the Löwenheim–Skolem property, applied to an $\mathcal{L}$-sentence coding these pairs and partial isomorphisms between them, give countable $\mathcal{A} \models \varphi$ and $\mathcal{B} \models \neg\varphi$ with a back-and-forth system. Then $\mathcal{A} \cong \mathcal{B}$, which contradicts $\mathcal{A} \models \varphi$ and $\mathcal{B} \models \neg\varphi$.

Example: second-order logic is a regular extension of first-order logic that is not equivalent to it. By the theorem, it must lack the compactness theorem or the Löwenheim–Skolem theorem; in fact it lacks both. The infinitary logic $L_{\omega_1\omega}$ has the Löwenheim–Skolem property, so it must fail compactness, and it does.

Going deeper

For a student

The theorem, proved by Per Lindström in 1969, founded abstract model theory, which compares logics by their properties. It explains why first-order logic is the default logic of model theory: any gain in expressive power costs compactness or the Löwenheim–Skolem theorem.