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
- 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.