Following are the first three pages of the book on the λ-calculus by Alonzo Church (1941).
Underlying the formal calculi which we shall develop is the concept of a function, as it appears in various branches of mathematics, either under that name or under one of the synonymous names, "operation" or "transformation." The study of the general properties of functions, independently of their appearance in any particular mathematical (or other) domain, belongs to formal logic or lies on the boundary line between logic and mathematics. This study is the original motivation for the calculi — but they are so formulated that it is possible to abstract from the intended meaning and regard them merely as formal systems.
A function is a rule of correspondence by which when anything is given (as argument) another thing (the value of the function for that argument) may be obtained. That is, a function is an operation which may be applied on one thing (the argument) to yield another thing (the value of the function). It is not, however, required that the operation shall necessarily be applicable to everything whatsoever; but for each function there is a class, or range, of possible arguments — the class of things to which the operation is significantly applicable — and this we shall call the range of arguments, or range of the independent variable, for that function. The class of all values of the function, obtained by taking all possible auguments, will be called the range of values, or range of the dependent variable.
If f denotes a particular function, we shall use the notation (fa) for the value of the function f for the argument a. If a does not belong to the range of arguments of f, the notation (fa) shall be meaningless.
It is, of course, not excluded that the range of arguments or range of values of a function should consist wholly or partly of functions. The derivative, as this notion appears in the elementary differential calculus, is a familiar mathematical example of a function for which both ranges consist of functions. Or, turning to the integral calculus, if in the expression ∫01(fx)dx we take the function f as independent variable, we are led to a function for which the range of arguments consists of functions and the range of values, of numbers. Formal logic provides other examples; thus the existential quantifier, according to the present account, is a function for which the range of arguments consists of propositional functions, and the range of values consists of truth values.
In particular it is not excluded that one of the elements of the range of arguments of a function f should be the function f itself. This possibility has frequently been denied, and indeed, if a function is defined as a correspondence between two previously given ranges, the reason for the denial is clear. Here, however, we regard the operation or rule of correspondence, which constitutes the function, as being first given, and the range of arguments then determined as consisting of the things to which the operation is applicable. This is a departure from the point of view usual in mathematics, but it is a departure which is natural in passing from consideration of functions in a special domain to the consideration of function in general, and it finds support in consistency theorems which will be proved below.
The identity function I is defined by the rule that (Ix) is x, whatever x may be; then in particular (II) is I. If a functIon H is defined by the rule that (Hx) is I, whatever x may be, then in particular (HH) is I. If Σ is the existential quantifier, then (ΣΣ) is the truth-value truth.
The functions I and H may also be cited as examples of functions for which the range of arguments consists of all things whatsoever.
The foregoing discussion leaves it undetermined under what circumstances two functions shall be considered the same.
The most immediate and, from some points of view, the best way to settle this question is to specify that two functions f and g are the same if they have the same range of arguments and, for every element a that belongs to this range, (fa) is the same as (ga). When this is done we shall say that we are dealing with functions in extension.
It is possible, however, to allow two functions to be different on the ground that the rule of correspondence is different in meaning in the two cases although always yielding the same result when applied to any particular argument. When this is done we shall say that we are dealing with functions in intension. The notion of difference in meaning between two rules of correspondence is a vague one, but, in terms of some system of notation, it can be made exact In various ways. We shall not attempt to decide what is the true notion of difference in meaning but shall speak of functions in intension in any case where a more severe criterion of identity is adopted than for functions in extension. There is thus not one notion of function in intension, but many notions; involving various degrees of intensionality.
In the calculus of λ-conversion and the calculus of restricted λ-K-conversion, as developed below, It is possible, if desired, to interpret the expressions of the calculus as denoting functions in extension. However, in the calculus of λ-δ-conversion, where the notion of identity of functions is introduced into the system by the symbol δ, it is necessary, in order to preserve the finitary character of the transformation rules, so to formulate these rules that an interpretation by functions in extension becomes impossible. The expressions which appear in the calculus of λ-δ-conversion are interpretable as denoting functions in intension of an appropriate kind.
So far we have tacitly restricted the term "function" to functions of one variable (or, of one argument). It is desirable, however, for each positive integer n, to have the notion of a function of n variables. And, in order to avoid the introduction of a separate primitive idea for each n, it is desirable to find a means of explaining functions of n variables as particular cases of functions of one variable. For our present purpose, the most convenient and natural method of doing this is to adopt an idea of Schönfinkel (1924), according to which a function of two variables is regarded as a function of one variable whose values are functions of one variable, a function of three variables as a function of two variables whose values are functions of one variable, and so on.