> It’s important to understand that this is a big problem. If a type system is Turing complete, than it either has to be inconsistent or incomplete. In other words it either must allow type invalid programs through, or it must prevent some type valid programs (or both!).
No, you're mixing up concepts (consistency vs. soundness).
If a type system has non-normalizing types (or non-normalizing terms which appear in types), then it is inconsistent as a logic, which means that via Curry-Howard you can prove anything (ex falso quodlibet). Regarding incompleteness, any sufficiently expressive logic is incomplete per Gödel's first incompleteness theorem.
A type system which is inconsistent as a logic can still be sound as a type system. Soundness is the property that you described in your second paragraph (not letting "invalid" programs through). A simple example is System U. It's sound as a type system, but inconsistent as a logic. That means it works for programming, but not for proving.
No, you're mixing up concepts (consistency vs. soundness).
If a type system has non-normalizing types (or non-normalizing terms which appear in types), then it is inconsistent as a logic, which means that via Curry-Howard you can prove anything (ex falso quodlibet). Regarding incompleteness, any sufficiently expressive logic is incomplete per Gödel's first incompleteness theorem.
A type system which is inconsistent as a logic can still be sound as a type system. Soundness is the property that you described in your second paragraph (not letting "invalid" programs through). A simple example is System U. It's sound as a type system, but inconsistent as a logic. That means it works for programming, but not for proving.