Finite witnesses, infinite consequences
If every finite piece of an infinite list of axioms can be satisfied, so can the whole list. That one fact conjures up infinitely large numbers and colors infinite graphs.
Press Add Axiom to grow a theory of dense linear orders one axiom at a time. Watch the models column: every finite batch of axioms so far still has a model.
Build a theory of dense linear orders one axiom at a time. Every finite subset has a model -- so by compactness, the entire infinite theory has a model.
∀x ∀y ∀z ((x < y ∧ y < z) → x < z)
Transitivity
∀x ∀y (x < y ∨ x = y ∨ y < x)
Totality
∀x ¬x < x
Irreflexivity
∀x ∀y (x < y → ∃z (x < z ∧ z < y))
Density
∀x ∃y (x < y)
No maximum
∀x ∃y (y < x)
No minimum
c₀ ≠ c₁
At least 2 elements
c₂ ≠ c₀ ∧ c₂ ≠ c₁
At least 3 elements
c₃ ≠ c₀ ∧ c₃ ≠ c₁ ∧ c₃ ≠ c₂
At least 4 elements
The Compactness Theorem is one of the most powerful results in model theory: a set of first-order sentences has a model if and only if every finite subset has a model. In other words, if you cannot derive a contradiction from any finite collection of your axioms, then the entire infinite collection is consistent -- it has a structure that makes all the sentences simultaneously true.
The name "compactness" comes from topology: the space of all complete theories (the Stone space) is compact, and the theorem is equivalent to this topological fact. But its consequences are purely algebraic and combinatorial. It lets us build exotic structures -- non-standard models of arithmetic with infinitely large numbers, infinitesimal elements in analysis, and colorings of infinite graphs -- by reducing infinite consistency to finite consistency.
The theorem can be proved via the Completeness Theorem (Gödel) or via ultraproducts. Either way, the key insight is the same: first-order logic cannot "see" the difference between a very large finite set and an infinite one, and this blindness is precisely what gives the theorem its power.
Key insight: You never need to check infinitely many axioms at once. The Compactness Theorem tells us that if no finite subset leads to a contradiction, neither does the whole theory. This shifts the burden of proof from the infinite to the finite.
Keep pressing Add axiom to demand c > 0, c > 1, c > 2, and so on; each time a big enough number works. Once all the axioms are in, drag the zoom slider across the infinite gap to the non-standard part.
Start with the standard model N = { 0, 1, 2, 3, ... } and add a new constant c that must be greater than every standard number. Every finite subset of these axioms has a model -- by compactness, so does the whole theory.
Standard model N
Add a new constant c to the language of arithmetic, together with axioms c > 0, c > 1, c > 2, and so on. Every finite subset of these axioms has a model in the standard naturals -- just interpret c as a large enough number. By compactness, the full theory has a model containing a "non-standard" element larger than every standard number.
Key insight: The non-standard model satisfies every first-order sentence that the standard naturals satisfy, yet it contains elements that are "infinitely large." This shows that first-order logic cannot pin down the natural numbers uniquely -- there are always non-standard models lurking, and compactness is what conjures them into existence.
Add vertices, click one vertex and then another to join them with an edge, choose the number of colors k, and press Color Graph to see a proper coloring.
Build a graph and choose k colors. If every finite subgraph is k-colorable, compactness guarantees the entire (even infinite) graph is k-colorable. Click a vertex to select it, then click another to add an edge.
The Compactness Argument
For each vertex v, introduce a sentence saying "v has one of the k colors." For each edge (u, v), add "u and v have different colors." Any finite subset of these sentences involves only finitely many vertices -- a finite subgraph -- which is k-colorable by assumption. By compactness, the entire infinite set of sentences has a model: a valid k-coloring of the full graph.
Compactness has a beautiful application to combinatorics: if every finite subgraph of an infinite graph can be properly colored with k colors, then the entire infinite graph can be k-colored.
Key insight: This result -- sometimes called the De Bruijn-Erdős theorem -- reduces an infinite combinatorial problem to finitely many finite ones. The trick is to encode "vertex v has color i" and "adjacent vertices have different colors" as first-order sentences, then invoke compactness.
Spot a mistake or have an idea?