Return to 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:

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.

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.

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 existe of a type, but without any assumptions about it). We typically work with schemata, i.e., we use meta-level symbols for types. This is akin to using propositional symbols in the propositional calculus.

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 : o, q : o, r : o \vdash p \land q \Rightarrow (r \Rightarrow p \land r) : o,$$ Now proving the formula amounts to proving the equation $p \land q \Rightarrow (r \Rightarrow p \land r) = \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.

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.

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 existe of a type, but without any assumptions about it). We typically work with schemata, i.e., we use meta-level symbols for types. This is akin to using propositional symbols in the propositional calculus.

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 : o, q : o, r : o \vdash p \land q \Rightarrow (r \Rightarrow p \land r) : o,$$ Now proving the formula amounts to proving the equation $p \land q \Rightarrow (r \Rightarrow p \land r) = \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.

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 existe of a type, but without any assumptions about it). We typically work with schemata, i.e., we use meta-level symbols for types. This is akin to using propositional symbols in the propositional calculus.

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 : o, q : o, r : o \vdash p \land q \Rightarrow (r \Rightarrow p \land r) : o,$$ Now proving the formula amounts to proving the equation $p \land q \Rightarrow (r \Rightarrow p \land r) = \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.