[proofplan] The proof is a one-line reduction to two syntactic facts: [Gödel's Completeness Theorem](/theorems/1487), which says $S$ has a model iff $S$ is consistent, and the **finiteness of formal proofs**. We prove the contrapositive: if $S$ has no model, $S$ is inconsistent, so some **finite** subset of $S$ is already inconsistent (because the proof of $\bot$ from $S$ uses only finitely many premises), hence that finite subset has no model, contradicting the hypothesis. [/proofplan]

[step:Reduce "has a model" to "is consistent" via Gödel's Completeness Theorem] Recall that a set of sentences $T$ is **consistent** if $T \not\vdash \bot$. [Gödel's Completeness Theorem](/theorems/1487) (applied with $p = \bot$) yields \begin{align*} T \text{ has a model} &\iff T \text{ is consistent}. \end{align*} Indeed, $(\Rightarrow)$ if $A \models T$, then $A \not\models \bot$, so $T \not\models \bot$, hence by Soundness $T \not\vdash \bot$; $(\Leftarrow)$ is the nontrivial direction of the Completeness Theorem (as established in Step 2 of its proof via the Model Existence Lemma). Thus it suffices to prove the consistency version: **if every finite subset of $S$ is consistent, then $S$ is consistent.** [/step]

[step:Argue by contradiction using the finiteness of formal proofs]Suppose, for contradiction, that $S$ is inconsistent, i.e., $S \vdash \bot$. A formal proof is, by definition, a **finite** sequence of formulas, each of which is either a premise from $S$, a logical axiom, or obtained from previous formulas by modus ponens or generalisation. In particular, a derivation of $\bot$ from $S$ cites only finitely many premises from $S$. Let these premises be $s_1, s_2, \dots, s_n \in S$, and set \begin{align*} S_0 &= \{s_1, s_2, \dots, s_n\} \subseteq S. \end{align*} Then $S_0$ is a finite subset of $S$, and the very same formal proof witnesses $S_0 \vdash \bot$. Thus $S_0$ is inconsistent. By the equivalence of Step 1, $S_0$ has no model. This contradicts the hypothesis that **every** finite subset of $S$ has a model. Hence $S$ is consistent, and by Step 1, $S$ has a model.[/step]

[guided]The Compactness Theorem is a direct consequence of two facts, one deep and one elementary. **The deep fact.** By [Gödel's Completeness Theorem](/theorems/1487), semantic and syntactic consequence coincide. In particular, taking $p = \bot$ gives: $T$ has a model if and only if $T$ is consistent. One direction is Soundness (a model of $T$ cannot satisfy $\bot$, so $T \not\vdash \bot$); the other is the nontrivial content of the Completeness Theorem, itself built on the Model Existence Lemma. Under this equivalence, Compactness reduces to: **if every finite subset of $S$ is consistent, then $S$ is consistent**. **The elementary fact.** Formal proofs are finite objects. A derivation of $\bot$ from $S$ is a finite list of formulas, each entered by premise, axiom, modus ponens, or generalisation. Hence only finitely many premises from $S$ appear as line-citations in the derivation. **The contradiction.** Assume $S$ is inconsistent: $S \vdash \bot$. Pick a specific proof. Collect the finitely many premises it cites: \begin{align*} S_0 &= \{s_1, \dots, s_n\} \subseteq S. \end{align*} The exact same proof (a finite sequence of formulas) is a proof of $\bot$ from $S_0$ — every premise used lies in $S_0$ by construction. So $S_0 \vdash \bot$, i.e., $S_0$ is inconsistent. By Step 1, $S_0$ has no model. But **$S_0$ is a finite subset of $S$**, and by hypothesis every finite subset of $S$ has a model. Contradiction. Therefore $S$ is consistent, and by Step 1, $S$ has a model. **Remark on where compactness comes from.** The name "compactness" reflects a topological reformulation: the space of complete theories extending a given language can be topologised so that the sets $\{T : p \in T\}$ form a clopen basis, and the resulting space is compact in the usual sense. The proof above is, in effect, using the finite-character property of consistency — a trace of the same phenomenon.[/guided]