5
$\begingroup$

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

enter image description here

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:

enter image description here

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

2 Answers 2

4

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.

  • 1
    @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$.2019-04-13
4

Thank you for your help, Arthur, I decided to add my finished proof to this thread:

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.