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

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:

1. The Curry-Howard correspondence relates the propositional calculus to the simply-typed $\lambda$-calculus by an interpreation 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 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.

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.