Take the 2-minute tour ×
Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.

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.

share|improve this question

2 Answers 2

up vote 4 down vote accepted

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.

share|improve this answer
    
No formula in $T$ was used because these can be proved from the empty set? –  Matt N. Nov 16 '12 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.) –  Arthur Fischer Nov 16 '12 at 9:21
1  
@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 )$. –  Arthur Fischer Nov 16 '12 at 14:32
1  
@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! –  Arthur Fischer Nov 16 '12 at 16:43
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$. –  Arthur Fischer Nov 17 '12 at 3:53

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.

share|improve this answer
1  
Looks good from here! –  Arthur Fischer Nov 19 '12 at 14:18
    
@ArthurFischer Thank you for your help! –  Matt N. Nov 19 '12 at 14:21

Your Answer

 
discard

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.