> From a type-theoretic perspective, a language can be either logically consistent by means of strong normalization xor Turing-complete.
This is a common misconception. A counter-example: take System F, add an `IO` monad, and add a function `fix : forall a. (a -> a) -> IO a` for general recursion. Our language is now Turing-complete, but remains consistent since any falsehoods produced by `fix` can't escape the `IO` type, e.g. you can prove `fix id : IO _|_`, but not `_|_`.
This is a common misconception. A counter-example: take System F, add an `IO` monad, and add a function `fix : forall a. (a -> a) -> IO a` for general recursion. Our language is now Turing-complete, but remains consistent since any falsehoods produced by `fix` can't escape the `IO` type, e.g. you can prove `fix id : IO _|_`, but not `_|_`.