ostap

graph TD;
        a1("Syntax")-->|Completeness| a2("Semantics");
        a2-->|Soundness| a1;

Syntax is often semantically-driven, which is why it’s easy to prove soundness. Completeness, however, is much, much more difficult.