42.01.02 · mathematical-logic / first-order-logic-completeness

The Compactness Theorem for Propositional Logic

shipped3 tiersLean: none

Anchor (Master): Enderton 2001 §1.7 in full together with the topological proof via Tychonoff; Johnstone 1982 *Stone Spaces* (Cambridge) Ch. I-II (the Stone space of a Boolean algebra, compactness as a topological statement); Jech 2003 *Set Theory* 3e (Springer) Ch. 2 and the Boolean-prime-ideal / ultrafilter material on the strength of compactness as a weak choice principle; de Bruijn-Erdős 1951 *Indag. Math.* 13 (the colouring theorem)

Intuition Beginner

Imagine you are handed an endless list of demands, each one a constraint on which of countless little switches must be on and which off. Some demands talk about switches 3 and 7; another talks about switches 7, 12, and 50; the list never ends. You want to know whether there is one setting of all the switches that meets every demand at once. Checking the whole infinite list directly is hopeless. The compactness theorem says something almost too good: you only ever have to check finite pieces. If every finite handful of demands can be met by some setting, then the entire infinite list can be met by a single setting.

The word "compact" is borrowed from geometry, where it names shapes with no missing edges or escaping-to-infinity behaviour. Here the same flavour appears: the demands cannot conspire to fail "only in the limit." Any genuine clash must already show up among finitely many of them. So failure is always local and finite, never a mysterious infinite accident.

Why care? Many real questions are about infinite situations built from finite rules: colouring an infinite map so neighbours differ, ordering an endless collection consistently, extending a partial plan to a full one. Compactness turns each of these infinite problems into a finite-checking problem. You verify the finite cases, which you can actually do, and the theorem hands you the infinite solution for free. The rest of the unit makes "demand" precise as a logical formula and "setting" precise as a truth assignment, then proves the promise in several different ways.

Visual Beginner

Picture the demands as a growing tree of partial decisions. At each level you decide one more switch, on or off, and you keep only the branches that have not yet broken any demand. The theorem is about whether some branch runs forever.

   Building a setting one switch at a time (keep only "still-OK" branches)

   switch 1:            on            off
                       /  \          /  \
   switch 2:        on    off      on    off
                    |      |        X      |      (X = a finite demand already broken)
   switch 3:      on off  on off          on off
                  |   X    |  |            X   |
                  ...      ...  ...            ...

   If every finite handful of demands is satisfiable, no level is ever
   completely pruned away, so an infinite "still-OK" path survives.
   That surviving path is one setting meeting all demands at once.

Read the tree downward. A branch dies the moment some finite group of demands is violated by the choices made so far. The key observation is that each demand mentions only finitely many switches, so it can only kill a branch after finitely many levels. If finitely many demands could never be satisfied together, that failure would already appear at some finite depth and prune that whole region.

level	finite check you can actually do	what survives
1	demands using only switch 1	the on/off choices that pass
2	demands using switches 1-2	passing partial settings of length 2
3	demands using switches 1-3	passing partial settings of length 3

Because no finite level is ever fully pruned (every finite collection is satisfiable), an unbroken path descends forever, and that infinite path is the setting that meets every demand.

Worked example Beginner

We test the promise on a small infinite list of demands about switches $p_{1}, p_{2}, p_{3}, \dots$ , where each switch is either on (true) or off (false). The list is: "exactly one of all the switches is on." We break that into demands each of which mentions only finitely many switches at a time, and watch finite-satisfiability decide the infinite question.

Step 1. Write demands of the first kind: "at most one switch is on." For every pair $i \neq = j$ we add the demand "not ( $p_{i}$ on and $p_{j}$ on)." Each such demand mentions just two switches.

Step 2. Add one demand of the second kind: "at least one switch is on," meaning " $p_{1}$ on or $p_{2}$ on or $p_{3}$ on or ..." This single demand mentions infinitely many switches, so for the finite-checking method we instead consider its finite approximations later; for now keep the at-most-one demands, which are all finite.

Step 3. Check a finite handful. Take any finite group of the at-most-one demands. They mention finitely many switches, say up to $p_{N}$ . Turn on exactly $p_{1}$ and leave the rest off. No two switches are both on, so every demand in the handful is met. So every finite handful of the at-most-one demands is satisfiable.

Step 4. Apply the promise. Since every finite handful is satisfiable, the whole infinite collection of at-most-one demands is satisfiable. Indeed turning on only $p_{1}$ satisfies all of them at once.

Step 5. Note the contrast. If we also demand "no switch is on" together with "at least one switch is on," then a finite handful already clashes once it contains both, so finite-checking correctly reports failure.

What this tells us: the theorem reduces an endless consistency question to checking finite pieces, and a real contradiction always surfaces in some finite piece. The next sections make "demand," "switch setting," and "satisfiable" exact, and prove the reduction in full.

Check your understanding Beginner

Exercise (easy, multiple choice).

A real clash among an infinite list of demands, when one exists, must already appear:

A. only after checking all infinitely many demands

B. among some finite subset of the demands

C. never, since infinite lists cannot clash

D. only if the demands mention infinitely many switches each

Hint

Each demand mentions only finitely many switches; an unsatisfiable infinite list has an unsatisfiable finite piece.

Answer

