I have two, somewhat conflicting, views on this.

From the point of view of modern model theory, the Compactness Theorem is central to almost everything in the model theory of first order logic, while the Completeness Theorem is almost irrelevant. Completeness comes into play when proving the decidability of complete recursively axiomatized theories or in dealing with recursively saturated models for example, but these are not very central. Even when we want to apply Completeness, what's important is that the set of logical consequences of $T$ is recursively enumerable in $T$--the details of the proof system are of no importance whatsoever. This explains why in my model theory book, while I do explain that Compactness is an almost trivial consequence of Completeness, I give a direct Henkin-style proof.

Nevertheless, I view the Completeness Theorem as one of the great intellectual achievements of our subject. The fact that the semantic notion of logical consequence" can be captured by the syntactic notion of proof" is really surprising. The first is, a priori, $\Pi_1$ over the universe of sets, while the second is recursively enumerable. I find this amazing.

I have two, somewhat conflicting, views on this.

From the point of view of modern model theory, the Compactness Theorem is central to almost everything in the model theory of first order logic, while the Completeness Theorem is almost irrelevant. Completeness comes into play when proving the decidability of complete recursively axiomatized theories or in dealing with recursively saturated models for example, but these are not very central. Even when we want to apply Completeness, what's important is that the set of logical consequences of $T$ is recursively enumerable in $T$--the details of the proof system are of no importance whatsoever. This explains why in my model theory book, while I do explain that Compactness is an almost trivial consequence of Completeness, I give a direct Henkin-style proof.

Nevertheless, I view the Completeness Theorem as one of the great intellectual achievements of our subject. The fact that the semantic notion of "logical consequence" can be captured by the syntactic notion of "proof" is really surprising. The first is, a priori, $\Pi_1$ over the universe of sets, while the second is recursively enumerable. I find this amazing.