In the section 6 of Programming Languages course, Dan Grossman discussed about the soundness and the completeness of the type system. He said that:

• A type-system is sound implies that all of type-checked programs are correct (in the other words, all of the incorrect program can't be type checked), i.e. there won't be any false negative [1].
• A type-system is complete implies that all of the correct program can be accepted by the type checker, i.e. there won't be any false positive [2].

With this explanation, I have better understanding to the soundness and the completeness of the logic system. In the logic system, we would say that:

• A logic system is sound means that all provable statements are true in models [3].
• A logic system is complete means that all statements which are true in all models are provable [3].

Besides, according to Godel's incompleteness theorems, if your system is expressive enough to represent natural numbers, then it can't be both sound and complete. This theorem applies to the type system as well. Usually, most programming language would prefer soundness over completeness, since false negative will result in bad consequence.

Edit (01/31/2023): In the earlier version, I incorrectly mentioned false positive in the last sentence. It should be false negative. The text has been updated. Special thanks to Yuk Lam Sung for pointing this out to me.