(Mathematical logic:)

At first, this seems a perverse name for a theorem in logic. "Compactness" is a term from topology, not logic. Closer examination reveals a distinct similarity to the property of compactness. And, indeed, a proof of the compactness theorem manages to define a topology and use it.

Theorem. Let Φ be a set of propositions of some first order language. Suppose that every finite subset F⊆Φ is satisfiable (i.e., it leads to no contradiction). Then the entire set Φ is satisfiable.

In plain English, if Φ leads to a contradiction, then it has some finite subset that also leads to a contradiction. Or, given Godel's completeness theorem (no, not an incompleteness theorem, this is another kettle of formula), if every finite subset of Φ has a model, then Φ has a model.

Proofs of the compactness theorem are mostly technical and unenlightening. A handwaving proof comes from the first observation above: If Φ leads to some contradiction, then the derivation of the contradiction would "have to" use only finitely many propositions of Φ (since it is of finite length) -- but we're assuming Φ is finitely satisfiable.

This theorem is incredibly important. It does not hold in a useful form for second order logic, mostly because there is no completeness theorem there. Back in first-order logic, Robinson's non-standard analysis uses a parametrized version of compactness to prove results in the non-standard world. Even in "zero'th order logic" -- propositional calculus -- compactness is not completely trivial (although the handwaving proof above becomes more convincing).

Some relatively easy applications:

Logic

The following are true for any theory in first-order logic

• If a set Φ has arbitrarily large finite models, then it has an infinite model. This is an upwards Skolem-Löwenheim theorem.
• No proposition of first-order logic can express "the world is finite". And, since propositions can always be negated, no proposition of first-order logic can express "the world is infinite".

Algebra

Almost anything algebraic is a model. As just one example, every partial order can be extended to a total order.

Graph theory

The language of graph theory has a world of the graphs nodes, and contains a single relation, "aEb", that states "a is adjacent to b". To get graph theory, add the propositions "∀a.∀b.aEb → bEa" and "∀a.~(aEa)" to all sets Φ below (but the results hold without these axioms -- they're true of digraphs with cycles, too). Any graph is a model of the above axioms.

• There is no formula F(x,y) that says "x is connected to y". Since SQL is just first-order logic, it follows that it cannot express connectivity either, unless denormalized by adding extra tables! Connectivity is not expressible in first-order logic.
• If every finite subset of a graph can be k-coloured, then the entire graph can be k-coloured.

Here is one (non-constructive) proof of the compactness theorem for propositional calculus. I've seen constructive versions of this proof before, but they're boring and... constructive. And longer. I love Zorn's lemma too much for my own good.

First, some foundational work. A propositional calculus language contains an indefinite number of variables (named v_n, indexed by natural numbers) along with the connectives ¬ (negation) and ∧ (conjunction). The familiar connectives of propositional calculus can be built from these two alone.

A model in propositional calculus can be a sequence a_n that assigns a truth value to each variable v_n. A set of propositions is said to be satisfiable (or sat.) of such an assignment exists that makes each proposition true. If every finite set of a set of propositions is satisfiable, the whole set is said to be finitely satisfiable (or, for brevity's sake, fin. sat)

The compactness theorem says that a set of propositions Φ is sat. iff it is fin. sat.. Let's begin.

If Φ is sat., then it must be fin. sat. as well, trivially. If a finite piece of Φ didn't accept an assignment, then all of Φ wouldn't accept an assignment either.

Secondly, assume Φ is fin. sat. Let v_n be the (possibly infinite) set of all the variables mentioned in Φ. Establish the following partial order on sets of propositions over v_n:

α ≤ β iff α ⊆ β and α and β are fin. sat.

There are a couple issues with establishing this partial order, but these can be resolved. Let λ be the set of all propositions in v_n variables; this set is countably infinite since godel numbering puts it in one-to-one coorespondence with an infinite subset of the natural numbers.

Let α be a subset of λ and A be any proposition from λ such that A and ¬A aren't in α. Now, assume that both α ∪ A and α ∪ ¬A are not fin. sat. But the first condition means α can deduce ¬A, and the second means α can deduce A, so α alone can deduce A ∧ ¬A, meaning it is not fin. sat. as was assumed. This proves by contradiction that one of either α ∪ A or α ∪ ¬A is fin. sat. (but not both, obviously!)

This demonstrates that our partial order isn't empty. With the partial order, we can construct many chains of the form:

Φ ≤ ψ₁ ≤ ψ₂ ≤ ... ≤ ψ_k

For each chain, ψ_k is an upper bound, so by Zorn's lemma there exists a maximal, fin. sat. set of propositions, which I'll call λ'. λ' is complete, because otherwise there would be a proposition P such that either P or ¬P wasn't in λ'. From our construction of λ', we know that either λ'∪P or λ'∪(¬P) is fin.sat., and whichever one is fin.sat. is also "greater than but not equal to" λ' under the partial order — a contradiction.

From this we can define the following assignment:

a_n = true if v_n is in λ', false otherwise.

This is possible because λ', being complete, contains the one of 'v_n' or '¬v_n' for every variable mentioned in φ. This is why we proved the existence of λ', because we weren't assured that any sentence of the form 'v_n' were contained in Φ. In any case, since λ' also includes Φ, this assignment will satisfy Φ! That is, Φ is sat.!

This proves the compactness theorem in propositional calculus. •