Taxonomy of proofs of compactness in propositional logic I know of two proofs of compactness in propositional logic, one which is a very fast use of Tychonoff's theorem.  The other takes a very long tour through several lemmas, but sticks to strictly propositional logic flavored statements.  For reference, I have in mind the sort of proof in the first chapter of Hinman's book Fundamentals of Mathematical Logic.
But I could swear that a few years ago I saw some blog post or discussion of a different way of proving compactness, which sounded much better than these other two.  I believe someone said "Usually you prove compactness to prove completeness, but in fact you can prove completeness first.  It's a little bit of extra work on the completeness proof, but then it makes the proof of compactness much faster, and does not require any reference to Topology."
Does anyone know about this other style of proof for the compactness theorem and where I might find it?  I may not have even the rough details correct since I am working from a dim memory of this thing I read.  So perhaps even a description of a few of the most popular proofs of compactness would be illuminating for me.
I have seen others say that compactness follows quickly from completeness, so I guess really the question is just: How do you prove completeness without compactness, and in such a way that it's actually nicer doing it this way than it is proving everything the usual way (i.e. first compactness then completeness)?
 A: Not that it matters, but it's not clear to me that compactness first is really the "usual" way - I for example didn't learn about it until long after I'd learned the completeness theorem.
Anyway, completeness implies compactness very easily.


Compactness Theorem. If $S$ is a set of formulas of propositional logic and  every finite subset of $S$ is satisfiable then $S$ is satisfiable.


Proof: Assume $S$ is not satisifiable. The completeness theorem shows that $S$ is inconsistent: there exists $p$ such that $$S\vdash p\land\lnot p.$$Since a proof is finite by definition it can use only finitely many elements of $S$. So there exists a finite set $F\subset S$ with $$F\vdash p\land\lnot p;$$in particular, $F$ is not satisfiable.
A: Completeness is a statement about the proof system at hand, so you can’t prove it without getting into its grotesque details. Compactness trivially follows from it due to the finiteness of proofs. If you want such a proof of completeness(using the Hilbert system), see for instance Enderton’s logic book. But the main point is that compactness is actually a simpler theorem than completeness. If you want a slick (non-topological) proof of compactness then (for the countable case at least) you can apply König’s lemma. For the uncountable case see Andreas Blass’s answer here: Is there a "tree-like" proof of compactness theorem in the case of uncountably many variables? which generalises the countable proof using transfinite induction.
