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?

naturalexamples is a very good one. There are plenty of natural compact logics beyond first-order (the book Model-theoretic logics forms an excellent source on this point - while several chapters are quite technical, there are a number which focus on explicit natural examples), and I don't know if all of them are known to have an r.e. set of validities. $\endgroup$