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)$.
The argument is basically correct, but it could stand to be fleshed out a bit. For convenience I’ll write $\mathbf{T}$ and $\mathbf{F}$ instead of $\text{TRUE}$ and $\text{FALSE}$. I’ll also write $m(p_k)=\mathbf{T}$ to indicate that $p_k$ is true in the model $m$.
Let $S_n$ be the set of all formulas in $S$ containing at most the propositional variables $p_1,\dots,p_n$. There is a finite set $E_n\subseteq S_n$ such that every formula in $S_n$ is equivalent to one in $E_n$, so $S_n$ has a model $m_n$. Note that for any $n\in\Bbb Z^+$, each model $m_k$ with $k\ge n$ assigns $p_n$ a truth value.
Let $N_1=\Bbb Z^+$. Each $m_n$ with $n\in N_1$ assigns $p_1$ a truth value. Let $T_1=\{n\in N_1:m_n(p_1)=\mathbf{T}\}$. If $T_1$ is infinite, set $m(p_1)=\mathbf{T}$, and let $N_2=\{k\in T_1:k\ge 2\}$. Otherwise, set $m(p_1)=\mathbf{F}$, and let $N_2=\{k\in N_1\setminus T_1:k\ge 2\}$. Note that in both cases $N_2$ is infinite, $m_k(p_1)=m(p_1)$ for all $k\in N_2$, and $m_k(p_2)$ is defined for each $k\in N_2$.
Now repeat the process. Let $T_2=\{n\in N_2:m_n(p_2)=\mathbf{T}\}$. If $T_2$ is infinite, set $m(p_2)=\mathbf{T}$, and let $N_3=\{k\in T_2:k\ge 3\}$. Otherwise, set $m(p_2)=\mathbf{F}$, and let $N_3=\{k\in N_2\setminus T_2:k\ge 3\}$. In both cases $N_3$ is infinite, $m_k(p_2)=m(p_2)$ for each $k\in N_3$, and $m_k(p_3)$ is defined for each $k\in N_3$.
For the general step, given an infinite $N_n\subseteq\Bbb Z^+$ such that $m_k(p_n)$ is defined for each $k\in N_n$, let $T_n=\{k\in N_n:m_k(p_n)=\mathbf{T}\}$. If $T_n$ is infinite, set $m(p_n)=\mathbf{T}$, and let $$N_{n+1}=\{k\in T_n:k\ge n+1\}\;.$$ Otherwise, set $m(p_n)=\mathbf{F}$, and let $$N_{n+1}=\{k\in N_n\setminus T_n:k\ge n+1\}\;.$$ As before, in both cases $N_{n+1}$ is by construction infinite, $m_k(p_n)=m(p_n)$ for each $k\in N_{n+1}$, and $m_k(p_{n+1})$ is defined for each $k\in N_{n+1}$, so the recursive construction can proceed.
This construction defines a model $m$ that assigns a truth value to each $p_k$. Take any formula $\varphi$ in $S$; it belongs to some $S_n$. Pick any $k\in N_{n+1}$; then $m_k$ is a model for $S_n$ and hence for $\varphi$. Moreover, the construction ensures that $m_k(p_i)=m(p_i)$ for $i=1,\dots,n$, so $m$ is also a model for $S_n$ and hence for $\varphi$.
Best Answer
It's clear that the compactness theorem reduces the completeness theorem to its finite case: "if a finite theory is consistent then it has a model".
In the propositional logic case, depending on the proof system you choose, that finite form can be relatively straightforward to prove, because a finite set $F$ of propositional formulas only mentions a finite number of variables, and so there are really only $2^n$ cases to consider where $n$ is the number of variables. Thus, for example, in a tableaux system the tree for a finite set of propositional formulas will be finite. In other proof systems, you might want to use a deductive rule such as $(A \to \phi) \to (\lnot A \to \phi) \to \phi$, applied $n$ times, once for each variable $A$ mentioned by the formulas, letting $\phi$ be $(\bigwedge F) \to \bot$. The point is the make the deduction essentially a proof by cases that considers all $2^n$ rows of a truth table for $F$.
This method does not work as well for first-order logic because, even if a theory has only a finite number of formulas, there are usually infinitely many terms to worry about. For example, in the tableaux setting, the tree can be infinite even if the theory is finite.