[eli_gottlieb]

From a type-theoretic perspective, a language can be either logically consistent by means of strong normalization xor Turing-complete. The untyped lambda calculus is the smallest, most elegant functional language on the right half of that fork. It's also not strongly normalizing, so you can't prove theorems with it -- oh well!

[YellPika]

> 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 `_|_`.

[eli_gottlieb]

Fair enough, and that's been one of the approaches to paraconsistency and inconsistency in modal logic, too. Of course, from a theorem-proving perspective, it's utterly useless, as with a proof-checker, at some point I need to escape the monadic container and get back into `Prop`.