Proof of compactness theorem in first order logic - clarification My question is about this question and the users's answer to it.
Here's the statement of the compactness theorem: If $T$ is a first order theory in some language $L$.  The $T$ has a model if and only if every finite subset of $T$ has a model.
One direction $\implies$ is trivial.  The user proves the other direction as follows
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$. 
My questions are 
1.) Why is it clear that $\varphi$ is provable from $S$?
2.) If there are any $\varphi'_i \in S$, then why are all of them axioms of $T$?
 A: $S\vdash\varphi$ simply because $\varphi\in S$.
The axioms of $T$ are by definition the sentences in $T$. $S\subseteq T$, so every $\varphi_k'\in S$ is a sentence in $T$, i.e., an axiom of $T$. The $\varphi_k'$ that are not in $T$ are either provable from sentences in $T$ or tautologies.
A: *

*$\varphi$ is provable from $S$ since $\varphi$ is in $S$.


*Perhaps it was not clearly written out.  Since $T \vdash \neg \varphi$, we can consider a formal proof: $\varphi_1^\prime , \ldots , \varphi_n^\prime$ (where $\varphi_n^\prime$ is $\neg \varphi$).  Now consider $S^\prime = T \cap \{ \varphi_1^\prime , \ldots , \varphi_n^\prime \}$: these are the axioms from $T$ which were used in the above proof.  So it is really the definition of $\cap$ that ensure that each $\varphi_i^\prime$ belonging to $S$ (or in this write-up $S^\prime$) also belongs to $T$.
Note that the same formal proof gives us that $S^\prime \vdash \neg \varphi$.  Taking $S = S \cup \{ \varphi \}$ we have that $S \subseteq T$, and $S$ proves both $\varphi$ and $\neg \varphi$.
