The compactness theorem

Theorem

The compactness theorem

T-127Home MU-403Threads logic

Statement

Let \(L\) be a first-order language and let \(T\) be a set of \(L\)-sentences. Then \(T\) is satisfiable (i.e. there exists an \(L\)-structure \(\mathcal{M}\) with \(\mathcal{M}\models\varphi\) for every \(\varphi\in T\)) if and only if every finite subset \(T_0\subseteq T\) is satisfiable. Equivalently, in contrapositive form: if \(T\) is unsatisfiable then some finite \(T_0\subseteq T\) is already unsatisfiable.

Why it matters

The compactness theorem converts a question about a possibly infinite set of first-order constraints into a question about finite fragments of it. This single fact underlies almost all existence proofs in model theory: constructing nonstandard models of arithmetic and analysis, proving the existence of models of arbitrary infinite cardinality (Löwenheim–Skolem), and showing that many natural classes of structures — finite groups, well-orderings, connected graphs — are not axiomatizable by any set of first-order sentences.

Its power is almost paradoxical: it says that first-order logic, despite quantifying over potentially infinite domains, is controlled entirely by finite information, because a proof of a contradiction (like any formal proof) can only ever use finitely many premises.

Hypotheses

\(L\) is a first-order language (a fixed signature of relation, function and constant symbols) and \(T\) is a set of first-order \(L\)-sentences. Counterexample sketch: in the infinitary logic \(L_{\omega_1,\omega}\), which allows countable conjunctions/disjunctions, let \(T=\{\exists x_1\cdots\exists x_n\ \textstyle\bigwedge_{i\lt j\le n} x_i\ne x_j : n\in\mathbb{N}\}\cup\{\varphi_{\mathrm{fin}}\}\) where \(\varphi_{\mathrm{fin}}\) is the countable disjunction "the domain has exactly \(1\) element, or exactly \(2\), or exactly \(3\), \(\dots\)". Every finite subset of \(T\) only bounds the domain size below by some fixed \(n\), so is satisfied by a sufficiently large finite structure; but \(T\) itself forces the domain to be simultaneously finite and of every size \(n\), hence is unsatisfiable. Compactness fails outright once infinite conjunctions are allowed.

The underlying logic is classical (two-valued) first-order logic, with a sound and complete finitary proof calculus. Counterexample sketch: full second-order logic (with standard, full-power set semantics for second-order quantifiers) has no complete finitary proof system, and compactness fails there too. Let \(T=\mathrm{PA}_2\cup\{c\ne 0, c\ne 1, c\ne 2,\dots\}\) (second-order Peano arithmetic plus a fresh constant \(c\) declared different from every numeral). \(\mathrm{PA}_2\) is categorical: its only model (up to isomorphism) is the standard \(\mathbb{N}\). Every finite subset of \(T\) only excludes finitely many numerals for \(c\), so is satisfiable by interpreting \(c\) as a larger standard number. But the full \(T\) is unsatisfiable, since in the unique model \(\mathbb{N}\), \(c\) would have to equal some numeral. So the "finite subsets satisfiable \(\Rightarrow\) whole satisfiable" implication fails for second-order logic.

\(T\) is a set of sentences (no free variables) — satisfaction is evaluated in a single fixed structure, not relative to a variable assignment. If free variables were allowed without universal closure, "satisfiable" would be ambiguous (satisfiable by some assignment vs. all assignments), and the finite-character argument via proof-length would need to track witnessing terms separately; the theorem is stated for sentences precisely to avoid this bookkeeping.

Proof

(\(\Rightarrow\)) If \(T\) is satisfiable, every finite subset of \(T\) is satisfiable.

If \(\mathcal{M}\models T\) then in particular \(\mathcal{M}\models\varphi\) for every \(\varphi\) in any subset \(T_0\subseteq T\), by the definition of \(\mathcal{M}\models T\) as "\(\mathcal{M}\models\varphi\) for all \(\varphi\in T\)". A

(\(\Leftarrow\)) Assume every finite \(T_0\subseteq T\) is satisfiable; we must produce a model of all of \(T\). We argue by contraposition: suppose instead that \(T\) is unsatisfiable, and derive that some finite subset is unsatisfiable.

Standard reduction of an "only if all finite pieces are consistent" statement to its contrapositive, which is easier to attack via syntax. A

