# Proof of compactness theorem

I wanted to prove the compactness theorem, p 79 Just/Weese:

The (i) <= (ii) direction is not obvious to me. I thought I could prove it by showing not (i) implies not (ii) as follows:

Assume $T$ does not have a model. Then for every $\varphi \in T$, $T \models \varphi$ and by completeness, $T \vdash \varphi$. That is, there is a finite sequence of $\varphi_i$, $i = 1, \dots n$, with $\varphi = \varphi_n$. (Unfortunately, these $\varphi_i$ are not necessarily all in $T$.) Since $T$ doesn't have a model, we also have $T \models \lnot \varphi$ and hence there are $\bar{\varphi}_i$, $i= 1, \dots m$ with $\bar{\varphi}_m = \lnot \varphi$, again, unfortunately these don't have to be in $T$. My proof then ended as follows: Then $\{\varphi, \lnot \varphi\}$ is a finite subset of $T$ that doesn't have a model.

Unfortunately, I can't assume that $\{\varphi, \lnot \varphi\}$ is a subset of $T$. At first I thought a theory automatically contained all provable formulas, too but that's not the case since the book defines a separate set for that on the same page:

Can someone show me how to fix my proof? Thank you.

Claim: If $T$ is a theory in a first-order language $L$ then $T$ has a model iff every finite subset $S$ of $T$ has a model.

Proof:

$\implies$: Assume $T$ has a model. Then this model is also a model of every subset of $T$.

$\Longleftarrow$: Assume $T$ does not have a model. Then every sentence $\varphi$ in $L$ is provable from $T$. Let $\varphi$ be any sentence in $T$. Then there is a proof of $\lnot \varphi$ from $T$, $\varphi_1' , \dots, \varphi_n' = \lnot \varphi$. Now let $S = T \cap \{ \varphi, \varphi_1' , \dots, \varphi_n' \}$. Then $S$ is a subset of $T$ and $\varphi$ and $\lnot \varphi$ are provable from it. To see that $\lnot \varphi$ is provable from $S$, observe that $\varphi_i'$ used in the proof are each either a sentence in $T$ or a consequence of such or a formula that is tautologically true. If $S$ is empty, that is, none of them are in $T$, then $\lnot \varphi$ is provable without $T$ and the claim holds. If there are any $\varphi_i' \in S$ then all of them are axioms of $T$ so that by definition, $\lnot \varphi$ is provable from $S$.

Now $S$ is a finite subset such that $S \vdash \varphi$ and $S \vdash \lnot \varphi$ that is, $S$ is an inconsistent theory and hence does not have a model.

You are almost on the right track. If $T$ does not have a model, then by Completeness $T \vdash \phi$ for all $\phi$ (not just those in $T$). In particular $T \vdash ( \forall x ) ( x = x )$ and $T \vdash \neg ( \forall x ) ( x = x )$. Consider formal proofs of these, and then look at the collection of formulae from $T$ that were used in either of these proofs.

• No formula in $T$ was used because these can be proved from the empty set? Nov 16, 2012 at 9:17
• @Matt: Perhaps look a bit closer at the formulae I wrote out. Especially the second one. (Note that if both could be proved from the logical axioms alone, then first-order logic would be inconsistent, and that would be a very bad thing.) Nov 16, 2012 at 9:21
• @Matt: I'm not saying that $S$ and $S^\prime$ will be subsets of $T$. But if $S$ and $S^\prime$ denote all of the formulae in these proofs, respectively, consider $T_0 = T \cap ( S \cup S^\prime )$. This is a subset of $T$, and you should be able to show that $T_0 \vdash ( \forall x ) ( x = x )$ and $T_0 \vdash \neg ( \forall x ) ( x = x )$. Nov 16, 2012 at 14:32
• @Matt: If $T_0 = \varnothing$ this means that no axioms from $T$ were used in either proof. This then means that for each proof every formula in that proof is either a logical axiom, or follows by some rule of inference from previous formulae. To me this is the very definition of provability from only the logical axioms! Nov 16, 2012 at 16:43
• @Matt: Note that $T_0$ only contains sentences from $T$ (since $T_0$ is the intersection of $T$ by some other set). Again, it is completely irrelevant whether $T_0$ is empty or not. But the final two sentences of your comment are the important points. The proofs that we have come up with for $\varphi$ and $\neg \varphi$ can be shown to have the property that each formula in them is either a logical axiom, a formula from $T_0$, or follows by some rule of inference from previous formulae. And this is exactly what we would mean by a formal proof from $T_0$. Nov 17, 2012 at 3:53