The <propositional compactness theorem> states that an arbitrary set $S$ of <propositional formulas> is satisfiable if and only if every finite <subset> of $S$ is satisfiable:
$$
\boxed{S\text{ has a model}\quad\Longleftrightarrow\quad
\text{every finite }S_0\subseteq S\text{ has a model}.}
$$
The satisfying <Boolean valuation> may depend on $S_0$ on the right; the conclusion on the left provides one <Boolean valuation> satisfying all of $S$ simultaneously.

Solution

Past exam of the computer science course of the University of Oxford / 2015 / Logic and proof / 1 / e / Solution

 Solution (source code)