There are many sources saying that the simply typed lambda calculus is strongly normalizing [(for instance, Wikipedia)][1] and hence not strong enough to be Turing-complete. Its strength is usually compared to propositional logic (I think intuitionistic).

However, it also seems to be well known that the simply typed lambda calculus is equivalent to "simple type theory," which is equivalent to higher order logic and hence has no sound, complete, effective proof system. For example, see the article "[Seven Virtues of Simple Type Theory][2]", which cites Godel's theorem and explicitly addresses the "virtue" that STT can create categorical theories (such as second-order PA).

How can these two things possibly both be true?

I thought the issue was with STT's "definite description" expression, which they use to define quantifiers -- however, the article in question cites a 1905 article by Bertrand Russell "[On Denoting][3]" showing it adds nothing to the expressive power of the theory.

What is the correct way of understanding this?


  [1]: https://en.wikipedia.org/wiki/Simply_typed_lambda_calculus
  [2]: https://www.sciencedirect.com/science/article/pii/S157086830700081X
  [3]: https://doi.org/10.1093/mind/XIV.4.479