Compactness (first-order logic)
From Learning Logic for Computer Science
The compactness theorem describes how satisfiability of infinite sets of first-order formulas can be reduced to satisfiability of finite sets of first-order formulas. This is reminiscent of a phenomenon in topology called compactness. In fact, it is the same phenomenon.
Theorem [Compactness theorem] Let $\mathcal S$ be an arbitrary signature and $\Phi$ an arbitrary set of $\mathcal S$-formulas. Then $\Phi$ is satisfiable if, and only if, every finite set $\Phi_0 \subseteq \Phi$ is satisfiable.
Corollary Let $\mathcal S$ be an arbitrary signature, $\Phi$ an arbitrary set of $\mathcal S$-formulas, and $\psi$ any $\mathcal S$-formula. Then $\Phi \models \psi$ if, and only if, $\Phi_0 \models \psi$ for some finite set $\Phi_0 \subseteq \Phi$.
This theorem (its corollary) is a fundamental result on first-order logic.
Proof (using a proof system)
There are several proofs of the compactness theorem; a common approach is to take a syntactic approach via a sound and complete proof system.
Assume we are given any sound and complete proof system for first-order logic and $\vdash$ denotes deduction in this proof system. Consider, for instance, the natural proof system. Any reasonable proof system is based on proofs, which are, essentially, finite lists of formulas where one formula results from previous formulas by an application of a proof rule or by using a premise. This implies that in every proof only a finite number of premises are used. Formally, this means that if $\Phi \vdash \psi$, then $\Phi_0 \vdash \psi$ for some finite set $\Phi_0 \subseteq \psi$.
As we assume that the proof system is sound and complete, we conclude $\Phi \models \psi$ if there is a finite set $\Phi_0 \subseteq \Phi$ such that $\Phi_0 \models \psi$, which proves the corollary.
The theorem itself follows from the basic fact that $\Phi$ is satisfiable if, and only if, $\Phi \not\models \bot$.
Simple application
Compactness has many different and deep applications. Here is a very simple one.
Theorem Let $\mathcal S$ be the empty signature and let $\mathcal K$ be the class of all finite $\mathcal S$-structures. In other words, $\mathcal K$ is the class of finite sets. Then $\mathcal K$ is not axiomatizable.
Proof The proof is by way of contradiction. Assume $\mathcal K$ is axiomatizable, say $\mathcal K = \text{Mod}(\Phi_{< \infty})$ for some set of $\Phi_{< \infty}$ of first-order formulas without free variables.
For every $n \geq 1$, consider the formula $\varphi_n$ defined by \begin{align} \varphi_n & = \exists x_0 \dots \exists x_{n-1} \bigwedge_{i<j<n} \neg x_i \doteq x_j \enspace. \end{align} Then $\mathcal A \models \varphi_n$ if, and only if, $A$ has at least $n$ elements. In other words, letting $\Phi_\infty = \{\varphi_1, \varphi_2, \dots\}$, we obtain $\text{Mod}(\Phi_\infty) = \{\mathcal A \colon \text{card}(A) = \infty\}$.
Finally, consider $\Phi = \Phi_\infty \cup \Phi_{<\infty}$. Clearly, $\Phi$ is not satisfiable, that is, $\text{Mod}(\Phi) = \emptyset$, simply because a set cannot have a finite number of elements and at the same time an infinite number of elements. But every finite subsetq $\Phi_0$ of $\Phi$ is satisfiable for the following reason. Since $\Phi_0$ is finite, there is some $k$ such that $\Phi_0 \subseteq \Phi_{<\infty} \cup \{\varphi_1, \dots, \varphi_k\}$. Any $\mathcal A$-structure with at least $k$ elements is a model of this set—a contradiction.