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.

  • 0
    No formula in $T$ was used because these can be proved from the empty set?2012-11-16
  • 0
    @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.)2012-11-16
  • 0
    True. I must have misremembered the rule $a \lor \lnot a, a, \lnot a$. But from the empty set we can prove $x = x$ and from that $\forall x (x = x)$. Right?2012-11-16
  • 0
    @Matt: That one can be proved using logical axioms alone is immaterial. I could have chosen sentences $( \forall x ) ( \forall y ) ( x = y )$ and $\neg ( \forall x ) ( \forall y ) ( x = y )$. The main point is that they each have proofs from $T$, that proofs are _finite_, and that any theory proving both must be inconsistent.2012-11-16
  • 0
    Ok. Let's assume that we can prove each using $S = \{\varphi_1, \dots, \varphi_n\}$ and $S' = \{ \bar{\varphi}_1, \dots, \bar{\varphi}_n \}$, respectively. Then neither $S$ nor $S'$ are subsets of $T$. How do I proceed from there?2012-11-16
  • 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 )$.2012-11-16
  • 0
    Say $T_0 = \varnothing$. Does it then follow that $\varphi$ and $\lnot \varphi$ are provable from the logical axioms? I think yes but I don't know how to prove it.2012-11-16
  • 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!2012-11-16
  • 0
    Ok. Is this correct: The elements in $T_0 = T \cap (S \cup S')$ are either axioms (sentences in $T$) or things deduces from such. If $T_0$ does not contain any axioms then neither do $S,S'$ and hence $\varphi, \lnot \varphi$ can be deduced from $\varnothing \subset T$. If $T_0$ contains axioms then $\varphi, \lnot \varphi$ can be deduced from these axioms. Hence $T_0 \subset T$ is a finite subset of $T$ from which $\varphi, \lnot \varphi$ can be deduced and which therefore does not have a model.2012-11-16
  • 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$.2012-11-17
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.