I think this might be, because the definition seems to stem from mathematical notion of logic. And logicians usually want to have their logics sound, because if

I think this might be, because the definition seems to stem from mathematical notion of logic. And logicians usually want to have their logics sound, because if you can prove false statements, what is the point of your logic, right? So to distinguish between sound/unsound typesystem, I would look at it as if it were logic, where types are my theorems, and typechecking is attempt to find a proof. Of course, type-system for a language has to have some compromises, Java explicitly tells you, that even typechcecked program still will have runtime exceptions (like ClassCastException). In haskell you can still fall into an infinite loop, even though all the types flow through the system as expected :-)