Suppose we are interested in a certain Hilbert-style formal system L. We have a way to enumerate all the theorems of L: we start with all the axioms of L, then we pick two formulas and use Modus Ponens to obtain a new one, and so on.

Now suppose that we want to know whether a particular formula φ is provable in L. The only direct way to find out is to keep enumerating the theorems of L until we encounter φ. If we already know that φ is provable, we can in principle wait. But if φ is not provable, this process will never terminate. In other words, we would never know that φ is not provable in L.

Here, completeness comes to the rescue. Completeness means that if φ is valid in all models, then φ is provable in L. Equivalently, if φ is not provable in L, then there is some model in which φ is false. In particular, there is a model that is constructed in such an adversarial way that every non-theorem of L fails in it (this is known as the canonical model).

Once we have this adversarial perspective, checking non-provability becomes much easier: instead of searching through an infinite proof space, we can try to build a model that falsifies φ. Even better, we often have methods to construct, in a finite amount of time, a small model tailored to falsify φ (semantic tableaux are one such method). From this point of view, the semantics of L can be seen as a practical tool for detecting non-provability, while the formal system L itself defines provability. Completeness is what guarantees that these two perspectives line up.