By Gödel's Completeness Theorem for first-order logic, for any set of sentences \(\Sigma\): \(\Sigma\) is satisfiable \(\iff\) \(\Sigma\) is (syntactically) consistent, i.e. \(\Sigma\nvdash\bot\) in a sound and complete finitary Hilbert- or natural-deduction-style proof calculus.

This is a named external lemma (Gödel, 1929), proved independently of compactness by the Henkin construction: build a maximal consistent extension of \(\Sigma\) with witnesses for every existential sentence and take the term model of the resulting theory. We invoke it as a black box here. B

Since \(T\) is unsatisfiable, the Completeness Theorem gives \(T\vdash\bot\): there is a formal derivation \(D\) of a contradiction from \(T\).

Contrapositive application of Step 3 with \(\Sigma=T\): satisfiable \(\iff\) consistent, so unsatisfiable \(\iff\) inconsistent, i.e. \(T\vdash\bot\). A

A derivation \(D\) is by definition a finite sequence of formulas \(\psi_1,\dots,\psi_k=\bot\), each either a logical axiom, or a member of \(T\), or obtained from earlier \(\psi_i\) by one of finitely many inference rules (each of finite arity).

This is the syntactic definition of a formal proof in any standard first-order calculus (Hilbert system, sequent calculus, natural deduction): proofs are finite objects by construction — this is what "finitary proof system" means. C

Let \(T_0=\{\psi_i : \psi_i\in T,\ 1\le i\le k\}\). Then \(T_0\) is finite (at most \(k\) elements) and \(T_0\subseteq T\), and the very same sequence \(D\) is a valid derivation of \(\bot\) from \(T_0\), so \(T_0\vdash\bot\).

A derivation only ever cites finitely many premises — namely those \(\psi_i\) in the sequence that are premises rather than axioms or rule-consequences — and citing exactly that finite set as the premise set still validates the identical derivation, since none of the intermediate steps used anything about the rest of \(T\). B

By soundness of the proof calculus (the easy direction of Completeness): \(T_0\vdash\bot\ \Rightarrow\ T_0\models\bot\), i.e. \(T_0\) has no model, so \(T_0\) is unsatisfiable.

Soundness: every derivable sentence is a semantic consequence, proved by induction on derivation length showing each axiom is valid and each rule preserves validity in every structure. A

We have produced a finite subset \(T_0\subseteq T\) that is unsatisfiable. This is the contrapositive of the desired implication, so: every finite subset of \(T\) satisfiable \(\Rightarrow\) \(T\) satisfiable.

Discharge of the contraposition set up in Step 2; combined with Step 1 this gives the full biconditional. A

Result

\(T\text{ satisfiable} \iff \text{every finite } T_0\subseteq T \text{ is satisfiable.}\)

Reading. An infinite list of first-order requirements can be jointly met by some single structure exactly when every finite sub-list can be met (possibly by different structures for different sub-lists) — satisfiability is a "finite character" property.

Scope. Applies to any set of sentences in any first-order language (arbitrary cardinality of the signature and of \(T\) itself). It does not apply to second-order logic with full semantics, nor to infinitary logics such as \(L_{\omega_1,\omega}\) or \(L_{\infty,\omega}\), nor to logics with generalized quantifiers like "there exist uncountably many" that break finitary proof theory.

Corollaries & converses

