What is the actual significance of the lambda calculus for the formalization of math?

Question

The Simply Typed Lambda Calculus was proposed initially as a foundational system for the formalization of mathematics. As such, I would expect that soon there would be attempts to implement most of our daily high-level math on it. Decades after, seems like that idea never became a reality: we haven't formalized anything on the lambda calculus at all. Indeed, I wonder if someone ever implemented a single trigonometric function on it.

Why has this never happened? Am I misunderstanding the purpose of the STLC, or did it just fail its goal?

Answer 1

The answer to your question is that the simply typed lambda calculus has been instrumental in creating new foundations for (constructivist) mathematics, though it has done so indirectly as part of long sequence of events.

Note that early type theory preceded Church's simply typed lambda calculus by exactly 37 years, so there is a rich history prior to the listing here that may be investigated for those who are interested.

What follows is an abridged history of the developments that directly involve the simply typed lambda calculus and its variants (ascending, by year):

---

(1932) A. Church, "A set of postulates for the foundation of logic", Annals of Mathematics, Series 2, 33:346–366

• Church introduces the lambda calculus as part of his investigation into the foundations of mathematics.

(1934) Curry, Haskell B. "Functionality in combinatory logic." Proceedings of the National Academy of Sciences 20.11 (1934): 584-590

• Curry observes that types of the combinators could be seen as axiom-schemas for an intuitionistic implicational logic.

(1935) Kleene, S. C. & Rosser, J. B. "The inconsistency of certain formal logics". Annals of Mathematics 36 (3): 630–636

• The Kleene-Rosser paradox is established, showing the inconsistency of Curry's combinatory logic and Church's original lambda calculus.

(1936) A. Church, "An unsolvable problem of elementary number theory", American Journal of Mathematics, Volume 58, No. 2. (April 1936), pp. 345-363

• In response to Kleene and Rosser, Church introduces what would later be called the untyped lambda calculus. He did this by isolating the relevant portions of the original lambda calculus that pertained solely to computation.

(1940) Church, A. "A Formulation of the Simple Theory of Types". Journal of Symbolic Logic 5: 1940.

• Church introduces the simply typed lambda calculus.

(1958) Curry, H. B., Feys, R., Craig, W., & Craig, W. (1958). Combinatory logic, vol. 1. North-Holland Publ.

• Curry, et al, observes a close correspondence between axioms of positive implicational propositional logic and "basic combinators".

(1969) Howard, W., 1980 [1969], “The formulae-as-types notion of construction,” in J. Seldin and J. Hindley (eds.), To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, London, New York: Academic Press, pp. 480–490

• The Curry-Howard correspondence is circulated as notes but would not be officially published until 1980. It was based on the "formulas-as-types" or "propositions-as-sets" principle and linked with Church's simply typed lambda calculus.

• Howard did so by taking the untyped lambda calculus and creating what could be interpreted as a variant of the simply typed lambda calculus (in § "Type symbols, terms and constructors) that could be more readily expressed with the concepts he was explaining at the time.

• This correspondence would make intuitionistic natural deduction part of computer science proper [1], and would be instrumental to further developments in type theory.

(1972) Martin-Löf, P. "An intuitionistic theory of types." Omtryckt i (Sambin och Smith 1998)

• This is abridged, as there was a prior formalization in 1971 called "A theory of types" that was shown to be inconsistent as demonstrated by Girard's paradox, and his later refinements became predicative, along with adding many other seminal contributions to type theory. There would also be intensional and extensional variants.
• The historical context is that it was based on an isomorphism between propositions and types, which is associated with the Curry-Howard correspondence, in which Howard directly mentions Martin-Löf during his communications. Thus, this links intuitionistic type theory to the simply typed lambda calculus, or, at the very minimum, to the entire family of the lambda calculi.

(2009-) Voevodsky, Vladimir. "Notes on type systems." Unpublished notes, (www.math.ias.edu/~ vladimir/Site3/Univalent_Foundations) HTML

• Voevodsky introduces the starting point of the homotopy type theory and the univalent foundations. All of this was based on Voevodsky's investigations into the foundations of mathematics, just as it was with Church, and those before him. Church's simply typed lambda calculus has played a not insignificant role in the history of these developments, despite its seeming invisibility in the most modern incarnation of these theories.

• Later refinements came in "The Simplicial Model of Univalent Foundations" (2012) and more can be read in the Homotopy Type Theory book. An overview was published in Quanta magazine that is highly approachable.

---

Many other authors have contributed to type theory. They are all important. For space reasons, they could not be fully detailed here. As was mentioned, this is only with the context of the simply typed lambda calculus. I have done my best to provide an accounting of the relevant details. If anything is incorrect I will update promptly.