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.

$\endgroup$

2 Answers 2

Reset to default
5
$\begingroup$

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.

$\endgroup$
0
4
$\begingroup$

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.

$\endgroup$
10
  • $\begingroup$ No formula in $T$ was used because these can be proved from the empty set? $\endgroup$
    – Rudy the Reindeer
    Nov 16, 2012 at 9:17
  • $\begingroup$ @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.) $\endgroup$
    – user642796
    Nov 16, 2012 at 9:21
  • 1
    $\begingroup$ @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 )$. $\endgroup$
    – user642796
    Nov 16, 2012 at 14:32
  • 1
    $\begingroup$ @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! $\endgroup$
    – user642796
    Nov 16, 2012 at 16:43
  • 1
    $\begingroup$ @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$. $\endgroup$
    – user642796
    Nov 17, 2012 at 3:53

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .