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.

  • 1
    $\begingroup$ What is your definition of inconsistent? Also, could you add the statement of Henkin's Lemma? $\endgroup$ Commented Apr 26, 2020 at 11:16
  • $\begingroup$ +1 on what Taroccoesbrocco says. Also I am not sure what "enumerable" is doing there. This seems irrelevant and probably even wrong (there are many theories without an enumerable model, e.g. theories with only finite models, or only uncountable models). $\endgroup$ Commented Apr 26, 2020 at 11:20
  • 2
    $\begingroup$ @HarryRothschild Then your formulation of Henkin's Lemma is simply false. E.g. consider the language with a constant symbol for each element of $\mathbb{R}$ and the theory $\{a \neq b : a, b \in \mathbb{R}, a \neq b\}$. $\endgroup$ Commented Apr 26, 2020 at 11:22
  • 2
    $\begingroup$ @HarryRothschild To be clear, your proof idea will work. It is just that there are a few problems as you currently write it. And it is important to be precise. Certainly when there is the danger of circular reasoning (as there often is with this kind of proofs). $\endgroup$ Commented Apr 26, 2020 at 11:25
  • 1
    $\begingroup$ @HarryRothschild Have you noticed yet how every time you have used the terminology "enumerable" or "denumerable" on this site, someone has been confused by it? $\endgroup$ Commented Apr 26, 2020 at 13:21

1 Answer 1


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.

  • $\begingroup$ ⊥ What does this notation mean? $\endgroup$
    – user770683
    Commented Apr 26, 2020 at 11:44
  • 2
    $\begingroup$ @HarryRothschild It is the common symbol for "falsity" or "absurdity", the thing that is never true. Even if your definitions do not include this symbol, you can always 'build' it, for example as $\exists x(x \neq x)$. $\endgroup$ Commented Apr 26, 2020 at 11:46
  • $\begingroup$ @HarryRothschild - Or as $p \land \lnot p$ if you are in propositional logic. $\endgroup$ Commented Apr 26, 2020 at 12:03

You must log in to answer this question.