B. Compactness, stated in reverse, says an unsatisfiable collection has an unsatisfiable finite subset, so any genuine clash is finitely witnessed. Feedback-correct: failure is always local and finite. Feedback-wrong: A and C miss that finiteness of each demand localises any contradiction; D is false because demands here each mention finitely many switches.

Formal definition Intermediate+

Fix the sentential language of 42.01.01 pending: a set $A$ of sentence symbols (here permitted to be of any cardinality, not only countable), the connectives, and the well-formed formulas over them. A truth assignment is a function $v : A \to {F, T}$ ; its recursive extension $\overset{v}{ˉ}$ to all wffs is the unique connective-respecting extension supplied by unique readability. A wff $σ$ is satisfied by $v$ when $\overset{v}{ˉ} (σ) = T$ . A set $Σ$ of wffs is satisfiable when some single $v$ has $\overset{v}{ˉ} (σ) = T$ for every $σ \in Σ$ ; it is finitely satisfiable when every finite subset $Σ_{0} \subseteq Σ$ is satisfiable ^{[Enderton §1.7]}.

Compactness theorem (statement). A set $Σ$ of wffs is satisfiable if and only if it is finitely satisfiable. Equivalently, in consequence form, $Σ ⊨ τ$ holds if and only if $Σ_{0} ⊨ τ$ for some finite $Σ_{0} \subseteq Σ$ .

The two formulations are interchangeable. If $Σ ⊨ τ$ then $Σ \cup {(\neg τ)}$ is unsatisfiable, so by the satisfiability form some finite $Δ \subseteq Σ \cup {(\neg τ)}$ is unsatisfiable; taking $Σ_{0} = Δ \cap Σ$ gives $Σ_{0} ⊨ τ$ . The converse direction is monotonicity of $⊨$ .

Three viewpoints organise the proofs. Algebraically, the wffs modulo tautological equivalence form a Boolean algebra, the Lindenbaum-Tarski algebra $L_{A}$ , with $[[σ]] \leq [[τ]]$ iff $σ ⊨ τ$ , meet $\land$ , join $\lor$ , complement $\neg$ , top $⊤ = [[tautology]]$ , bottom $⊥$ . A truth assignment is a Boolean homomorphism $L_{A} \to 2$ , equivalently an ultrafilter of $L_{A}$ . Topologically, the set $2^{A} = {F, T}^{A}$ of all truth assignments carries the product topology with ${F, T}$ discrete; this is the Stone space of $L_{A}$ . For a wff $σ$ the model set $Mod (σ) = {v \in 2^{A} : \overset{v}{ˉ} (σ) = T}$ is clopen (closed and open), being a finite union of basic cylinders fixing the finitely many symbols occurring in $σ$ . Combinatorially, partial assignments to finite symbol sets form a tree under extension.

Counterexamples to common slips Intermediate+

"Compactness says every finitely satisfiable set is finite." It says the opposite is harmless: an infinite set is satisfiable as soon as its finite subsets are. The set ${A_{1}} \cup {(\neg A_{n}) : n \geq 2}$ is infinite, finitely satisfiable, and satisfiable.
" $Mod (σ)$ is only closed, like the zero set of a continuous function." In $2^{A}$ with the product topology each $Mod (σ)$ is clopen, because $σ$ depends on finitely many symbols, so the set is decided by finitely many coordinates. This is sharper than mere closedness and is what makes the finite-intersection argument work without separate openness hypotheses.
"Compactness is a triviality once you have completeness." The deductive route does derive it from completeness, but compactness is equivalent to the Boolean prime ideal theorem and so is not a theorem of $ZF$ alone; the semantic content survives even where no deductive calculus is fixed, which is why the topological and ultrafilter proofs matter independently.
"The product space $2^{A}$ is compact because each factor is finite, by a finite argument." For infinite $A$ this is precisely Tychonoff's theorem for the infinite product, whose use of choice is genuine; the compactness of $2^{A}$ is equivalent over $ZF$ to the ultrafilter lemma, not provable by finite means.

Key theorem with proof Intermediate+

The signature theorem is compactness itself, proved here by the topological route, which exhibits most directly why the name "compactness" is literal: it is the topological compactness of the space of truth assignments.

Theorem (compactness, topological proof). Let $A$ be any set of sentence symbols and $Σ$ a set of wffs over $A$ . If every finite subset of $Σ$ is satisfiable, then $Σ$ is satisfiable ^{[Enderton §1.7]}.

Proof. Topologise the set $X = 2^{A} = {F, T}^{A}$ of truth assignments as the product of copies of the two-point discrete space, one copy per sentence symbol. By Tychonoff's theorem $X$ is compact, since each factor ${F, T}$ is compact ^{[Johnstone Ch. II]}. For a wff $σ$ let $Mod (σ) = {v \in X : \overset{v}{ˉ} (σ) = T}$ . The value $\overset{v}{ˉ} (σ)$ depends only on the coordinates $v (A_{i})$ for the finitely many symbols $A_{i}$ occurring in $σ$ , so $Mod (σ)$ is a union of finitely many basic cylinder sets, each of which is clopen; hence $Mod (σ)$ is clopen, in particular closed.

