5
$\begingroup$

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.

  • 1
    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.2012-04-09

2 Answers 2

5

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.

4

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$.

  • 0
    @CarlMummert, ah, makes sense, thanks.2012-04-09