[Math] How to the simply typed lambda calculus be Turing-incomplete, yet stronger than second-order logic

lambda-calculuslo.logicproof-theorytype-theory

It is well-known that the simply typed lambda calculus is strongly normalizing (for instance, Wikipedia). Hence, it is not strong enough to be Turing-complete, as also mentioned on the Wikipedia page for Turing-completeness. 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", 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.

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.

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 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 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" 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 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 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, 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," 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", citing Church's theory. They also have a page on "Simple Type Theory and the Lambda Calculus" 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 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.

Best Answer

The simply-typed $\lambda$-calculus is not stronger than second-order logic.

The simply-typed $\lambda$-calculus has:

product types $A \times B$, with corresponding term formers (pairing and projections)
function types $A \to B$, with corresponding term formers (abstraction and application)
equations governing the term formers and subtitution

The simply-typed $\lambda$-calculus does not postulate the existence of any types. Sometimes we postulate the unit type $1$, and often we postulate the existence of a collection of basic types, but without any assumptions about them being inhabited. This is akin to using a collection of propositional symbols in the propositional calculus, where we make no claims as to their truth value.

Simple type theory is simply-typed $\lambda$-calculus and additionally at least:

the type of truth values $o$, with the corresponding term formers (constants $\bot$ and $\top$, connectives, quantifiers at every type)
the type of natural numbers $\iota$, with the corresponding term formers (zero, succcesor, primitive recursion into arbitrary types)
equations governing the term formers and substitution

There are several variations:

we may postulate excluded middle for truth values
we may include a definite description operator
we may include the axiom of choice
we may vary the extensionality principles

We quickly obtain a formal system that expresses Heyting (or Peano) arithmetic and more, which suffices for incompleteness phenomena to kick in.

What I think is confusing you is the fact that there are two ways to relate logic to type theory:

The Curry-Howard correspondence relates the propositional calculus to the simply-typed $\lambda$-calculus by an interpreation of propositional formulas as types.
Higher-order logic embeds into simple type theory by an interpretation of logical formulas as terms of the type $o$ of truth values.

There is a difference of levels, which makes all the difference.

To illustrate, consider the propositional formula $$p \land q \Rightarrow (r \Rightarrow p \land r).$$ In the simply typed $\lambda$-calculus it is interpreted as the type $$P \times Q \to (R \to P \times R).$$ To prove the formula amounts to giving a term of the type. In constrast, in simple type theory it is interpreted as the term $$p \land q \Rightarrow (r \Rightarrow p \land r) : o$$ (with parameters $p, q, r$ of type $o$). Now proving the formula amounts to proving the equation $(p \land q \Rightarrow (r \Rightarrow p \land r)) =_o \top$ in the simple type theory.

A higher-order formula, such as $(\forall r : \mathsf{Prop} . r \Rightarrow p) \Rightarrow p$ cannot be encoded in the simply-typed $\lambda$-calculus, whereas in the simple type theory it is again just a term of type $o$ (just replace the sort of propositions $\mathsf{Prop}$ with the type $o$).

Also note that the pure simply-typed $\lambda$-calculus does not postulate the natural numbers. If we add the natural numbers to the simply-typed $\lambda$-calculus we get a fragment of simple type theory known as Gödel's System T (or a version of it, depending on minutiae of how equality is treated), which suffers from – or enjoys, depending on your point of view – the incompleteness phenomena already.

Related Solutions

[Math] Why is there no product type in simply typed lambda-calculus

You have not really encoded the sum type $\alpha \sqcup \beta$, but made a "virtual embedding" of the sum type into $(\rho^{\rho^\beta})^{\rho^\alpha}$. You could not encode sum types in such a calculus, simply because sum types are not expressible in it (you may know this result in a different form --- disjunctions are not definable in an implicational fragment of intuitionistic propositional logic). To see how your embedding works, let me assume for a moment that our calculus has both sum and product types. Then: $$(\rho^{\rho^\beta})^{\rho^\alpha} \approx \rho^{\rho^\alpha \times \rho^\beta} \approx \rho^{\rho^{\alpha \sqcup \beta}}$$ Therefore, your embedding may be thought of as canonical morphism: $$\alpha \sqcup \beta \rightarrow \rho^{\rho^{\alpha \sqcup \beta}}$$ Actually, $\rho^{\rho^{(-)}}$ is a continuation monad, and the embedding $\tau \overset{\mathit{ret}}\rightarrow \rho^{\rho^{\tau}}$ lifts types to the continuation semantics, where as you have figured out, coproducts "virtually exist". By the way, I have said "embedding", but $\mathit{ret}$ generally is not an embedding --- it is a monomorphism if and only if $\rho$ is an internal cogenerator --- which means that the internal contravariant hom-functor $\rho^{(-)}$ is faithfull (see also this answer).

As pointed out by Peter in the comments, you may similarly "embed" product types: $$\alpha \times \beta \rightarrow \rho^{\rho^{\alpha \times \beta}} \approx \rho^{(\rho^{\beta})^\alpha}$$ Then instead of working with $\alpha \times \beta$, work with continuation type $\rho^{(\rho^{\beta})^\alpha}$. For example you may define the first projection $\rho^{(\rho^{\beta})^\alpha} \rightarrow \rho^{\rho^\alpha}$ as: $$\lambda p \colon \rho^{(\rho^{\beta})^\alpha} . \lambda f \colon \rho^\alpha . p (\lambda a \colon \alpha . \lambda b \colon \beta . f a \colon \rho)$$ and in the same manner the second projection $\rho^{(\rho^{\beta})^\alpha} \rightarrow \rho^{\rho^\beta}$ as: $$\lambda p \colon \rho^{(\rho^{\beta})^\alpha} . \lambda g \colon \rho^\beta . p (\lambda a \colon \alpha . \lambda b \colon \beta . g b \colon \rho)$$

However, it is worth saying that to emulate product types you do not need the above construction --- functions from a product type $\alpha \times \beta \rightarrow \tau$ are tantamount to functions $\alpha \rightarrow \tau^\beta$, and function to a product type $\tau \rightarrow \alpha \times \beta$ are tantamount to pairs of functions $\tau \rightarrow \alpha$ and $\tau \rightarrow \beta$, therefore in both cases are (in some sense) "redundant".

To not be worse, here is my GHC session:

pair :: Integer -> Bool -> (Integer -> Bool -> Bool) -> Bool
pair a b = \c -> c a b

first :: ((Integer -> Bool -> Bool) -> Bool) -> (Integer -> Bool) -> Bool
first p = \f -> p (\a b -> f a)

second :: ((Integer -> Bool -> Bool) -> Bool) -> (Bool -> Bool) -> Bool
second p = \g -> p (\a b -> g b)

*Main> let p = pair 2 True in first p ((<)1)
True
*Main> let p = pair 2 True in first p ((<)3)
False
*Main> let p = pair 2 True in second p ((||) False)
True
*Main> let p = pair 2 False in second p ((||) False)
False

Best Answer

Related Solutions

[Math] Why is there no product type in simply typed lambda-calculus

Related Question