Why do we need formal semantics for predicate logic? Consider this question solved. I will not pick a best answer as all of them have contributed to my understanding of the topic.

Im unsure what benefit we have by formally defining the semantics of predicate logic. But I do see value in having a formal proof calculus. My point is that we would not need formal semantics to justify the inference rules of proof calculi. 

We could define a calculus that mimicks the "laws of thought", i.e. the rules of inference that have been used by mathematicians for hundreds of years to proof their theorems. Such a calculus already exists: natural deduction. Then we would define this calculus to be sound and complete.  

This can be justified by realising that the formal semantics of predicate logic is just a model. The appropriateness of the model can only be justified intuitively. Thus, by showing that natural deduction is sound and complete with reference to the formal semantics does not make natural deduction more "true". It would be just as good if we would directly justify the rules of natural deduction intuitively. The detour using formal semantics gives us nothing.

Then, having defined natural deduction to be sound and complete, we could show the soundness and completeness of other calculi by showing that the proofs they produce can be translated to natural deduction and vice versa.

Are my reflections above correct?
Why is it important to prove the soundness and completeness of proof calculi by reference to formal semantics?
A minor comment, and a more serious answer. 

First, it doesn't make sense to declare a natural deduction system complete by fiat. Natural deduction is interesting precisely because it has a natural internal notion of consistency and/or completeness -- namely, cut-elimination. This is a fantastic theorem, and IMO fully justifies attempts to give purely proof-theoretic semantics (and by the CH correspondence, it likewise justifies the use of operational methods in programming language semantics). But this is interesting precisely because it offers a more refined notion of getting the logic right than consistency. Taking the proof theoretic road means you'll have to do more work, but in exchange you get stronger results.

However, it happens that sometimes the logic per se takes a secondary role. We may begin with a (family of) models, and then look for ways of talking syntactically about them, using a logic. The soundness and completeness of a logic with respect to a family of models indicates that the logic really does capture everything both interesting and true you can say about the class of models. A concrete example of when models are more interesting than the logical theories occurs in program analysis and model checking. There, the usual thing to do is to take your model to be the execution of a program, and the logic to be some fragment of temporal logic. The propositions you can say in these languages are (deliberately) not terribly exciting -- e.g., null pointer dereferences never occur -- but it's the fact that it applies to actual program runs that gives it interest.