It is well-known that the simply typed lambda calculus is strongly normalizing [(for instance, Wikipedia)][1]. Hence, it is not strong enough to be Turing-complete, as also mentioned on the Wikipedia page for [Turing-completeness][2]. Its strength is usually compared to propositional logic (I think intuitionistic), and one way to show this is the Curry-Howard Correspondence.

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][3]", 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? What is the correct way of understanding this?

  [1]: https://en.wikipedia.org/wiki/Simply_typed_lambda_calculus
  [2]: https://en.wikipedia.org/wiki/Turing_completeness#Non-Turing-complete_languages
  [3]: https://www.sciencedirect.com/science/article/pii/S157086830700081X