Recall the two following fundamental theorems of mathematical logic:
Completeness Theorem: A theory T is syntactically consistent — i.e., for no statement P can the statement "P and (not P)" be formally deduced from T — if and only if it is semantically consistent: i.e., there exists a model of T.
Compactness Theorem: A theory T is semantically consistent iff every finite subset of T is semantically consistent.
It is well-known that the Compactness Theorem is an almost immediate consequence of the
Completeness Theorem: assuming completeness, if T is inconsistent, then one can deduce
"P and (not P)" in a finite number of steps, hence using only finitely many sentences of T.
The traditional proof of the completeness theorem is rather long and tedious: for instance, the book Models and Ultraproducts by Bell and Slomson takes two chapters to establish it, and Marker's Model Theory: An Introduction omits the proof entirely. There is a quicker proof due to Henkin (it appears e.g. on Terry Tao's blog), but it is still relatively involved.
On the other hand, there is a short and elegant proof of the compactness theorem using ultraproducts (again given in Bell and Slomson).
So I wonder: can one deduce completeness from compactness by some argument which is easier than Henkin's proof of completeness?
As a remark, I believe that these two theorems are equivalent in a formal sense: i.e., they are each equivalent in ZF to the Boolean Prime Ideal Theorem. I am asking about a more informal notion of equivalence.
UPDATE: I accepted Joel David Hamkins' answer because it was interesting and informative. Nevertheless, I remain open to the possibility that (some reasonable particular version of) the completeness theorem can be easily deduced from compactness.
Best Answer
There are indeed many proofs of the Compactness theorem. Leo Harrington once told me that he used a different method of proof every time he taught the introductory graduate logic course at UC Berkeley. There is, of course, the proof via the Completeness Theorem, as well as proofs using ultrapowers, reduced products, Boolean-valued models and so on. (In my day, he used Boolean valued models, but that was some time ago, and I'm not sure if he was able to keep this up since then!)
Most model theorists today appear to regard the Compactness theorem as the significant theorem, since the focus is on the models---on what is true---rather than on what is provable in some syntactic system. (Proof-theorists, in contast, may focus on the Completeness theorem.) So it is not because Completness is too hard that Marker omits it, but rather just that Compactness is the important fact. Surely it is the Compactness theorem that has deep applications (or at least pervasive applications) in model theory. I don't think formal deductions appear in Marker's book at all.
But let's get to your question. Since the exact statement of the Completeness theorem depends on which syntactic proof system you set up---and there are a huge variety of such systems---any proof of the Completeness theorem will have to depend on those details. For example, you must specify which logical axioms are formally allowed, which deduction rules, and so on. The truth of the Completness Theorem depends very much on the details of how you set up your proof system, since if you omit an important rule or axiom, then your formal system will not be complete. But the Compactness theorem has nothing to do with these formal details. Thus, there cannot be hands-off proof of Completeness using Compactness, that does not engage in the details of the formal syntactic proof system. Any proof must establish some formal properties of the formal system, and once you are doing this, then the Henkin proof is not difficult (surely it fits on one or two pages). When I prove Completeness in my logic courses, I often remark to my students that the fact of the theorem is a foregone conclusion, because at any step of the proof, if we need our formal system to be able to make a certain kind of deduction or have a certain axiom, then we will simply add it if it isn't there already, in order to make the proof go through.
Nevertheless, Compactness can be viewed as an abstract Completness theorem. Namely, Compactness is precisely the assertion that if a theory is not satisfiable, then it is because of a finite obstacle in the theory that is not satisfiable. If we were to regard these finite obstacles as abstract formal "proofs of contradiction", then it would be true that if a theory has no proofs of contradiction, then it is satisfiable.
The difference between this abstract understanding and the actual Completness theorem, is that all the usual deduction systems are highly effective in the sense of being computable. That is, we can computably enumerate all the finite inconsistent theories by searching for formal syntactic proofs of contradiction. This is the new part of Completness that the abstract version from Compactness does not provide. But it is important, for example, in the subject of Computable Model Theory, where they prove computable analogues of the Completeness Theorem. For example, any consistent decidable theory (in a computable language) has a decidable model, since the usual Henkin proof of Completeness is effective when the theory is decidable.
Edit: I found in Arnold Miller's lecture notes an entertaining account of an easy proof of (a fake version of) Completeness from Compactenss (see page 58). His system amounts to the abstract formal system I describe above. Namely, he introduces the MM proof system (for Mickey Mouse), where the axioms are all logical validities, and the only rule of inference is Modus Ponens. In this system, one can prove Completeness from Compactness easily as follows: We want to show that T proves φ if and only if every model of T is a model of φ. The forward direction is Soundness, which is easy. Conversely, suppose that every model of T is a model of φ. Thus, T+¬φ has no models. By Compactness, there are finitely many axioms φ0, ..., φn in T such that there is no model of them plus ¬φ. Thus, (φ0∧...∧φn implies φ) is a logical validity. And from this, one can easily make a proof of φ from T in MM. QED!
But of course, it is a joke proof system, since the collection of validities is not computable, and Miller uses this example to illustrate the point as follows:
And he then goes on to describe how one might construct Val, and give what amounts to a traditional proof of Completeness.