The direction "\(T\) satisfiable \(\Rightarrow\) every finite subset satisfiable" is itself already the converse of the substantive half of the theorem, and it is the trivial half (Step 1) — so compactness is genuinely a biconditional with one easy and one deep direction, not a one-way implication awaiting a converse.
Upward Löwenheim–Skolem: if \(T\) has an infinite model, it has models of every infinite cardinality \(\ge|L|\); proved by adding \(\kappa\)-many fresh constants with pairwise-distinctness axioms and applying compactness (finite subsets only mention finitely many new constants, satisfiable in the original infinite model).
Nonstandard models of \(\mathrm{Th}(\mathbb{N})\), \(\mathrm{Th}(\mathbb{R})\) (hyperreals), and any theory with an infinite model exist, by adjoining a constant declared larger than every numeral/standard element.
Compactness for propositional logic is the analogous statement for a (possibly infinite) set of propositional formulas and is proved the same way (or directly via König's Lemma on finitely-branching trees of partial truth assignments); first-order compactness as proved above reduces to it via the completeness theorem, but a direct semantic (ultrafilter/ultraproduct) proof of first-order compactness exists too and does not route through provability at all.
Compactness is strictly weaker than the full Axiom of Choice: it is equivalent to the Boolean Prime Ideal Theorem (equivalently, the existence of nonprincipal ultrafilters), a strictly weaker choice principle.

Fails without

Dropping first-order restriction (infinitary logic \(L_{\omega_1,\omega}\)): as in the Hypotheses box, \(T=\{\exists x_1\cdots\exists x_n\bigwedge_{i\lt j}x_i\ne x_j : n\in\mathbb{N}\}\cup\{\varphi_{\mathrm{fin}}\}\) has every finite subset satisfiable but \(T\) itself is not, since it demands the domain be both infinite (arbitrarily many elements) and finite (\(\varphi_{\mathrm{fin}}\)).
Dropping classical/finitary proof theory (full second-order logic): \(T=\mathrm{PA}_2\cup\{c\ne \underline{n} : n\in\mathbb{N}\}\) has every finite subset satisfiable (interpret \(c\) as a large enough standard numeral) but \(T\) is unsatisfiable, because categoricity of \(\mathrm{PA}_2\) leaves no room for a nonstandard witness for \(c\).
Dropping "finite" in "every finite subset satisfiable" and asking about arbitrary infinite subsets instead: trivial degeneracy — if we only demanded that some fixed infinite \(T_1\subsetneq T\) be satisfiable, this says nothing about \(T\setminus T_1\), so \(T\) can certainly still be unsatisfiable (e.g. \(T=T_1\cup\{\lnot\psi\}\) for \(\psi\in T_1\)); the theorem specifically needs the "finite" quantifier to range over all finite subsets, which is what makes syntactic derivations (finite by nature) the right tool.

Common errors

Believing compactness gives a single uniform bound "\(n\)" such that satisfiability of the first \(n\) sentences implies satisfiability of all of \(T\); in fact the theorem only guarantees that each finite subset is separately satisfiable, possibly by wildly different structures, and existence of a single common model for all of \(T\) is exactly the (nontrivial) conclusion, not an intermediate bound.
Assuming the models witnessing finite subsets converge or embed into the eventual model of \(T\); the proof (via completeness/consistency, or via ultraproducts) generally produces the model of \(T\) abstractly, with no direct structural relationship to the finite-subset models.
Applying compactness to conclude a property is first-order axiomatizable, when the correct use is the reverse: compactness is used to show classes are not axiomatizable (finiteness, connectedness, well-foundedness) by exhibiting a theory whose finite subsets are satisfiable but which forces a structure with none of the target property.
Forgetting the hypothesis that \(T\) consists of sentences (no free variables) and conflating "\(T\) is satisfiable" with "\(T\) is satisfiable by every assignment", which silently changes the semantics being compactified.
Trying to prove compactness "directly" by taking a limit or union of the finite-subset models; there is in general no way to form such a union (different finite-subset models can have incompatible domains), which is precisely why the proof must go through an indirect device (provability, or an ultrafilter/ultraproduct).

Discussion

The compactness theorem is named by analogy with topological compactness: give \(2^{L}\) (or the Stone space of complete theories) a suitable topology in which basic open sets correspond to single sentences, and satisfiability of \(T\) corresponds to a family of closed sets having the finite intersection property; the theorem is then literally the statement that this space is compact. This is not just decoration — the standard alternative proof of compactness constructs an ultrafilter \(U\) on the index set of finite subtheories (or, in the ultraproduct formulation, takes an ultraproduct \(\prod_{T_0} \mathcal{M}_{T_0}/U\) of the witnessing finite-subset models) and shows via Łoś's Theorem that the resulting structure models all of \(T\).

Historically the result is due to Gödel (1930, as a corollary of his completeness theorem for countable languages) with the uncountable case established by Anatoly Mal'tsev (1936); Alfred Tarski coined "compactness" and connected it explicitly to the topological picture in the 1950s. The theorem became one of the two pillars (with Löwenheim–Skolem) on which classical model theory of the 1950s–60s was built.

The theorem's chief service is negative: it is the standard tool for proving non-definability results. To show a class \(K\) of structures is not axiomatizable by any first-order theory, one exhibits sentences \(\theta_n\) true throughout \(K\) but forming, together with a further sentence, a theory whose finite parts are satisfiable in \(K\)-structures while the whole forces something outside \(K\) (e.g. an infinite element, an infinite path, a nonstandard integer). This is the source of the classical results that "finite", "well-ordered", "connected", and "torsion" are not first-order expressible.

A subtlety worth flagging: because the syntactic proof above routes through Gödel's completeness theorem, and completeness itself is usually proved (via the Henkin construction) without presupposing compactness, there is no circularity — but one should not casually assume completeness "is" compactness in disguise; they coincide in strength only via this specific pair of implications, and the semantic (ultraproduct) proof of compactness is fully independent of any proof calculus, giving a genuinely different route to the same fact and clarifying that compactness is fundamentally a fact about ultrafilters, not about provability.

Worked examples

Construct a nonstandard model of arithmetic. Let \(L_A=\{+,\cdot,\lt,0,1\}\) and let \(\mathrm{Th}(\mathbb{N})\) be the (complete) set of all \(L_A\)-sentences true in the standard model \(\mathbb{N}\). Add one new constant symbol \(c\) and set \(T=\mathrm{Th}(\mathbb{N})\cup\{c\gt\underline{n} : n\in\mathbb{N}\}\), where \(\underline{n}\) is the term \(1+1+\cdots+1\) (\(n\) times).

Setup: a theory designed so any model must contain an element larger than every standard natural number. B

Any finite \(T_0\subseteq T\) mentions only finitely many of the sentences \(c\gt\underline{n}\), say for \(n\le N\). Interpret \(c\) as \(N+1\) inside the standard model \(\mathbb{N}\); this satisfies \(\mathrm{Th}(\mathbb{N})\) (trivially, it's \(\mathbb{N}\) itself) and every \(c\gt\underline{n}\) with \(n\le N\). So \(T_0\) is satisfiable.

Direct construction of a witnessing model for each finite subset, expanding \(\mathbb{N}\) by one extra numeral-interpretation for \(c\). A

By the Compactness Theorem, \(T\) is satisfiable: there is \(\mathcal{M}\models T\).

Application of T-127 with the finite-subset satisfiability just verified. A

\(\mathcal{M}\models\mathrm{Th}(\mathbb{N})\), so \(\mathcal{M}\) satisfies the same first-order sentences as \(\mathbb{N}\) (it is elementarily equivalent to \(\mathbb{N}\)), yet \(\mathcal{M}\) has an element \(c^{\mathcal{M}}\) exceeding every standard numeral, so \(\mathcal{M}\not\cong\mathbb{N}\).

Reading off the conclusion from the definition of \(T\): elementary equivalence from membership of \(\mathrm{Th}(\mathbb{N})\), non-isomorphism from the extra element having no counterpart among finite standard numerals. B

\(\exists\,\mathcal{M}\not\cong\mathbb{N}\ :\ \mathcal{M}\equiv\mathbb{N}\text{ (nonstandard model of arithmetic, with an infinite integer).}\)

De Bruijn–Erdős theorem via compactness. Let \(G=(V,E)\) be a graph (possibly infinite) such that every finite subgraph of \(G\) is \(k\)-colourable. Show \(G\) itself is \(k\)-colourable. Introduce propositional variables \(p_{v,i}\) for \(v\in V\), \(1\le i\le k\), meaning "\(v\) gets colour \(i\)".

Encoding a colouring problem as a satisfiability problem: this is the propositional-logic form of compactness, proved by the same finite-derivation argument (or via König's Lemma). B

Let \(T\) consist of: (a) \(p_{v,1}\lor\cdots\lor p_{v,k}\) for each \(v\) (every vertex gets some colour); (b) \(\lnot(p_{v,i}\land p_{v,j})\) for \(i\ne j\) (at most one colour per vertex); (c) \(\lnot(p_{v,i}\land p_{w,i})\) for each edge \((v,w)\in E\) and each \(i\) (adjacent vertices differ).

Direct transcription: a truth assignment satisfying \(T\) is exactly a proper \(k\)-colouring of \(G\). A

Any finite \(T_0\subseteq T\) mentions only finitely many vertices and edges, i.e. constrains a finite subgraph \(G_0\subseteq G\). By hypothesis \(G_0\) is \(k\)-colourable, and any proper colouring of \(G_0\) (extended arbitrarily to colour-\(1\) on vertices not mentioned) satisfies \(T_0\).

Using the hypothesis "every finite subgraph is \(k\)-colourable" exactly at the scale (finite subgraph) that a finite subset of \(T\) can see. B

By Compactness (propositional form), \(T\) is satisfiable.

Application of T-127 (propositional instance) to the finite satisfiability just shown. A

\(\text{Every finite subgraph of } G \text{ is } k\text{-colourable} \implies G \text{ is } k\text{-colourable, for any graph } G.\)

Problems

Show that the class of finite \(L\)-structures (for \(L=\varnothing\), say) is not axiomatizable by any set of first-order sentences: there is no set \(\Sigma\) such that "\(\mathcal{M}\models\Sigma\)" is equivalent to "\(\mathcal{M}\) is finite".
Solution
Suppose toward contradiction such \(\Sigma\) exists. Let \(T=\Sigma\cup\{\theta_n : n\ge 2\}\), where \(\theta_n\) says "there exist \(n\) pairwise distinct elements" (a first-order sentence: \(\exists x_1\cdots\exists x_n\bigwedge_{i\lt j}x_i\ne x_j\)). Every finite subset of \(T\) mentions only finitely many \(\theta_n\), say up to \(\theta_N\); any finite structure with \(\ge N\) elements models \(\Sigma\) (it's finite) and this finite subset. So every finite subset of \(T\) is satisfiable. By Compactness, \(T\) has a model \(\mathcal{M}\). But \(\mathcal{M}\models\Sigma\) means \(\mathcal{M}\) is finite, while \(\mathcal{M}\models\theta_n\) for all \(n\) means \(\mathcal{M}\) has at least \(n\) elements for every \(n\), i.e. \(\mathcal{M}\) is infinite. Contradiction. So no such \(\Sigma\) exists.
Let \(L=\{E\}\) with \(E\) a binary relation symbol (graph edge relation). Show "\(G\) is connected" is not expressible by any first-order theory, i.e. there is no \(\Sigma\) such that \(\mathcal{M}\models\Sigma \iff \mathcal{M}\) is a connected graph.
Solution
Suppose \(\Sigma\) works. Add two new constants \(a,b\) and let \(\delta_n\) say "there is no path of length \(\le n\) from \(a\) to \(b\)" (expressible: \(\lnot\bigvee_{m\le n}\exists x_1\cdots x_{m-1}(E(a,x_1)\land E(x_1,x_2)\land\cdots\land E(x_{m-1},b))\), a finite first-order sentence for each fixed \(n\)). Let \(T=\Sigma\cup\{\delta_n : n\in\mathbb{N}\}\). A finite subset of \(T\) only involves \(\delta_n\) for \(n\le N\); take a long path graph (a "ray" of length \(\gt N\)) with \(a,b\) at the two ends more than \(N\) apart — this is connected (models \(\Sigma\)) and satisfies \(\delta_n\) for \(n\le N\). So finite subsets of \(T\) are satisfiable, and by Compactness \(T\) has a model \(\mathcal{M}\). Then \(\mathcal{M}\models\Sigma\) so \(\mathcal{M}\) is connected, meaning some finite path connects \(a^{\mathcal M}\) and \(b^{\mathcal M}\), yet \(\mathcal{M}\models\delta_n\) for every \(n\) says no path of any finite length connects them — contradiction. So connectivity is not first-order axiomatizable.
Prove the Upward Löwenheim–Skolem theorem using compactness: if \(T\) has an infinite model and \(\kappa\ge|L|\) is an infinite cardinal, then \(T\) has a model of cardinality exactly \(\kappa\).
Solution
Add a set \(C=\{c_\alpha : \alpha\lt\kappa\}\) of \(\kappa\)-many new constant symbols and let \(T'=T\cup\{c_\alpha\ne c_\beta : \alpha\ne\beta\lt\kappa\}\). Any finite subset \(T_0'\subseteq T'\) mentions only finitely many of the new inequalities, say among \(c_{\alpha_1},\dots,c_{\alpha_m}\); since \(T\) has an infinite model \(\mathcal{M}\), pick \(m\) distinct elements of \(\mathcal{M}\) to interpret \(c_{\alpha_1},\dots,c_{\alpha_m}\) (possible as \(\mathcal M\) is infinite) and interpret the rest of \(C\) arbitrarily; this expanded structure models \(T_0'\). So every finite subset of \(T'\) is satisfiable, and by Compactness \(T'\) has a model \(\mathcal{N}\), which has \(\ge\kappa\) elements (the interpretations of the \(c_\alpha\) are pairwise distinct) and models \(T\) (as \(T\subseteq T'\)). If \(|\mathcal N|\gt\kappa\), pass to an elementary substructure of size \(\kappa\) containing the \(c_\alpha^{\mathcal N}\) via the (downward) Löwenheim–Skolem theorem, using \(\kappa\ge|L|\) to have room for the required Skolem witnesses; this substructure still has exactly \(\kappa\) elements and models \(T\).
Use compactness to construct a nonstandard, non-Archimedean ordered field extending \(\mathbb{R}\) with an infinitesimal element (the starting point of nonstandard analysis).
Solution
Let \(L\) be the language of ordered rings expanded with a constant \(\underline r\) for every \(r\in\mathbb{R}\) (so \(\mathbb{R}\) is an \(L\)-structure with obvious interpretations), let \(\mathrm{Th}(\mathbb{R})\) be the set of all \(L\)-sentences true in this structure, add a new constant \(\varepsilon\), and set \(T=\mathrm{Th}(\mathbb{R})\cup\{0\lt\varepsilon\lt\underline r : r\in\mathbb{R}, r\gt0\}\). Any finite subset only restricts \(\varepsilon\) below finitely many positive reals \(r_1,\dots,r_m\); interpreting \(\varepsilon\) as \(\min(r_1,\dots,r_m)/2\) inside \(\mathbb{R}\) itself satisfies that finite subset together with \(\mathrm{Th}(\mathbb{R})\). By Compactness, \(T\) has a model \({}^*\mathbb{R}\). Since \({}^*\mathbb{R}\models\mathrm{Th}(\mathbb{R})\), it is an ordered field elementarily equivalent to \(\mathbb{R}\) (so inherits every first-order property of \(\mathbb{R}\), e.g. the intermediate value theorem for definable functions), yet \(\varepsilon^{{}^*\mathbb{R}}\) is positive and smaller than every standard positive real, i.e. an infinitesimal — so \({}^*\mathbb{R}\) is non-Archimedean and \({}^*\mathbb{R}\ne\mathbb{R}\).
(Harder.) Prove the propositional compactness theorem directly via König's Lemma (every finitely branching infinite tree has an infinite branch), for a countable set of propositional variables \(\{p_n : n\in\mathbb{N}\}\) and a set \(\Sigma\) of propositional formulas such that every finite subset is satisfiable. Then explain why this gives an independent proof not relying on Gödel's completeness theorem.
Solution
Build a tree \(\mathcal{T}\) whose level-\(n\) nodes are the truth assignments to \(p_1,\dots,p_n\) (functions \(\{1,\dots,n\}\to\{0,1\}\)) that satisfy every formula of \(\Sigma\) mentioning only \(p_1,\dots,p_n\), with the tree order given by extension of assignments. Each node has at most \(2\) children (extend by \(p_{n+1}=0\) or \(1\)), so \(\mathcal T\) is finitely branching. Level \(n\) is nonempty: the finite subset of \(\Sigma\) mentioning only \(p_1,\ldots,p_n\) is satisfiable by hypothesis, and any satisfying assignment restricted to \(\{p_1,\dots,p_n\}\) gives a node at level \(n\) — actually more carefully, one shows by induction that every level is nonempty, using that a satisfying assignment for the (finite) set of \(\Sigma\)-formulas mentioning only \(p_1,\ldots,p_n\) extends the previous level's assignment for such formulas restricted to \(n-1\) variables. Since \(\mathcal T\) is finitely branching and has nodes at every level, it is infinite, so by König's Lemma \(\mathcal T\) has an infinite branch \(b\), which defines a full assignment \(v:\{p_n\}\to\{0,1\}\). Any \(\varphi\in\Sigma\) mentions finitely many variables, say up to \(p_N\); the level-\(N\) node on \(b\) already satisfies every formula of \(\Sigma\) mentioning only \(p_1,\dots,p_N\), including \(\varphi\), and \(v\) agrees with that node on \(p_1,\dots,p_N\), so \(v\models\varphi\). Hence \(v\models\Sigma\). This proof uses only König's Lemma (itself a compactness-flavoured combinatorial fact about trees, provable directly by König's original "always choose a branch with infinitely many descendants" argument, which needs only countable choice) and never mentions provability or a proof calculus, so it is genuinely independent of Gödel's completeness theorem — giving a second, purely combinatorial/semantic route to compactness (which generalizes to the ultrafilter/ultraproduct proof for uncountable languages).