"Valid" means, intuitively, that if I skip the compile-time type checks, and run the program with the types checked at runtime. If the type system is sound, and the compile-time type checks all pass, then it is impossible to hit a runtime type error. More formally, a program is valid if the execution within the operational semantics (basically, the semantics of running the program) do not lead to an error. This is distinct from type checking correctly.
Similarly, in formal logic "true" and "provable" are not equivalent. We'd like them to be, for sure, but the various incompleteness theorems ensure that we'll never be able to prove every possible true statement.
This tells me you've totally misunderstood my comment. More simply, "true" and "true" are equivalent, and "provable" and "provable" are equivalent. But while "valid" and "valid" are equivalent in the other definition, "typed" and "typechecked" are not.
> "program that typechecks" and "can be typed" are not [equivelent]
Sure. The above statement be more rigorous if it said 'has consistent types assigned to it by the type checker' and 'will be assigned consistent types when run through the type checker'.
[And, yes, every runtime ClassCastError demonstrates Java's type-checker's unsoundness, and a 'Sound Java' would have no need for the concept]
In the other one, the first phrase uses "program that typechecks" and "is valid"; the second phrase uses "valid program" and "can be typed". "is valid" and "valid program" are equivalent, but "program that typechecks" and "can be typed" are not.
So the two completeness/soundness definitions taken as a whole are not equivalent. That's what I was trying to get at with my example - it's not that the exception throws, but that the exception even exists.