Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. Join them; it only takes a minute:

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

Is there a quick way to prove the completeness theorem (every consistant theory has a model) from the compactness theorem (a theory has a model iff every finite subtheory of it has a model)? Usually the compactness theorem is a very easy result of the completeness theorem, but it can also be proved in other ways (e.g. using Tychonoff's theorem) and I wonder if this provides a "shortcut" to the completeness theorem.

I'm only asking about propositional calculus, but if the same holds for first order logic I'll be happy to hear it as well.

share|cite|improve this question
In the FOL versions both are equivalent to the Ultrafilter Lemma, as well to the Boolean Prime Ideal Theorem. In turn this is exactly Tychonoff's theorem for Hausdorff compact spaces. – Asaf Karagila Apr 9 '12 at 8:21
This is all very nice but without a reference/proof sketch it doesn't help me too much. – Gadi A Apr 9 '12 at 8:30
And that is why I used a comment and not an answer... When I had to teach the compactness theorem for propositional calculus earlier this year I was knee-deep in references. I cannot find any of them right now. I'll post an answer if I have something good. – Asaf Karagila Apr 9 '12 at 8:53

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.

share|cite|improve this answer

Here's a sketch of a proof you can find in R. Buss's "An introduction to proof theory". The interesting thing about it is that it's direct, in the sense that it doesn't create a model for a consistent theory but rather prove that logical consequence implies provability.

You want to prove that $\Gamma\models\phi$ then $\Gamma\vdash\phi$. Let's assume that $\Gamma\models\phi$. Using compactness this implies that a finite subset of $\Gamma$, $\{\psi_1,\ldots\psi_n\}\models\phi$, or equivalently $\models\psi_1\to(\psi_2\to\ldots(\psi_n\to\phi)\ldots)$. Hence you just need that tautologies are provable.

To show that, first you prove that given $\phi$, and $p_0,\ldots,p_n$ the atoms of $\phi$, if $f:n+1\to 2$ then $$(\lnot)^{f(0)}p_0,\ldots,(\lnot)^{f(n)}p_n\vdash\phi\textrm{ or } (\lnot)^{f(0)}p_0,\ldots,(\lnot)^{f(n)}p_n\vdash\lnot\phi$$ (where $(\lnot)^1=\lnot$ and $(\lnot)^0$ is nothing). You can do this by induction on the complexity of $\phi$, given some simple provable statements about connectives.

Now observe that if $\Gamma,\sigma\vdash\chi$ and $\Gamma,\lnot\sigma\vdash\chi$ then $\Gamma\vdash\chi$. Given a tautology $\phi$, by soundness you have that for every $f:n+1\to2$ it is the case that $(\lnot)^{f(0)}p_0,\ldots,(\lnot)^{f(n)}p_n\vdash\phi$. Then using the above remove the propositional atoms one by one to reach that $\vdash\phi$.

share|cite|improve this answer
This is a much better explanation of the $(A \to \phi) \to (\lnot A \to \phi) \to \phi$ technique I mentioned in the the answer I posted. – Carl Mummert Apr 9 '12 at 12:41
I am sorry, what does $f : n + 1 \to 2$ mean? – Daniil Apr 9 '12 at 12:49
@Daniil: it means that $f$ is a function from $\{0, \ldots, n\}$ to $\{0,1\}$. It is common in some areas to identify a natural number with the set of strictly smaller natural numbers. – Carl Mummert Apr 9 '12 at 13:25
@CarlMummert, ah, makes sense, thanks. – Daniil Apr 9 '12 at 15:07

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.