Proof of the Compactness Theorem for Propositional Logic I have a problem understanding the proof for the compactness theorem for propositional logic in my logic course.
The compactness theorem states that there is a model for an infinite set $S$ of propositional formulas, if and only if, there is a model for every finite subset of $S$.
The following (quite lengthy) sketch of the proof was given to us in class:
The premise is that we have a model for each finite subset of $S$, so we need to construct from these models a model for the whole set $S$.
First we notice that for any (possibly infinite) set of formulas $S_n \subseteq S$ with $n$ propositional variables there are at max $2^{2^n}$ equivalent formulas with $n$ variables, which is finite. So for every finite equivalence class $E_n$ of $S_n$ there is a model $m_n$, which is also a model for the infinite $S_n$. Furthermore, $m_n$ is also a model for all sets $S_1 \subseteq S_2 \subseteq \cdots \subseteq S_{n-1}$.
Now, from all of the models $m_1, m_2, \ldots$ we derive a model $m$ for the whole set $S$. We start with an empty model $m=\{\}$. We then iterate over all the propositional variables $p_1, p_2, \ldots$ and assign a truth value to each and add them to $m$ as follows: We set $p_1 = \textrm{TRUE}$, if there are infinitely many sets $S_i$, whose model also assigns $\textrm{TRUE}$ to $p_1$. Now we delete all the sets $S_j$, in which $p_1 = \textrm{FALSE}$. Repeat for all $p_2, p_3, \ldots~$.
The proof goes on to proof that the so constructed model $m$ is in fact a model for $S$.
What I have problems with understanding is how we know that there are infinitely many models that assign some truth value to one of the variables. So, I don't find this proof convincing at all.
 A: The argument is basically correct, but it could stand to be fleshed out a bit. For convenience I’ll write $\mathbf{T}$ and $\mathbf{F}$ instead of $\text{TRUE}$ and $\text{FALSE}$. I’ll also write $m(p_k)=\mathbf{T}$ to indicate that $p_k$ is true in the model $m$.
Let $S_n$ be the set of all formulas in $S$ containing at most the propositional variables $p_1,\dots,p_n$. There is a finite set $E_n\subseteq S_n$ such that every formula in $S_n$ is equivalent to one in $E_n$, so $S_n$ has a model $m_n$. Note that for any $n\in\Bbb Z^+$, each model $m_k$ with $k\ge n$ assigns $p_n$ a truth value. 
Let $N_1=\Bbb Z^+$. Each $m_n$ with $n\in N_1$ assigns $p_1$ a truth value. Let $T_1=\{n\in N_1:m_n(p_1)=\mathbf{T}\}$. If $T_1$ is infinite, set $m(p_1)=\mathbf{T}$, and let $N_2=\{k\in T_1:k\ge 2\}$. Otherwise, set $m(p_1)=\mathbf{F}$, and let $N_2=\{k\in N_1\setminus T_1:k\ge 2\}$. Note that in both cases $N_2$ is infinite, $m_k(p_1)=m(p_1)$ for all $k\in N_2$, and $m_k(p_2)$ is defined for each $k\in N_2$.
Now repeat the process. Let $T_2=\{n\in N_2:m_n(p_2)=\mathbf{T}\}$. If $T_2$ is infinite, set $m(p_2)=\mathbf{T}$, and let $N_3=\{k\in T_2:k\ge 3\}$. Otherwise, set $m(p_2)=\mathbf{F}$, and let $N_3=\{k\in N_2\setminus T_2:k\ge 3\}$. In both cases $N_3$ is infinite, $m_k(p_2)=m(p_2)$ for each $k\in N_3$, and $m_k(p_3)$ is defined for each $k\in N_3$.
For the general step, given an infinite $N_n\subseteq\Bbb Z^+$ such that $m_k(p_n)$ is defined for each $k\in N_n$, let $T_n=\{k\in N_n:m_k(p_n)=\mathbf{T}\}$. If $T_n$ is infinite, set $m(p_n)=\mathbf{T}$, and let $$N_{n+1}=\{k\in T_n:k\ge n+1\}\;.$$ Otherwise, set $m(p_n)=\mathbf{F}$, and let $$N_{n+1}=\{k\in N_n\setminus T_n:k\ge n+1\}\;.$$ As before, in both cases $N_{n+1}$ is by construction infinite, $m_k(p_n)=m(p_n)$ for each $k\in N_{n+1}$, and $m_k(p_{n+1})$ is defined for each $k\in N_{n+1}$, so the recursive construction can proceed.
This construction defines a model $m$ that assigns a truth value to each $p_k$. Take any formula $\varphi$ in $S$; it belongs to some $S_n$. Pick any $k\in N_{n+1}$; then $m_k$ is a model for $S_n$ and hence for $\varphi$. Moreover, the construction ensures that $m_k(p_i)=m(p_i)$ for $i=1,\dots,n$, so $m$ is also a model for $S_n$ and hence for $\varphi$.
A: Either your construction is a bit off or I don't understand it.  Does it not claim it constructs a model S' in the following setup: Let $S$ be any arbitrary set of propositional formulas, let $p$ be a fresh symbol not appearing in $S$, and let $S' = \{p\} \cup \{\lnot p \land \phi | \phi \in S\}$.  I think if you apply your construction, you could get $S_1 = \{p\}$, then $m_1$ sets the $p$ to true, the rest of $S'$ is promptly thrown away (or "deleted"), every other variable can then safely be set to true, and $S'$ is satisfied by setting everything to true. Something is rotten here.
There are a lot of proofs online you can try examining. This proof is rather jargon free.
A: Isn't a simpler way to prove the compactness theorem using the following moduls tollens proof?
One direction is trivial since if $\Sigma$ is satisfiable, then certainly $\Sigma_0 \subseteq \Sigma$ is satisfiable for some finite $\Sigma_0$. 
For the other direction, say $\Sigma$ is a set of sentences that is not satisfiable. Then, by the completeness theorem, there exists a finite subset of that set that is inconsistent $-$ i.e.,  $\exists \  \Sigma_0 \subseteq \Sigma$ such that $\Sigma_0$ is finite and proves a proposition of the form $P \ \& \sim P $. So $\Sigma_0$ must not be satisfiable. 
Or am I missing something here?
