Revision 995566cf-ff15-4642-86d8-00a87645cc27

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?

----

EDIT: people have asked for some references on the equivalence between the terms "Simply Typed Lambda Calculus" and "Simple Type Theory." When I said that, I didn't mean they were two different systems that admit some technical "equivalence," but rather that I have generally seen the two terms used interchangeably to mean the same thing, which is the thing defined in [Alonzo Church's 1940 paper][4].

To be clear, this paper describes a simply typed lambda calculus with two base types - that of propositions and that of "individuals" (not the same as a primitive "integer" type, but more general and without any particular description of the inhabitants of that type). He also defines as primitives negation, logical OR, universal quantification, and a definite description operation, from which he further derives existential quantifiers, an implication relation, a propositional bidirectional implication, an equality relation on "individuals," an encoding of numerals with a "successor relation," and so on.

Church also gives an inference system as a list of additional axioms. His axioms 1-4 are sufficient to derive the law of excluded middle, adding his axioms 5-6 are sufficient for the "logical functional calculus" (which I believe is his term for first-order logic, given that these axioms define how quantifiers work), axioms 7-9 describe the universe of individuals and yield that there are infinitely many, 10-11 give axioms of extension and choice. Church describes which axioms are required to prove different theories; axioms 1-4 are sufficient for "propositional calculus," 1-6 are sufficient for "logical functional calculus" (FOL?), 1-9 are sufficient for "elementary number theory," 1-11 are sufficient for "classical real analysis."

Church then goes onto derive the Peano axioms from the above, including the Peano induction axiom. I am not sure how strong the induction axiom is.

There are a few other papers describing ways to simplify Church's system: for instance, you can derive quantifiers from lambda plus definite description (Quine 1956, Henkin 1963). A good reference for these is [Stanford's Encyclopedia page on Church's Type Theory][5].

Here are a few examples in which the terms "Simply Typed Lambda Calculus" and "Simple Type Theory" are used to describe the same system from Church's paper:

**Referring to Church's System as "Simply Typed Lambda Calculus"**

- [Wikipedia's page on the Simply Typed Lambda Calculus][1] states in the first paragraph "The simply typed lambda calculus was originally introduced by Alonzo Church in 1940 as an attempt to avoid paradoxical uses of the untyped lambda calculus, and it exhibits many desirable and interesting properties."
- In general, Wikipedia is fairly uniform in defining the "simply typed lambda calculus" as the typed lambda calculus without polymorphic types, dependent types, etc, and explicitly citing Church's version.
- Thierry Coquand's [course notes on Type Theory][6] says: "Church formulated then an elegant formulation of higher-order logic, using simply typed λ-calculus [5], which can be seen as a simplification of the type system used in Principia Mathematica, but also is in some sense a return to Frege."
- In general, an arXiv search for "Simply Typed Lambda Calculus" "Higher Order Logic" yields plenty of results. For instance, see the paper "[An overview of type theories][7]" by Nino Guallart, which says "Simply typed lambda calculus. Simply typed lambda calculus was also originally developed by Church (1940,1941). It is a higher order logic system based on lambda calculus and it uses the same syntax."

**Referring to Church's System as Simple Type Theory**

- The article [Seven Virtues of Simple Type Theory][3] refers to Church's system instead as "Simple Type Theory," and says "In 1940 A. Church presented an elegant formulation of simple type theory, known as Church's type theory..." They claim that the abstract "simple type theory" that Church's version is "a formulation of" is equivalent to Russell's "ramified theory of types plus the Axiom of Reducibility."
    - The same article writes "Simple type theory, also known as higher-order logic, is a natural extension of first-order logic. It is based on the same principles as first-order logic but differs from first-order logic in two principal ways. First, terms can be higher-order, i.e., they can denote higher-order values such as sets, relations, and functions. Predicates and functions can be applied to higher-order terms, and quantification can be applied to higher-order variables in formulas."
    - [Seven Virtues][3] gives an explicit formulation of "a version" of "Simple Type Theory" which is claimed to be "a version of" Church's theory and equivalent to it. Their derivation seems to be equivalent to the one on [Stanford's page][5], which shows that some of Church's primitives (such as universal quantification) are redundant and can be derived from lambda plus equality.
    - The "Seven Virtues" paper proves as a theorem that any nth-order logic can be embedded in their STT, which they prove in Theorem 2.
- The Stanford Encyclopedia of Philosophy has an article on "[Church's Type Theory][8]," for which they make clear that they consider Church's theory "a formulation of" type theory, and also state "Type theories are also called higher-order logics, since they allow quantification not only over individual variables (as in first-order logic), but also over function, predicate, and even higher order variables."
    - Stanford also has a subsection on "adding types" to their page on the lambda calculus, in ["Lambda Calculus - Adding Types"][9], citing Church's theory. They also have a page on ["Simple Type Theory and the Lambda Calculus"][10] which goes into detail about how Russell's type structure from Principia can be derived using Church's typed lambda calculus.
- All such examples above referring to "Simple Type Theory" or "Church's Type Theory" do not incorporate any notion of polymorphic types, dependent types, etc.
- In general it is also not difficult to find references citing Church's paper and using the term "Simple Type Theory" for it. Here is an arXiv paper called [Formalising Mathematics In Simple Type
Theory][11] that says "Higher-order logic is based on the work of Church [10], which can be seen as a simplified version of the type theory of Whitehead and Russell."

----

So that was my point. I have seen the terms "STLC" and "STT" used interchangeably to describe the same system, which is Church's typed system, or various equivalent formulations of it. The terminology seems messy and I am not sure exactly in what sense Church's system is or isn't stronger than FOL.


  [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
  [4]: https://pdfs.semanticscholar.org/28bf/123690205ae5bbd9f8c84b1330025e8476e4.pdf
  [5]: https://plato.stanford.edu/entries/type-theory-church/#ForBasEqu
  [6]: http://www.cse.chalmers.se/~coquand/newnotes.pdf
  [7]: https://arxiv.org/pdf/1411.1029.pdf
  [8]: https://plato.stanford.edu/entries/type-theory-church/
  [9]: https://plato.stanford.edu/entries/lambda-calculus/#AddTyp
  [10]: https://plato.stanford.edu/entries/type-theory/#SimpTypeTheoLCalc
  [11]: https://arxiv.org/pdf/1804.07860.pdf