The definitions are relevant to a Logical system and can be extended to Formal mathematical theories.
See the Wiki's page (some lines below your quote):
Soundness of a deductive system is the property that any sentence that is provable in that deductive system is also true on all interpretations or structures of the semantic theory for the language upon which that theory is based. Strong soundness of a deductive system is the property that any sentence P of the language upon which the deductive system is based that is derivable from a set Γ of sentences of that language is also a logical consequence of that set.
if provable, then valid.
The converse of that definition is that of completeness:
A deductive system with a semantic theory is strongly complete if every sentence P that is a semantic consequence of a set of sentences Γ can be derived in the deduction system from that set.
if valid, then provable.
Informally, a soundness theorem for a deductive system expresses that all provable sentences are true. Completeness states that all true sentences are provable.
In formal system, a "proof" is a formal proof (aka: derivation).
A falsifying interpretation can be useful as a counterexample, to prove that a formula is invalid, isn't it?
Correct. In propositional logic we have the truth table method that can be applied to every formula to verify (in a finite number of steps) if the formula is valid or not. A single row in the truth table that "outputs" FALSE is enough to show that the formula is invalid.
In the same way, truth tree method will produce a counterexample, if any, showing the invalidity of the formula.
Having found a counterexample, we apply soundness ("if provable, then valid") to conclude that the formula (being not valid) is not derivable in the calculus.
The discussion above id related to the decidability topic.
In propositional logic we have the method of truth table that can be used to verify (in a finite number of steps) for every formula if the formula is valid or not.
A corresponding method is not available for first-order logic. This means that, completeness ensures that if formula P is valid then we have a prove of it.
But we have no general method to verify in advance if P is valid or not.
This means that validity if FOL is not decidable.
See also the post: How is First Order Logic complete but not decidable?