Combinatory logic

A branch of logic devoted to the study and analysis of such concepts and methods as a variable, a function, the substitution operation, the classification of objects into types or categories, and related matters.

In combinatory logic one chooses as basic the concepts of a one-place function and the operation of applying a function to an argument (application). Here the concept of a function is regarded as primitive, instead of that of a set, and is generalized in such a way that a function can be applied to objects at the same level with it. In particular, a function $f$ can serve as an argument of itself. Since functions can be used both as arguments and values, the notion of a many-placed function reduces to that of a one-placed function. The result of applying a function $f$ to an argument $x$ is denoted by $(fx)$. For simplicity the brackets are often omitted, so that the expression $fx_1\dots x_n$ stands for $(\dots(fx_1)\dots x_n)$. A function $f$ satisfying the equation

$$fx_1\dots x_n=\mathfrak X,$$

where $x_1,\dots,x_n$, $n\geq1$, are arbitrary functions and $\mathfrak X$ is an object constructed from these functions (perhaps not from all of them), is called a combinator. (The existence of combinators is tacitly postulated.) Any combinator can be expressed in terms of the two combinators $S$ and $K$ satisfying the following equations:

$$Sxyz=xz(yz),\quad Kxy=x$$

(where $x,y,z$ are arbitrary functions).

One of the first problems in combinatory logic was that of the reduction of the primitive concepts in logic to a minimal number of sufficiently simply concepts. The individual function $U$ was introduced, which generalizes the Sheffer stroke (if $f$ and $g$ are one-place propositional functions, then $Ufg$ is interpreted as $(\forall x)(f(f(x)\Rightarrow\neg g(x))$), and it was proved that every formula of the predicate calculus can be represented as a combination of the letters $U,S,K$ (and brackets); whence the name "combinatory logic" (H.B. Curry, around 1930). In such a representation, variables are not used at all; this enables one to do away with the variable as a primitive concept. (Moreover, the distinctions between the primitive concepts of an individual constant, a proposition and a propositional function are also eliminated.) However, as the subsequent development of combinatory logic showed, the construction of a logical system on such a basis met with considerable difficulties. The first logical calculi of this type, proposed by A. Church and Curry, proved to be inconsistent (the Kleene–Rosser paradox, see [4]). In order to escape from this inconsistency, combinatory logic has to be constructed either as a logic possessing very feeble deductive possibilities, or as one whose objects are divided into various categories. The main development of combinatory logic has proceeded along the second route.

The part of combinatory logic that does not deal with "logic" but is merely interested in the properties of combinators is called the pure theory of combinators. It has been proved that this theory is consistent. Its formalization has resulted in several calculi, which all divide into two sharply distinct classes: the combinator calculus and the $\lambda$-calculus.

References

[1]	H.B. Curry, R. Feys, "Combinatory logic" , 1 , North-Holland (1958)
[2]	H.B. Curry, J.R. Hindley, J.P. Seldin, "Combinatory logic" , 2 , North-Holland (1972)
[3]	A. Church, "The calculi of lambda conversion" , Princeton Univ. Press (1941)
[4]	S.C. Kleene, J. Rosser, "The inconsistency of certain formal logics" Ann. of Math. , 36 (1935) pp. 630–636
[5]	S. Yanovskaya, "Combinatory logic" , Philosophical Encyclopaedia , 3 , Moscow (1964) pp. 226–227 (In Russian)
[6]	A.S. Kuzichev, "On the subject and methods of combinatory logic" , History and Anthology of the Natural Sciences , 14 (1973) pp. 131–141 (In Russian)

Comments

The notation $U$ and an analysis of the first problem in combinatory logic can be found in M. Schönfinkel's paper [a1], which was the first paper on the subject.

An elementary introduction is [a3]; [a4] is a key modern reference.

References

[a1]	M. Schönfinkel, "Über die Bausteine der mathematischen Logik" Math. Ann. , 92 (1924) pp. 305–316
[a2]	M. Schönfinkel, "Über die Bausteine der mathematischen Logik" J. van Heijenoort (ed.) , From Frege to Gödel , Harvard Univ. Press (1967) pp. 355–366 (Reprint of the previous reference)
[a3]	J.R. Hindley, J.P. Seldin, "Introduction to combinators and $\lambda$-calculus" , Cambridge Univ. Press (1986)
[a4]	H.P. Barendrecht, "The lambda-calculus, its syntax and semantics" , North-Holland (1977)