Consider the family $C = {Mod (σ) : σ \in Σ}$ of closed subsets of $X$ . A point of $⋂ C$ is exactly a $v$ satisfying every $σ \in Σ$ , so $Σ$ is satisfiable iff $⋂ C \neq = \emptyset$ . By the finite intersection property characterisation of compactness, $⋂ C \neq = \emptyset$ provided every finite subfamily has nonempty intersection. Given finitely many $σ_{1}, \dots, σ_{n} \in Σ$ , the set ${σ_{1}, \dots, σ_{n}}$ is a finite subset of $Σ$ , hence satisfiable by hypothesis; a satisfying assignment $v$ lies in $Mod (σ_{1}) \cap \dots \cap Mod (σ_{n})$ , which is therefore nonempty. Every finite subfamily of $C$ meets, so by compactness $⋂ C \neq = \emptyset$ , and any $v$ in the intersection satisfies all of $Σ$ . $□$

Corollary (consequence form). $Σ ⊨ τ$ iff $Σ_{0} ⊨ τ$ for some finite $Σ_{0} \subseteq Σ$ . If $Σ ⊨ τ$ then $Σ \cup {(\neg τ)}$ has empty model set, so by the theorem (contrapositive) some finite $Δ \subseteq Σ \cup {(\neg τ)}$ is unsatisfiable; $Σ_{0} = Δ ∖ {(\neg τ)}$ is finite and $Σ_{0} ⊨ τ$ . The reverse is monotonicity.

Bridge. The clopen sets $Mod (σ)$ are the foundational reason the name is no metaphor: satisfiability of $Σ$ is the nonemptiness of an intersection of closed sets, and the finite intersection property is exactly the finite-satisfiability hypothesis, so compactness of $2^{A}$ is the compactness theorem. This builds toward the Stone-duality reading, in which $2^{A}$ is the Stone space of the Lindenbaum-Tarski algebra and ultrafilters are truth assignments, and it appears again in the first-order compactness theorem 42.01.07 pending, where the same finite-intersection skeleton is run over spaces of complete types. The central insight is that a formula constrains only finitely many coordinates, so each constraint is topologically closed and any obstruction to a global solution is detected by a finite subfamily; this is exactly the mechanism by which compactness of a product transfers finite-local solvability to global solvability, and it generalises the switch-tree of the Beginner tier into the finite-intersection property. Putting these together, the deductive proof, the König's-lemma proof, and this topological proof are three readings of one fact — that unsatisfiability is finitely witnessed — and the next tier exhibits them as theorems of the same strength, each equivalent to the Boolean prime ideal theorem.

Exercises Intermediate+

Exercise 4 (medium, symbolic).

Use compactness to prove the de Bruijn-Erdős theorem for $k = 2$ : an infinite graph $G$ is $2$ -colourable (bipartite) iff every finite subgraph is $2$ -colourable.

Hint

For each vertex $v$ introduce a symbol $p_{v}$ (colour $0$ or $1$ ); for each edge $uv$ add the demand $\neg (p_{u} \leftrightarrow p_{v})$ . A finite subset of demands involves a finite subgraph.

Answer

For each vertex $v$ take a sentence symbol $p_{v}$ , reading $p_{v} = T$ as "colour $1$ " and $F$ as "colour $0$ ." For each edge $uv \in E (G)$ add the wff $σ_{uv} := (\neg (p_{u} \leftrightarrow p_{v}))$ , which is satisfied exactly when $u, v$ get different colours. Let $Σ = {σ_{uv} : uv \in E (G)}$ . A satisfying assignment of $Σ$ is precisely a proper $2$ -colouring of $G$ . Any finite $Σ_{0} \subseteq Σ$ mentions finitely many edges, hence lies in a finite subgraph $H \subseteq G$ ; by hypothesis $H$ is $2$ -colourable, and that colouring satisfies $Σ_{0}$ . So $Σ$ is finitely satisfiable, and by compactness satisfiable, giving a proper $2$ -colouring of all of $G$ . The converse is immediate, as a colouring of $G$ restricts to each finite subgraph. Rubric: full credit for the edge-clause encoding and the finite-subset-to-finite-subgraph step.

Exercise 5 (medium, symbolic).

Prove that compactness is equivalent to: every finitely satisfiable $Σ$ extends to a complete finitely satisfiable set $Σ^{*}$ (one containing, for every wff $γ$ , exactly one of $γ, (\neg γ)$ ). Then show $Σ^{*}$ defines a truth assignment.

Hint

Maximise by Zorn's lemma among finitely satisfiable sets; show maximality forces completeness; read off $v (A_{i}) = T$ iff $A_{i} \in Σ^{*}$ .

Answer

Order the finitely satisfiable supersets of $Σ$ by inclusion. A chain's union is finitely satisfiable, since any finite subset of the union lies in one chain member; by Zorn's lemma there is a maximal finitely satisfiable $Σ^{*} \supseteq Σ$ . For any $γ$ , at least one of $Σ^{*} \cup {γ}$ , $Σ^{*} \cup {(\neg γ)}$ is finitely satisfiable: otherwise finite $Δ_{1} \cup {γ}$ and $Δ_{2} \cup {(\neg γ)}$ are unsatisfiable with $Δ_{i} \subseteq Σ^{*}$ , but then $Δ_{1} \cup Δ_{2}$ is finite, finitely satisfiable, and every model of it satisfies one of $γ, (\neg γ)$ , a contradiction. Maximality then puts that consistent extension's new member into $Σ^{*}$ , so exactly one of $γ, (\neg γ)$ lies in $Σ^{*}$ . Define $v (A_{i}) = T$ iff $A_{i} \in Σ^{*}$ ; an induction on wffs using completeness and finite satisfiability of $Σ^{*}$ shows $\overset{v}{ˉ} (γ) = T$ iff $γ \in Σ^{*}$ , so $v$ satisfies $Σ^{*} \supseteq Σ$ . Rubric: full credit for the Zorn maximisation, the one-of-two completeness step, and the connective-respecting induction.

