In logic, the **Compactness Theorem **states that a first-order theory is satisfiable if and only if it is finitely satisfiable. Here we give a sketch of a proof for the Theorem using Henkin construction. (The full proof is very syntax-heavy and I’m too lazy to type that much LaTeX, but this is the overall idea of the method.)

Let be a first-order language and be a finitely satisfiable -theory.

We can construct a language and a finitely-satisfiable -theory such that any -theory extending has the witness property. The way we do this is by first adding a constant symbol to for each -formula with a single free variable, calling the result . For each such we also add to the -sentence

,

calling the resulting -theory . We then keep doing this indefinitely and call the unions of all such languages and theories and , respectively, with the result that is finitely satisfiable and any extension thereof has the witness property.

We then extend to a finitely-satisfiable and *maximal* -theory which by the above will also have the witness property. The way we do this is by adding either or to for each -sentence (exactly one of which will keep the theory finitely satisfiable).

Now that we have an extended theory (within an extended language) which is finitely satisfiable, maximal, and has the witness property, we show there is a model of it, which will obviously also be a model of our original theory .

We define the universe of to be the set of constant symbols of modulo , where is the relation such that

.

We also define

,

,

where is a function symbol and is a relation symbol of .

We then proceed to show by induction on terms and formulas that

for all sentences . This shows that is a model of , and thus is a model of , which is what we wanted.