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.
 A: 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.
A: 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.