Exercise 7 (hard, symbolic).

Use compactness to show that every partial order $(P, \leq)$ on a (possibly infinite) set extends to a total (linear) order on $P$ .

Hint

Introduce a symbol $p_{x y}$ meaning " $x$ precedes $y$ ." Write finite clause schemes for irreflexivity, transitivity, totality, and agreement with $\leq$ . Every finite subset involves finitely many elements; on a finite poset a linear extension exists (topological sort).

Answer

For each ordered pair $(x, y)$ with $x \neq = y$ introduce $p_{x y}$ , read " $x$ strictly precedes $y$ ." Impose the wffs: asymmetry $(\neg (p_{x y} \land p_{y x}))$ ; totality $(p_{x y} \lor p_{y x})$ for $x \neq = y$ ; transitivity $((p_{x y} \land p_{y z}) \to p_{x z})$ ; and fidelity $p_{x y}$ whenever $x < y$ in the given partial order. Call this set $Σ$ . A satisfying assignment names a total strict order refining $\leq$ : asymmetry and transitivity make it a strict order, totality makes it linear, fidelity makes it extend $\leq$ . Any finite $Σ_{0} \subseteq Σ$ mentions finitely many elements $S \subseteq P$ ; the restriction $\leq ↾_{S}$ is a finite partial order, which admits a linear extension by repeatedly choosing a minimal element (topological sort), and that linear extension satisfies $Σ_{0}$ . So $Σ$ is finitely satisfiable, hence by compactness satisfiable, and the resulting linear order extends $\leq$ on all of $P$ . Rubric: full credit for the order-axiom clauses, the fidelity clauses from $\leq$ , and the finite-poset topological-sort step feeding finite satisfiability.

Exercise 8 (hard, symbolic).

Show that the compactness theorem implies the deductive completeness statement is not needed for satisfiability arguments by deriving compactness from the ultrafilter lemma on the Lindenbaum-Tarski algebra, with no reference to a proof calculus.

Hint

Map $Σ$ into the Boolean algebra $L_{A}$ ; finite satisfiability means the filter generated by ${[[σ]]}$ is proper; extend to an ultrafilter; read it as a truth assignment.

Answer

Let $L_{A}$ be the Lindenbaum-Tarski algebra: wffs modulo tautological equivalence, a Boolean algebra with $[[σ]] \leq [[τ]]$ iff $σ ⊨ τ$ . For $Σ$ finitely satisfiable, the finite meets $[[σ_{1}]] \land \dots \land [[σ_{n}]] = [[σ_{1} \land \dots \land σ_{n}]]$ are all $\neq = ⊥$ , since ${σ_{1}, \dots, σ_{n}}$ has a model; so ${[[σ]] : σ \in Σ}$ has the finite-meet property and generates a proper filter $F$ . By the ultrafilter lemma $F$ extends to an ultrafilter $U$ on $L_{A}$ . The quotient map $L_{A} \to L_{A} / (complement of U) ≅ 2$ is a Boolean homomorphism $h$ sending each $[[σ]] \in U$ to $T$ ; setting $v (A_{i}) = h ([[A_{i}]])$ gives a truth assignment with $\overset{v}{ˉ} (σ) = h ([[σ]]) = T$ for every $σ \in Σ$ , because $[[σ]] \in F \subseteq U$ . Thus $Σ$ is satisfiable, using only the ultrafilter lemma and no deductive calculus. Rubric: full credit for the finite-meet/proper-filter step, the ultrafilter extension, and the homomorphism-to- $2$ reading as an assignment.

Advanced results Master

Compactness for propositional logic admits four proofs of differing flavour, all of one logical strength, and its applications and exact set-theoretic location organise the rest of the material.

Theorem 1 (four proofs, one theorem). The following routes each prove that a finitely satisfiable set $Σ$ over a set $A$ of sentence symbols is satisfiable, and each is, over $ZF$ , equivalent to the Boolean prime ideal theorem ^{[Jech Ch. 2]}. (i) Deductive. By soundness and completeness of the sentential calculus 42.01.01 pending, $Σ$ is satisfiable iff consistent; a deduction of a contradiction uses finitely many premises, so an inconsistent $Σ$ has an inconsistent finite subset, whence finite satisfiability forces satisfiability. (ii) Tree / König. For countable $A$ , build the binary tree of partial assignments preserving finite satisfiability; it is infinite and finitely branching, so König's lemma yields an infinite branch, a satisfying assignment. (iii) Topological. The model sets $Mod (σ)$ are closed in the compact space $2^{A}$ (Tychonoff) and have the finite intersection property, so their intersection is nonempty (Key theorem). (iv) Ultrafilter / Lindenbaum-Tarski. A finitely satisfiable $Σ$ generates a proper filter of the Boolean algebra $L_{A}$ ; an ultrafilter extending it is a homomorphism to $2$ , a satisfying assignment.

