Compactness theorem for propositional calculus - nice uses? The compactness theorem for propositional calculus states that a set of propositional sentences has a model (satisfying assignment) if and only if every finite subset of it has a model. I'm looking for uses of the theorem for something outside of logic that are simple enough to present without additional background.
An example is tiling, e.g. tiling of $\mathbb{Z}^2$ using Wang tiles. Given a set of Wang tiles one can introduce variables $X_{i,j}^k$ that means "Tile no. $k$ was placed in $(i,j)$". We now construct an infinite set of sentences saying that the assignment to the variables defines a legal tiling (i.e. for every $(i,j)$ exactly one $X_{i,j}^k$ is true, and we also check edge compatability). Now the compactness theorem can be used to prove that a set of tiles tiles the entire plane if and only if it tiles any finite zone in the plane.
Are there more uses in the same spirit?
 A: You can use the Compactness Theorem to show that a countable graph $G$ is $k$-colorable if and only if every finite subgraph of $G$ is $k$-colorable. A proof is explained here, but the general idea is clear, and it's almost easier to realize the solution than write it up.
You can also use the Compactness Theorem to introduce the notion of non-standard models of arithmetic, or the hyperreals. That is, you take the theory of $\mathbb{N}$ or $\mathbb{R}$ and adjoin the infinite family of sentences
$$ x > n$$
as $n$ ranges over $\mathbb{N}$ (here, $x$ is a new constant symbol). These sentences assert the existence of some value $x$ larger than every natural number. Since any finite subset of this theory is satisfiable (by interpreting $x$ as some sufficiently large number), the whole theory is satisfiable, and hence you get models with infinitesimal and/or unlimited elements. You can read more about nonstandard models of arithmetic here, and more on the hyperreals here, which naturally extends itself to studying non-standard analysis.
A: Suppose that you have a set $S$ of students and a set $C$ of classes. Each student will be assigned to just one class. Each student $s\in S$ has a finite list $C(s)\subseteq C$ of classes that he or she is willing to take, and each class $c\in C$ has a finite enrolment capacity $n_c$. For $T\subseteq S$, an acceptable course assignment is a function $f:T\to C$ such that 


*

*$f(t)\in C(t)$ for each $t\in T$, and  

*$\left|f^{-1}\left[\{c\}\right]\right|\le n_c$ for each $c\in C$.


(In other words, each student gets an acceptable class, and no class is oversubscribed.) 
The compactness theorem now easily implies that if each finite subset of $S$ admits an acceptable course assignment, then so does $S$. Probably the easiest way to model it is as a bipartite graph with parts $S$ and $C$, where each vertex in $S$ is to have degree $1$, each vertex $c\in C$ has degree no more than $n_c$ and for each $s\in S$ the unique edge adjacent to $s$ must terminate at one of the vertices in $C(s)$.
A: There is a very nice construction showing that every partial order can be extended to a total order using the propositional compactness theorem, see http://www.math.caltech.edu/~2010-11/3term/ma006c/Notes46c.pdf (Thanks to Brian M. Scott for an English version).
The proof works by assuming a given set $S$, and for each pair $a,b \in S$ of values, having a variable $L_{a,b}$ that stands for $a < b$. It is then easy to formalize the axioms of a total order and the existing partial order as a set of propositional formulas. Using compactness, one shows that the formula set is satisfiable, i.e., there is a total order.
