How can the simply typed lambda calculus be Turing-incomplete, yet stronger than second-order logic?

Question

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.

Answer 1

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 substitution

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, successor, 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 arise.

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

1. The Curry-Howard correspondence relates the propositional calculus to the simply-typed $\lambda$-calculus by an interpretation of propositional formulas as types.

2. 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 contrast, 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.

Answer 2

Simply typed lambda calculus and simple type theory are not equivalent. The former only has rules for alpha- and beta-reduction, the latter also has rules for Modus Ponens, extensionality and the Introduction of the quantification constant $\Pi$. The normalization results for lambda calculus only refer to rewriting modulo alpha- and beta reduction (there are also variants including eta, an extensionality rule for lambda terms). I will give a common set of rules below (following: Benzmüller, Miller: Automation of Higher-order Logic).

What is a little confusing is that lambda calculus can encode proofs in simple type theory. This is usually done via the Curry-Howard isomorphism but Farmer uses a different encoding. In both cases, we can verify a proof term by normalization but we can not find these terms by reduction.

• Simply typed LC (Church style)

  The types $o$ and $\iota$ are basic types. Every basic type is a (complex) type. Let $\tau_1, \tau_2$ be (complex) types, then the type application $\tau_1 \rightarrow \tau_2$ is a complex type.

  Terms are inductively defined:

  • A variable $x$ of type $\tau$ is a term of type $\tau$
  • Let $s$ be a term of type $\tau_1 \rightarrow \tau_2$ and $t$ be a term of type $\tau_1$. Then the application $s t$ is a term of type $\tau_2$
  • Let $x$ be variable of type $\tau_1$ and $t$ be a term of type $\tau_2$, then $\lambda x.t$ is a term of type $\tau_1 \rightarrow \tau_2$.

  We define the following inferences on lambda terms:

  • $\alpha$-equivalence: $(\lambda x.t[x]) = (\lambda y.t[y])$ when $x,y$ do not appear in t otherwise.
  • $\beta$-equivalence: $(\lambda x.s[x])t = s[t]$ when $x$ does not appear in $t$. Rewriting the equation left to right is called a $\beta$-reduction; rewriting right to left is called $\beta$-expansion.

  Remark: I made the containment requirements stricter than necessary to simplify the presentation. The main issue is overbinding, iotw. that $(\lambda x \lambda y.f x y) y$ $\beta$-reduces to $\lambda z.f y z$ but not to $\lambda y. f y y$.

  The decidability result you mentioned is that continued $\beta$-reduction of a term modulo $\alpha$-equivalence terminates and results in a normal form. There is also an upper bound ($O(2\uparrow\uparrow$n)) to the growth in size during this process such that we cannot express any function that grows faster than that.

• Elementary type theory: We assume the existence of variables for the logical connectives ($¬,∨,\Pi)$ of types $o\rightarrow o$, $o\rightarrow o \rightarrow o$ and $(\alpha \rightarrow o) \rightarrow o$. The connectives $\land,⊃$ can be derived the same way as in FOL. $\Pi$ represents universal quantification; $\forall x.f$ is defined as $\Pi \lambda x.f$ and $\exists x.f = \neg \forall x.\neg f$.

  We also add the following inference rules to typed LC:

  • Substitution: given the term $f x$ where $x$ is not free (*), infer the term $f a$ (under the condition that $x$ and $a$ have the same type)
  • Modus Ponens: from $f$ and $f ⊃ g$ infer $g$
  • Generalization: from $f x$ infer $\Pi f$ if $x$ is not free in $f$

  We also assume some Hilbert-style axioms describing the logical connectives.

• Simple type theory: We add even more axioms to elementary type theory: extensionality, Leibniz equality, number theory, description and choice.

It should be intuitive that applying inferences cannot terminate even for elementary type theory: after all, it allows to derive logical consequences for which $\beta$-reduction is not sufficient. LC is still a quite expressive language which even allows to encode proofs - it's just not strong enough to express the proof search.

Remark: the logical connectives can be defined in multiple ways, e.g. Andrews builds up the whole theory based on an equality predicate.

(*) a variable $x$ is bound in a term if it occurs inside an abstraction $\lambda x.t$ over $x$. All occurrences of a variable that are not bound are free occurrences.