Theorem 2 (compactness as the semantic shadow of finite proofs). The deductive route is not an accident of one calculus. Compactness expresses, on the semantic side, that the consequence relation $⊨$ is finitary: $Σ ⊨ τ$ implies $Σ_{0} ⊨ τ$ for a finite $Σ_{0}$ . The completeness theorem $⊢ = ⊨$ identifies this with the syntactic finiteness of deductions, each of which is a finite object. Thus compactness is exactly the statement that semantic entailment cannot outrun what some finite proof could certify; the equivalence $Σ$ satisfiable $\Leftrightarrow$ $Σ$ consistent is the precise bridge ^{[Enderton §1.7]}.

Theorem 3 (Stone duality reading). The Lindenbaum-Tarski algebra $L_{A}$ is a Boolean algebra, and its Stone space $S (L_{A})$ — the set of ultrafilters, topologised by the clopen sets $[[σ]] = {U : [[σ]] \in U}$ — is canonically homeomorphic to the closure of the truth-assignment space inside $2^{A}$ , and equals $2^{A}$ when $A$ is the symbol set and no nontrivial axioms are imposed ^{[Johnstone Ch. I-II]}. Under this duality a theory $Σ$ corresponds to the closed set $⋂_{σ \in Σ} [[σ]]$ , its models are the points of that closed set, and the compactness theorem is the compactness of $S (L_{A})$ : a family of basic closed sets with the finite intersection property meets. Satisfiability is closedness-plus-nonemptiness; finite satisfiability is the finite intersection property.

