I am interested in the relationship between completeness and compactness of formal logical systems. I think it is pretty well known that if an effective proof system can be developed for a formal semantics, then that semantics must have the compactness property. In a slogan: "Completeness implies compactness".
But what about the other way? Is it possible for a formal semantics to have the compactness, but with respect to which an effective proof system which sound&complete cannot be produced?
If such a system could be produced, this would represent a counter example to the slogan "Compactness implies completeness".
Thus my question is: While compactness and completeness are clearly not identical properties (completeness involves proof theoretic notions, like computability), are they extensionally equivalent over formal systems?