Verification for Proof of Compactness Theorem

compactnesslogicmodel-theorysolution-verification

How's this for a proof?

Assume every finite subset of $\Gamma$ has a model but $\Gamma$ has no model. Then $\Gamma$ has no enumerable model and by Henkin Lemma, $\Gamma$ is inconsistent. So by definition of inconsistency, there's some sentence $\varphi$ s.t. $\Gamma \vdash \varphi$ and $\Gamma \vdash \neg\varphi$. Since derivations are finite, this inconsistency arose from some finite $\Delta \subseteq \Gamma$, so we have $\Delta \vdash \varphi$ and $\Delta \vdash \neg\varphi$. So some $\Delta$ is inconsistent and by Soundness Theorem, $\Delta$ is also unsatisfiable and so has no model. But every finite $\Delta \subseteq \Gamma$ has a model. So this then contradicts our assumption. Therefore $\Gamma$ is consistent, and by Henkin Lemma, has a model.

Henkin's Lemma: If a set of sentences is consistent, then it has an enumerable model.

Best Answer

The general idea of the proof is right, and is basically how we prove compactness once we have completeness and soundness. Let's first make a few definitions and state some results to be clear what we are talking about.


As usual, for a theory $\Gamma$, the notation $\Gamma \vdash \varphi$ means there exists a formal derivation of $\varphi$ from $\Gamma$ (with respect to some classical proof system, it does not really matter which one). The notation $\Gamma \models \varphi$ means that $\varphi$ is valid in all models of $\Gamma$.

Definition. A theory $\Gamma$ is formally consistent if $\Gamma \not \vdash \bot$.

So $\Gamma$ is formally inconsistent if $\Gamma \vdash \bot$, which is equivalent to $\Gamma \vdash \varphi$ and $\Gamma \vdash \neg \varphi$ for some formula $\varphi$ (this is just to link this definition to what is used in the question).

Henkin's lemma. If $\Gamma$ is formally consistent, then it has a model.

Soundness theorem. If $\Gamma \vdash \varphi$, then $\Gamma \models \varphi$.

Completeness theorem. If $\Gamma \models \varphi$, then $\Gamma \vdash \varphi$.

Proof. We can actually easily prove the completeness theorem from Henkin's lemma (fair note: Henkin's lemma is far from trivial to prove). We will prove the contraposition, so suppose $\Gamma \not \vdash \varphi$. Then $\Gamma \cup \{\neg \varphi\}$ is formally consistent. By Henkin's lemma there is then a model of $\Gamma \cup \{\neg \varphi\}$. This is then in particular a model of $\Gamma$ where $\varphi$ is not valid, so $\Gamma \not \models \varphi$, as required.


Now we can prove compactness from soundness and completeness. Personally I like this proof because it gives a great intuition as to why the compactness theorem is true. Once we accept that semantics (i.e. "$\models$") and provability (i.e. "$\vdash$") coincide, then we can say that any contradiction must be derivable. Since derivations are finite it must be derivable from a finite set of assumptions. Let's make this precise.

Compactness theorem. If every finite subset of a theory $\Gamma$ has a model, then $\Gamma$ has a model.

Proof. Suppose not. So $\Gamma$ has no model, but every finite subset does have a model. Since $\Gamma$ has no model, we have (vacuously) $\Gamma \models \bot$. So by completeness $\Gamma \vdash \bot$ (alternatively: by the contraposition of Henkin's lemma). Since (formal) derivations are finite, there must be a finite subset $\Delta \subseteq \Gamma$ such that $\Delta \vdash \bot$. By soundness $\Delta \models \bot$, and as no model can satisfy $\bot$ we see that $\Delta$ has no models. This contradicts our assumption that every finite subset of $\Gamma$ has a model, so we conclude that $\Gamma$ must have a model.

Related Question