Theorem 4 (the de Bruijn-Erdős colouring theorem). For a fixed positive integer $k$ , an infinite graph $G = (V, E)$ is $k$ -colourable iff every finite subgraph of $G$ is $k$ -colourable ^{[de Bruijn-Erdős 1951]}. Encode with symbols $p_{v, c}$ for $v \in V$ , $1 \leq c \leq k$ , the clauses " $v$ gets at least one colour" $⋁_{c} p_{v, c}$ , " $v$ gets at most one colour" $(\neg (p_{v, c} \land p_{v, c^{'}}))$ for $c \neq = c^{'}$ , and "adjacent vertices differ" $(\neg (p_{u, c} \land p_{v, c}))$ for $uv \in E$ . A finite subset of clauses mentions finitely many vertices, hence a finite subgraph, $k$ -colourable by hypothesis; so the clause set is finitely satisfiable, and by compactness satisfiable, giving a $k$ -colouring of $G$ . The same template proves the linear-extension theorem (every partial order extends to a total order) and consistency-of-finite-fragments arguments throughout combinatorics 40.04.06.

Theorem 5 (exact strength: a weak choice principle). Over $ZF$ , the compactness theorem for propositional logic is equivalent to the Boolean prime ideal theorem (every proper ideal of a Boolean algebra extends to a prime ideal), to the ultrafilter lemma (every filter on a set extends to an ultrafilter), and to the Tychonoff theorem for Hausdorff spaces ^{[Jech Ch. 2]}. These principles follow from the axiom of choice but do not imply it: there are models of $ZF$ satisfying the Boolean prime ideal theorem in which the axiom of choice fails (Halpern-Lévy). For a countable symbol set the König's-lemma proof needs only weak König's lemma, dropping below the full prime ideal theorem; the genuine choice content appears for uncountable $A$ .

Synthesis. The four proofs are the foundational reason compactness is robust: the deductive route exhibits it as the semantic shadow of finite proofs, the topological route as literal compactness of $2^{A}$ , and the ultrafilter route as the Boolean prime ideal theorem on the Lindenbaum-Tarski algebra, and this is exactly the equivalence locating compactness strictly below the axiom of choice. The central insight is that a wff constrains finitely many coordinates, so each model set is clopen and any obstruction is finitely witnessed; this generalises the switch-tree into the finite intersection property and is dual to the syntactic finiteness of a single deduction. Putting these together, the colouring, ordering, and finite-fragment-consistency applications are one template — encode an infinite combinatorial constraint as a propositional theory, observe finite subsets meet finite sub-instances, and invoke compactness — and the bridge is Stone duality, under which theories are closed subsets of a Stone space and satisfiability is nonemptiness, the same picture that the first-order compactness theorem 42.01.07 pending re-runs over type spaces to manufacture nonstandard models. What changes in the first-order case is not the topological skeleton but the objects: cylinders of truth values become clopen sets of complete types, and the harvest — Löwenheim-Skolem, nonstandard arithmetic, the failure of finite axiomatisability — is the model-theoretic content absent from the decidable propositional warm-up.

Full proof set Master

Proposition 1 (model sets are clopen). In $2^{A}$ with the product topology, $Mod (σ)$ is clopen for every wff $σ$ .

Proof. Let $A_{i_{1}}, \dots, A_{i_{m}}$ be the finitely many sentence symbols occurring in $σ$ . The value $\overset{v}{ˉ} (σ)$ depends only on $v (A_{i_{1}}), \dots, v (A_{i_{m}})$ , by induction on $σ$ using the connective clauses. Hence $Mod (σ) = ⋃_{ε} C_{ε}$ , the union over those tuples $ε \in {F, T}^{m}$ making $σ$ true of the basic cylinder $C_{ε} = {v : v (A_{i_{j}}) = ε_{j}, 1 \leq j \leq m}$ . Each $C_{ε}$ is clopen (it fixes finitely many coordinates to clopen — indeed singleton — subsets of the discrete factors), and a finite union of clopen sets is clopen. $□$

Proposition 2 (compactness, topological proof). If every finite subset of $Σ$ is satisfiable, $Σ$ is satisfiable.

Proof. $2^{A}$ is compact by Tychonoff. The family ${Mod (σ) : σ \in Σ}$ consists of closed sets (Proposition 1). For finite $σ_{1}, \dots, σ_{n} \in Σ$ , a model $v$ of the finite set ${σ_{1}, \dots, σ_{n}}$ lies in $⋂_{j} Mod (σ_{j})$ , so the family has the finite intersection property. Compactness gives $⋂_{σ \in Σ} Mod (σ) \neq = \emptyset$ ; any member satisfies $Σ$ . $□$

Proposition 3 (compactness, König's-lemma proof, countable $A$ ). For countable $A = {A_{1}, A_{2}, \dots}$ , finite satisfiability of $Σ$ implies satisfiability.

Proof. Build a tree $T$ whose nodes at level $n$ are partial assignments $s : {A_{1}, \dots, A_{n}} \to {F, T}$ such that $Σ_{s} := Σ \cup {ℓ_{i}^{s} : 1 \leq i \leq n}$ is finitely satisfiable, where $ℓ_{i}^{s}$ is $A_{i}$ if $s (A_{i}) = T$ and $(\neg A_{i})$ otherwise; a node $s^{'}$ at level $n + 1$ extends a node $s$ at level $n$ when $s^{'} ↾ {A_{1}, \dots, A_{n}} = s$ . Each node has at most two children, so $T$ is finitely branching. $T$ is infinite: every level $n$ is nonempty, because finite satisfiability of $Σ$ supplies, for each finite $Δ \subseteq Σ$ , a model whose restriction to $A_{1}, \dots, A_{n}$ is a level- $n$ node keeping $Δ$ satisfiable, and a counting/finite-extension argument promotes this to a single level- $n$ node compatible with all finite $Δ$ . By König's lemma $T$ has an infinite branch; the union of the partial assignments along it is a total assignment $v$ . For any $σ \in Σ$ , the node at level $\geq$ (largest index in $σ$ ) keeps ${σ}$ satisfiable consistently with the chosen literals, so $\overset{v}{ˉ} (σ) = T$ ; hence $v$ satisfies $Σ$ . $□$

Proposition 4 (ultrafilter proof and equivalence with the Boolean prime ideal theorem). The ultrafilter lemma implies compactness; conversely compactness implies the Boolean prime ideal theorem.

Proof. ( $\Leftarrow$ ) Given finitely satisfiable $Σ$ , the classes $[[σ]]$ in $L_{A}$ have all finite meets nonzero (a finite subset's model witnesses $[[σ_{1} \land \dots \land σ_{n}]] \neq = ⊥$ ), so they generate a proper filter; an ultrafilter $U \supseteq F$ exists by the ultrafilter lemma, and the homomorphism $h : L_{A} \to 2$ with $h^{- 1} (T) = U$ gives $v (A_{i}) = h ([[A_{i}]])$ satisfying $Σ$ . ( $\Rightarrow$ ) Let $B$ be any Boolean algebra and $I$ a proper ideal; introduce a sentence symbol $p_{b}$ per $b \in B$ and the theory $Σ_{B}$ asserting that $b \mapsto \overset{v}{ˉ} (p_{b})$ is a homomorphism $B \to 2$ killing $I$ : clauses $(p_{b \lor c} \leftrightarrow (p_{b} \lor p_{c}))$ , $(p_{\neg b} \leftrightarrow (\neg p_{b}))$ , $p_{1}$ , $(\neg p_{0})$ , and $(\neg p_{b})$ for $b \in I$ . Every finite subset constrains a finite subalgebra on which a homomorphism to $2$ separating the relevant finite part of $I$ from $1$ exists (finite Boolean algebras are products of $2$ ), so $Σ_{B}$ is finitely satisfiable; a model is a homomorphism $B \to 2$ whose kernel is a prime ideal extending $I$ . $□$

Proposition 5 (de Bruijn-Erdős). For fixed $k$ , $G$ is $k$ -colourable iff every finite subgraph is.

Proof. Necessity is restriction. For sufficiency, take symbols $p_{v, c}$ ( $v \in V$ , $1 \leq c \leq k$ ) and the theory $Σ$ with $⋁_{c = 1}^{k} p_{v, c}$ for each $v$ (some colour), $(\neg (p_{v, c} \land p_{v, c^{'}}))$ for $c \neq = c^{'}$ (at most one colour), and $(\neg (p_{u, c} \land p_{v, c}))$ for $uv \in E$ , $1 \leq c \leq k$ (proper). A model assigns each $v$ exactly one colour with adjacent vertices distinct, a proper $k$ -colouring. A finite $Σ_{0} \subseteq Σ$ mentions finitely many vertices $V_{0}$ and edges among them, i.e. a finite subgraph $H$ ; a $k$ -colouring of $H$ (existing by hypothesis) satisfies $Σ_{0}$ . So $Σ$ is finitely satisfiable, hence satisfiable by Proposition 2, and its model is a $k$ -colouring of $G$ . $□$

Connections Master

Propositional logic as a formal system 42.01.01 pending supplies everything this unit presupposes: the inductively defined language, unique readability that makes $\overset{v}{ˉ}$ well defined, the semantic consequence relation $⊨$ , the Hilbert calculus with $⊢$ , and the soundness/completeness pair. That unit states sentential compactness as a single corollary (its Theorem 4); this unit owns the theorem in full, giving the topological, König's-lemma, and ultrafilter proofs, the de Bruijn-Erdős and linear-extension applications, and the location below the axiom of choice. The deductive proof here is the completeness theorem of 42.01.01 pending combined with the finiteness of deductions.
The compactness theorem for first-order logic, co-produced as 42.01.07 pending, is the deep counterpart: it runs the identical finite-intersection skeleton over spaces of complete types rather than the cube $2^{A}$ , but its harvest is qualitatively different — nonstandard models of arithmetic, the upward Löwenheim-Skolem theorem, the non-finite-axiomatisability of theories, and the existence of infinitesimals in nonstandard analysis. The connection matters because the propositional case isolates the topological mechanism (clopen constraints, finite intersection property, Stone duality) in a setting where the consequence relation is decidable, so that 42.01.07 pending can attribute its model-existence power precisely to the move from truth values to first-order structures, not to compactness itself.
Vertex colouring and the chromatic polynomial 40.04.06 is where the de Bruijn-Erdős theorem of Theorem 4 lives as a graph-theoretic statement: that unit develops finite chromatic number and Brooks' theorem, and the compactness argument here lifts those finite results to infinite graphs, certifying that infinite chromatic number is always witnessed on a finite subgraph. The connection is a genuine dependency — the infinite colouring theorem is proved by encoding the finite colouring theory of 40.04.06 as a propositional theory and applying compactness — not a topical coincidence.
The Stone space and Boolean algebra material that Theorem 3 invokes (the Lindenbaum-Tarski algebra, ultrafilters as $2$ -valued homomorphisms, the Stone duality between Boolean algebras and compact totally disconnected spaces) connects this unit to point-set topology's Tychonoff theorem and to the Boolean prime ideal theorem of set theory 42.01.07 pending; the compactness of the truth-assignment space is the propositional instance of Stone-space compactness, and the same duality reappears whenever a logical theory is studied through its space of models.

Historical & philosophical context Master

The compactness theorem for propositional logic emerged as a by-product of the metatheory of the sentential calculus in the 1920s and 1930s. Paul Bernays' work on the propositional calculus and the systematic treatment in Hilbert and Ackermann's Grundzüge der theoretischen Logik (1928) established the completeness of the calculus relative to truth-table semantics, from which the finitary character of consequence — the content of compactness — follows directly via the finiteness of deductions. The semantic statement was later isolated and proved independently of any calculus.

The topological reading is due to the development of Stone duality. Marshall Stone's 1936 representation theorem for Boolean algebras identified every Boolean algebra with the algebra of clopen sets of a compact totally disconnected space, its space of ultrafilters; under this duality the compactness of propositional logic is the compactness of the Stone space of the Lindenbaum-Tarski algebra ^{[Johnstone Ch. I-II]}. The exact set-theoretic strength was settled in the choice-principle literature: the Boolean prime ideal theorem, shown equivalent to the compactness theorem and to the Tychonoff theorem for Hausdorff spaces, was proved by J. D. Halpern and Azriel Lévy (1971) to be strictly weaker than the axiom of choice, exhibiting a permutation model of $ZF$ in which the prime ideal theorem holds and choice fails ^{[Jech Ch. 2]}. The combinatorial reach of the theorem was demonstrated by N. G. de Bruijn and Paul Erdős in 1951, who deduced the $k$ -colourability of infinite graphs from that of their finite subgraphs by exactly the compactness encoding given above ^{[de Bruijn-Erdős 1951]}.

Bibliography Master

@book{enderton2001logic,
  author    = {Enderton, Herbert B.},
  title     = {A Mathematical Introduction to Logic},
  edition   = {2},
  publisher = {Harcourt/Academic Press},
  year      = {2001}
}

@book{johnstone1982stone,
  author    = {Johnstone, Peter T.},
  title     = {Stone Spaces},
  series    = {Cambridge Studies in Advanced Mathematics},
  volume    = {3},
  publisher = {Cambridge University Press},
  year      = {1982}
}

@book{jech2003set,
  author    = {Jech, Thomas},
  title     = {Set Theory},
  edition   = {3, The Third Millennium Edition},
  series    = {Springer Monographs in Mathematics},
  publisher = {Springer},
  year      = {2003}
}

@article{debruijn1951colour,
  author  = {de Bruijn, N. G. and Erd\H{o}s, P.},
  title   = {A colour problem for infinite graphs and a problem in the theory of relations},
  journal = {Indagationes Mathematicae},
  volume  = {13},
  year    = {1951},
  pages   = {369--373}
}

@article{stone1936representation,
  author  = {Stone, Marshall H.},
  title   = {The theory of representations for Boolean algebras},
  journal = {Transactions of the American Mathematical Society},
  volume  = {40},
  number  = {1},
  year    = {1936},
  pages   = {37--111}
}

@article{halpernlevy1971boolean,
  author  = {Halpern, J. D. and L\'{e}vy, A.},
  title   = {The Boolean prime ideal theorem does not imply the axiom of choice},
  journal = {Proceedings of Symposia in Pure Mathematics},
  volume  = {13, Part I},
  year    = {1971},
  pages   = {83--134}
}

@book{hilbertackermann1928,
  author    = {Hilbert, David and Ackermann, Wilhelm},
  title     = {Grundz\"{u}ge der theoretischen Logik},
  publisher = {Springer},
  year      = {1928}
}

Prerequisites

42.01.01

Tier anchors

beginner: Enderton 2001 *A Mathematical Introduction to Logic* 2e (Harcourt/Academic Press) §1.2 and §1.7 (the compactness theorem read as 'satisfiable iff every finite chunk is satisfiable', with the colouring-of-an-infinite-map illustration before any topology); the finite-to-infinite reading of a list of constraints on true/false values
intermediate: Enderton 2001 *A Mathematical Introduction to Logic* 2e §1.7 (compactness for sentential logic stated and proved, both from completeness of the deductive calculus and by the König's-lemma / maximal-consistent-set route, with the de Bruijn-Erdős colouring application); Mendelson 2015 *Introduction to Mathematical Logic* 6e (CRC) §1.5
master: Enderton 2001 §1.7 in full together with the topological proof via Tychonoff; Johnstone 1982 *Stone Spaces* (Cambridge) Ch. I-II (the Stone space of a Boolean algebra, compactness as a topological statement); Jech 2003 *Set Theory* 3e (Springer) Ch. 2 and the Boolean-prime-ideal / ultrafilter material on the strength of compactness as a weak choice principle; de Bruijn-Erdős 1951 *Indag. Math.* 13 (the colouring theorem)

References

Enderton, H. B. — A Mathematical Introduction to Logic · 2nd edition, Harcourt/Academic Press (2001), Chapter 1, §1.7 ('Compactness and Effectiveness'). States the compactness theorem for sentential logic: a set Σ of well-formed formulas is satisfiable if and only if every finite subset of Σ is satisfiable; equivalently Σ ⊨ τ iff some finite Σ₀ ⊆ Σ has Σ₀ ⊨ τ. Gives two proofs: (i) the deductive route, satisfiable iff consistent (the completeness theorem of §1.7) and consistency is finitary because any deduction of a contradiction uses finitely many premises; (ii) a direct semantic route building a satisfying assignment one sentence symbol at a time, choosing each truth value so that finite satisfiability is preserved (a König's-lemma / finitely-branching-tree argument). Records the de Bruijn-Erdős consequence that an infinite graph is k-colourable iff every finite subgraph is, and the extension of a partial order to a total order, as applications, and contrasts the effectiveness of the propositional case with the first-order compactness theorem of Chapter 2.
Johnstone, P. T. — Stone Spaces · Cambridge Studies in Advanced Mathematics 3, Cambridge University Press (1982), Chapters I-II. Develops Stone duality between Boolean algebras and compact totally disconnected (Stone) spaces: the Stone space of a Boolean algebra B is the set of ultrafilters of B (equivalently 2-valued homomorphisms B → 2) topologised by the clopen sets b̂ = {ultrafilters containing b}. The space is compact, and this compactness is exactly the Boolean-algebraic content of the compactness theorem of propositional logic: the Lindenbaum-Tarski algebra of formulas modulo logical equivalence is a Boolean algebra whose Stone space is the space of truth assignments, and a satisfiable theory is one whose corresponding closed sets have the finite intersection property. The Boolean prime ideal theorem (every proper ideal of a Boolean algebra extends to a prime ideal) is equivalent over ZF to the compactness theorem and to the Tychonoff theorem for Hausdorff spaces.
Jech, T. — Set Theory · The Third Millennium Edition, Springer Monographs in Mathematics (2003), Chapters 2 and the choice-principle material. Treats the Boolean prime ideal theorem (BPI), the ultrafilter lemma (every filter on a set extends to an ultrafilter), and their equivalence, over ZF, with the compactness theorem of propositional logic and with the Tychonoff theorem for Hausdorff (specifically for products of finite/compact-Hausdorff) spaces. Establishes that BPI is strictly weaker than the full axiom of choice: AC implies BPI, but there are models of ZF + BPI in which AC fails (the basic Cohen and Halpern-Lévy permutation/symmetric models). The ultrafilter lemma suffices for the compactness theorem and for the existence of nonprincipal ultrafilters used in ultraproduct constructions, while full AC is not needed.
de Bruijn, N. G. and Erdős, P. — A colour problem for infinite graphs and a problem in the theory of relations · Indagationes Mathematicae 13 (1951), 369-373. Proves that for a fixed finite k, an infinite graph G is k-colourable if and only if every finite subgraph of G is k-colourable, assuming a suitable choice principle (the result is equivalent over ZF to the Boolean prime ideal theorem for general G). The proof encodes 'vertex v receives colour c' as propositional variables with clauses forcing each vertex exactly one colour and adjacent vertices distinct colours, then applies the compactness theorem: every finite subset of clauses involves finitely many vertices, hence a finite subgraph, which is k-colourable by hypothesis, so the finite subset is satisfiable; compactness yields a satisfying assignment, i.e. a colouring of all of G.

Estimated time

beginner: 18m
intermediate: 50m
master: 85m