Notes to Combinatory Logic

1. Moses Schönfinkel had a chance to publish just one paper on CL (see Schönfinkel (1924)). CL was soon rediscovered and greatly expanded in its scope by Haskell B. Curry, who was joined by several other logicians in an effort to develop CL and the closely related λ-calculi.

2. This sentence may be seen to formalize a well-known metatheorem about well-behaved sequent and consecution calculi — without explicating some of the technical details.

3. The formal notions of algorithms, computable functions and alike had not yet been formulated at the time when Schönfinkel published his paper. λ-calculi, Turing machines and Post's calculi appeared a decade or more later, and other notions such as Markov algorithms, register machines, 0-type grammars and abstract state machines are even newer. See Kleene (1967, Ch. V) concerning the early history of some of these concepts.

4.CGyx’ could be thought to be read as “y is less than x,” and ‘Lyx’ could stand for this binary predicate in a more mnemonic presentation of FOL. However, given G, ‘CGyx’ and ‘Lyx’ express the same thing.

5. The possibility of this move follows from, and therefore, illustrates the combinatorial completeness theorem. Although this last potential transformation is not important for the success of Schönfinkel's procedure, combinatorial completeness is.

6. This may be the reason why Schönfinkel gave second-order examples toward the end of his paper, despite the fact that he unequivocally stated at the beginning of his paper that he is concerned with FOL. (Incidentally, the misleading examples were not caught by the German editor, who, on the other hand, appended some paragraphs to the paper that contain mistaken claims.) The unfortunate choice of examples might have contributed to the misinterpretation of Schönfinkel's aims along the line that he attempted to provide a typefree framework for all of mathematics.

7. The importance of this idea can hardly be overstated. Viewing a function of several arguments as a function of one argument is often called “currying” (with the other direction termed “uncurrying”). The same idea reappears in recursion theory in the proof of the s-m-n theorem, in algebra as (abstract) residuation and in category theory (in the unary case) as adjoint functors.

8. One might contend that the understanding of (closed) formulas not only as meaningful sentences but also as sequences of symbols on paper is as crucial to Schönfinkel's procedure as it is to Gödel's first incompleteness theorem.

9. We follow Curry's meta-theoretical distinctions in calling the entities that CL deals with ‘objects’ rather than using the neutral expression ‘expressions’. (Curry uses ‘obs’ as a technical term.)

10. We do not follow Curry's terminology completely, according to which the combinator that is denoted here by M is only a combinator with “duplicative effect,” because we do not utilize the distinction between regular and nonregular combinators. The interested reader should consult Curry and Feys (1958) concerning a slightly different use of the terms “cancellator,” “duplicator,” “permutator,” etc.

Copyright © 2012 by
Katalin Bimbó <bimbo@ualberta.ca>

Open access to the SEP is made possible by a world-wide funding initiative.
Please Read How You Can Help Keep the Encyclopedia Free