History of Lambda Calculus

https://plato.stanford.edu/entries/paradoxes-contemporary-logic/#IncCerForLog

In the 1920's and early 30's, the orthodox view of logic among mathematicians was mostly type-theoretic or set-theoretic. Despite this, there was a renewed effort to develop new logics as substitutes for the logic of Principia Mathematica.

Combinatory logic and λ-calculus intially attempted to regain the simplicity of the untyped approach, originating in the so-called naive comprehension principle, but also to investigate the foundations of mathematics using the basic concept of operation instead of set, as well as to clarify the fundamental concepts underlying the notions of formal system, formalism, rule. They have both evolved since into the important tools for the development and study of programming languages.

In particular, Church and Curry proposed theories which 1. assume as primitive the notions of self-applicable function-in-intension 2. stress the very mechanism of definition/combination of concepts.

If one looks closely at the development of these systems, one can see that paradoxical constructions have become essential tools for defining objects and proving non-trivial logical mathematical facts.

Curry's formalism

Further developing the idea of Schönfinkel and aiming at a mathematical analysis of the substitution process, Curry has introduced a formal language based on basic general operators, the so-called combinators, in 1930:

• B (composition) Bxyz = x(yz)

• C (permutation) Cxyz = xzy

• W (duplication) Wxy = xyy

• K (cancellation) Kxy = y

• Q (equality) Qxyz = x(zy)

• logical constants like ∀ and implication

Expressions are then inductively generated by application from constants.

Intuitively, a term M stands for a function, and the applicative term MN denotes the value of the term obtained by replacing the first variable of M with N.

Self-application, MM, is admissible and this feature tells us that the objects of combinatory logic cannot be simply interpreted as set-theoretic functions.

The formal system consists of

• standard equations on combinators

• rules for equality

• the logical constants

The main goal of combinatory logic is to derive equalities X = Y and to make assertions of the form ⊢ X (X is provable).

Combinatory logic is a theory which analyzes the modes of combinations of formal objects, substitution, and the notions of proposition and propositional function.

(see the entry on combinatory logic for a proper introduction to variants of the formalism and an overview of the properties of related calculi https://plato.stanford.edu/entries/logic-combinatory/).

For Curry, the root of the paradoxes is found in assuming that combinations of concepts are always propositions. The notion of proposition becomes a theoretical concept, which is decided by the theory. Types are not assigned to the expressions of the formal system at the outset, but are instead inferred by means of the system itself, which has a dual nature: it can derive identities, but also truths.

In particular, if ⊢ M N is derived, this can be read as "N is of type M" or "N is an element of M".

These ideas foreshadow fundamental developments such as the Curry-Howard corespondence finalized in 1969 of formulas-as-types interpretation. The Curry-Howard correspondence is the interpretation of mathematical proofs as programs and logical formulae as types in a programming language.

Church's formalism

Church's formalism, originally introduced in 1932 as a set of postulates for the foundation of formal logic, includes conversion, i.e. computational rules, which allow the replacement of terms with intensionally equivalent ones, and rules for asserting certain terms as "true".

The syntax yields a general notation system for functions, based on an applicative language, where there is one basic category of terms (well-formed formulas in Church's terminology).

Some terms are formally provable (or assertable) and are classified as true.

Terms are inductively defined from a set of basic constants and variables by means of application and the characteristic lambda abstraction operator:

• if M is a term containing the variable x, then λx.M is a term, naming the function defined by M

The basic constants designate logical operations:

• (a kind of restricted) formal implication

• existential quantifier,

• conjunction,

• negation,

• description operation,

• generalized abstraction: i.e. if F is formal logical equivalence, then the A(F,M) is "what M has in common with any N formally equivalent to M"

It turns out that Church's logic can interpret naive class theory and hence the system is suspiciously strong and expressive (strength and expressivity are inherited by the formalism which was devised out of Church's, the lambda calculus https://plato.stanford.edu/entries/lambda-calculus/). Church's hope was that contradictions could be avoided by ensuring the possibility that a propositional function be undefined for some argument.

However, the theories of Curry and Church were almost immediately shown inconsistent in 1934, by Kleene and Rosser, who essentially proved a version of the Richard paradox (both systems can provably enumerate their own provably total definable number theoretic functions).

The result was triggered by Church himself in 1934, when he used the Richard paradox to prove a kind of incompleteness theorem (with respect to statements asserting the totality of number theoretic functions).

The reason for the inconsistencies was eventually clarified by Curry's 1941 essay. There he distinguishes two basic completeness notions:

• a system S is deductively complete if, whenever it derives a proposition B from the hypothesis A, then it also derives the implication A → B (deduction theorem, introduction rule for implication);

• a system S is combinatorially complete (Curry 1941, p.455.) if, whenever M is a term of the system possibly containing an indeterminate x, there exists a term (Church's λx.M) naming the function of x defined by M.

A -> B (A -> B) -> B

Curry then remarks that the paradox of Kleene-Rosser arises because Church's and Curry's systems satisfy both kinds of completeness, thus showing that the two properties are incompatible.

In the more technical part of the paper, Curry carefully axiomatizes the main ingredients exploited by Kleene and Rosser and carries out a lot of non-trivial work both on the logical side and the mathematical side (e.g, to develop a portion of recursive arithmetic, to define the existence of an enumerator, i.e.a term T such that, if a is the Gödel number of a closed term M and Za is the term formally representing a, then TZa=M is provable in S, etc.).

Curry's proof of the inconsistencies of combinatory systems is unsatisfactory because it heavily uses a detour through number theory and Gödelization, which, as a matter of fact, is unnecessary as Curry himself soon discovered and presented in a paper with the same title as the one by Kleene and Rosser, "in deference to the original discoverers of the contradiction" (Curry 1942). The main result in it is the following theorem (Curry's paradox, see the entry Curry's Paradox):