Propositional Calculus: Compactness implies Completeness? Is there a quick way to prove the completeness theorem (every consistant theory has a model) from the compactness theorem (a theory has a model iff every finite subtheory of it has a model)? Usually the compactness theorem is a very easy result of the completeness theorem, but it can also be proved in other ways (e.g. using Tychonoff's theorem) and I wonder if this provides a "shortcut" to the completeness theorem.
I'm only asking about propositional calculus, but if the same holds for first order logic I'll be happy to hear it as well.
 A: It's clear that the compactness theorem reduces the completeness theorem to its finite case: "if a finite theory is consistent then it has a model". 
In the propositional logic case, depending on the proof system you choose, that finite form can be relatively straightforward to prove, because a finite set $F$ of propositional formulas only mentions a finite number of variables, and so there are really only $2^n$ cases to consider where $n$ is the number of variables. Thus, for example, in a tableaux system the tree for a finite set of propositional formulas will be finite. In other proof systems, you might want to use a deductive rule such as $(A \to \phi) \to (\lnot A \to \phi) \to \phi$, applied $n$ times, once for each variable $A$ mentioned by the formulas, letting $\phi$ be $(\bigwedge F) \to \bot$.  The point is the make the deduction essentially a proof by cases that considers all $2^n$ rows of a truth table for $F$. 
This method does not work as well for first-order logic because, even if a theory has only a finite number of formulas, there are usually infinitely many terms to worry about. For example, in the tableaux setting, the tree can be infinite even if the theory is finite. 
A: Here's a sketch of a proof you can find in R. Buss's "An introduction to proof theory". The interesting thing about it is that it's direct, in the sense that it doesn't create a model for a consistent theory but rather prove that logical consequence implies provability.
You want to prove that $\Gamma\models\phi$ then $\Gamma\vdash\phi$. Let's assume that $\Gamma\models\phi$. Using compactness this implies that a finite subset of $\Gamma$, $\{\psi_1,\ldots\psi_n\}\models\phi$, or equivalently $\models\psi_1\to(\psi_2\to\ldots(\psi_n\to\phi)\ldots)$. Hence you just need that tautologies are provable.
To show that, first you prove that given $\phi$, and $p_0,\ldots,p_n$ the atoms of $\phi$, if $f:n+1\to 2$ then $$(\lnot)^{f(0)}p_0,\ldots,(\lnot)^{f(n)}p_n\vdash\phi\textrm{   or    } (\lnot)^{f(0)}p_0,\ldots,(\lnot)^{f(n)}p_n\vdash\lnot\phi$$ (where $(\lnot)^1=\lnot$ and $(\lnot)^0$ is nothing). You can do this by induction on the complexity of $\phi$, given some simple provable statements about connectives.
Now observe that if $\Gamma,\sigma\vdash\chi$ and $\Gamma,\lnot\sigma\vdash\chi$ then $\Gamma\vdash\chi$. Given a tautology $\phi$, by soundness you have that for every $f:n+1\to2$ it is the case that $(\lnot)^{f(0)}p_0,\ldots,(\lnot)^{f(n)}p_n\vdash\phi$. Then using the above remove the propositional atoms one by one to reach that $\vdash\phi$. 
