COMBINATORY LOGIC

Combinatory logic is a branch of mathematical logic that analyzes certain processes, such as substitution, which are associated with variables. These processes are taken for granted in most formulations of logic, but they are complex, and since a fundamental part of the resulting theory is recursively undecidable the analysis is not trivial. Combinatory logic contributes to simplifying the ultimate foundations of mathematical logic and to explaining the paradoxes; it contains an arithmetic in which exactly those numerical functions that are partial recursive are representable; and it has potential applications to the deeper study of such areas as logical calculuses of higher order, computer programming, and linguistics.

Before one can define combinatory logic precisely, it is necessary to explain some notions concerning formal systems. This will be done in the next section. In the following section the definition will be given and a plan presented according to which the later sections of this article will develop the subject. Each technical term is defined by the context in which it appears in italics.

Formal Systems

Consider a formal system of the following type: There is a class of formal objects, or obs, constructed from certain primitive obs, or atoms, by certain operations ; each ob has a unique such construction. Among these operations a binary one, called application, is singled out. If this is the only operation, the system is called applicative ; otherwise it is quasi-applicative. There is a unique unary predicate, symbolized by the sign "⊦" used as prefix; the elementary statements are then of the form
(1)      ⊦X,
where X is an ob. The elementary theorems form an inductive subclass of the elementary statements; they are generated from certain initial ones, the axioms, by deductive rules. The atoms, obs, elementary statements, and axioms are definite classes—that is, it can be effectively ascertained whether a proposed member of one of them is actually a member—but concerning the elementary theorems it is required only that the correctness of a derivation by the deductive rules can be effectively checked. Combinatory logic takes such a system as basis. Other sorts of system exist, but all those ordinarily used in mathematical logic can be reduced to the above type.

Assuming such a system, we observe the following conventions: The application of X to Y is symbolized as (XY ). Parentheses are omitted according to the rule of association to the left and also to the rule that outside parentheses are superfluous, so that XY ₁Y ₂Y ₃ is the same ob as (((XY ₁)Y ₂)Y ₃). A combination of given obs is an ob formed from some or all of them by application alone. The sign "≡" stands for definitional identity; "→" and "⇄" for metatheoretic implication and equivalence, respectively. Finally, "=" is defined, say, by
(2)      X = Y ⇄ ⊦ Q XY,
where Q is a specific ob, the axioms and rules being such that equality has the appropriate properties.

With such a formal system one associates two sorts of ontology. On the one hand, some persons insist on describing more definitely what the obs are; on the other hand, one may give a description of the meaning one intends for the elementary statements. The first description will be called a representation ; the second description will be called an interpretation.

For a representation it is customary to state that the obs are words in an object language. We will not do that here—all symbols belong to the U-language (metalanguage)—but it can be done quite easily for any given object language with two or more symbols. This permits a certain freedom in regard to use and mention.

An interpretation for combinatory logic may be described as follows (this is for motivation only and does not imply a commitment to any special type of metaphysics): One associates with certain obs contensive (known from prior experience) notions called interpretants. The fact that Y is the interpretant of X will be expressed simply as X means Y. Then if X means a function and Y means a possible value for the first assignment of that function, XY will mean the result of assigning the intepretant of Y as value to the first argument of X. Thus, if X means the addition function of natural numbers and Y means the number 1, then XY will mean a form of the successor function, and if Z means the number 2, then XYZ will mean the number 3. This device reduces many-place functions to unary ones without postulating ordered pairs. An elementary statement (1) will mean that X means an asserted statement; the interpretation is a valid one when every asserted statement is true.

Definition and Divisions of Combinatory Logic

The usual formal systems contain a special class of obs, usually atoms, called (formal ) variables. These are so named in the formalization and play a special role, such that arbitrary obs can be substituted for them (perhaps under restrictions). Variables do not have interpretants; obs containing them mean functions in which they stand for arguments. Thus, the elementary statements of Principia Mathematica, Sec. 1A, are not about p, q, r but about negation (∼) and alternation ∨ ); the interpretants of its elementary theorems state rather complex relationships, indicated by the variables, between these functions.

Let ℋ be a system as defined earlier, and let ℋ (x ₁, · · ·,x_m ) be the system formed by adjoining x ₁,· · ·,x_m as variables—that is, as new atoms—without further changes. As stated above, the natural interpretant of an ob M of ℋ (x ₁,· · ·,x_m ) is that function over ℋ whose value for arguments a ₁, · · ·, a_m ) is the result of substituting a ₁, · · ·, a_m for x ₁, · · ·, x_m, respectively, in M. Let us say that an ob X of ℋ designates M when and only when
(3)      Xx ₁x ₂· · ·x_m = M
is derivable in ℋ (x ₁,· · ·,x_m ). The system ℋ is called combinatorially complete when and only when such an X exists for every M. A constant (that is, an ob of an ℋ containing no variables) X is called a proper combinator when and only when it designates a combination of variables alone; a combinator is any combination of proper combinators.

Combinatory logic may now be defined as that branch of logic which studies combinators. This is tantamount, at least for applicative systems, to studying combinatorial completeness.

There are two methods of achieving combinatorial completeness. The first is to postulate a designator for every M. This idea leads to the theory of λ-conversion, which is discussed in the next section. It is a quasi-applicative system with bound variables. The other method is to exhibit all combinators as combinations of certain atomic ones, after which we can get along with an applicative system. This leads to synthetic combinatory logic, to which the rest of the article is devoted. The two approaches have been shown to be equivalent.

The subject of combinatory logic divides itself into two parts in another way. In the first part, called pure combinatory logic, one introduces no constant atoms except combinators and those atoms necessary to define equality and pays no attention to whether the obs have interpretants. In the second part, called illative combinatory logic, one introduces atoms meaning other logical notions, such as implication, quantification, and semantical categories. The question whether an ob has an interpretant, and if so, what sort of interpretant, belongs to the illative theory.

theory of Λ-conversion

In the theory of λ-conversion we postulate that given M, x ₁, · · ·, x_m, there is an X in ℋ such that (3) holds. This X, in Alonzo Church's notation, is λx ₁· · ·x_mM. It suffices to postulate this for m = 1, for we can define
λx ₁· · ·x_mx_{m +1}M ≡ λx ₁· · ·x_m (λx_{m +1}M ).
Thus, we need only a binary operation forming λxM from x and M. This operation is the only primitive operation besides application. Thus, x is a variable and is bound (in a natural extension of the usual sense) in λxM. One must distinguish, just as in predicate calculus, free and bound occurrences of variables. One understands "ob of ℋ" to include any ob formed from atoms of ℋ and variables without free occurrences of variables not in ℋ. Further, given an ob M, a variable x, and an ob N, we define [N/x ]M (subject to restrictions to prevent confusion of bound variables) as the ob obtained by the substitution of N for x in M.

In view of the intended interpretation, the following are acceptable (subject to the stated restrictions) as axiom schemes:
(α )λxM = λy [y/x ]M,
(β )(λxM )N = [N/x ]M.
Along with this one has the rules for equality, which give as a special case
(ξ )M = N → λxM = λxN.
The equality relation is called convertibility, and "cnv" is often used instead of "=." We call (β ) (as well as η and δ below) a replacement scheme. The definition is equivalent to saying that X cnv Y when and only when X can be converted to Y by zero or more successive applications of replacement schemes in either direction. There is also defined a relation of reducibility, indicated by "red," in which the replacement schemes can be used from left to right only. An ob is said to be in normal form when and only when no replacement scheme can be so applied to it.

There are various modifications of this system. In λ I-conversion (the original λ-conversion), λxM is defined only when M contains a free occurrence of x ; in λK-conversion this restriction is dropped. Again the additional axiom scheme (for x not free in U )
(η )λx (Ux ) = U
is acceptable from interpretations which maintain a strong extensionality principle. If it is adopted, the theory is here called λη-conversion, in contrast to the original λβ-conversion. Finally one may introduce axiom schemes (δ ) which single out special constants δ ₁, δ ₂, · · · and allow constants of the form δ_kU ₁U ₂· · ·U_nk, where n_k is fixed by δ_k and the U_j are in normal form, to be replaced by other constants determined in some uniform manner. Note that (δ ) is, in principle, illative.

The various forms of λ-conversion have differences in interpretation. In λ I-reduction no component is dropped; hence, if X has a normal form, so does every part of X. This is not true for λ K-reduction, a disadvantage if one identifies possession of an interpretant with having a normal form. Again, if one accepts (η ), every ob means a function (in some sense), and sometimes this is unacceptable. However, one may prefer to make such distinctions in the illative theory.

The principal result concerning λ -conversion is the Church–Rosser theorem. This states that if X cnv Y, then one can find effectively a Z such that X red Z and Y red Z. Thus, two different combinations of variables are never interconvertible; this establishes consistency. In 1936, Alonzo Church and J. B. Rosser ("Some Properties of Conversion," in Transactions of the American Mathematical Society 39, pp. 472–482) proved the theorem for λIβ -conversion; it has since been extended to all forms of λ -conversion.

The decision problem for all equations X = Y was shown by Church in 1936 ("An Unsolvable Problem of Elementary Number Theory," in American Journal of Mathematics 58, pp. 345–363) to be recursively unsolvable, as was the problem of determining whether X has a normal form. This result was the basis of Church's later proof of the recursive unsolvability of the decision problem for predicate calculus.

Since every kind of λ -conversion is equivalent to a synthetic theory and vice versa, the results described below for the synthetic theory are also results of λ -conversion and in some cases were first so obtained.

foundations of pure synthetic theory

Table 1 contains a list of special combinators. The names assigned to the combinators are in the first (X ) column and the values of m and M to be used in equation (3) are in the second and third columns. The other columns will be explained later. In the various formulations certain of the combinators will be atomic; the corresponding equations (3) will then be assumed as axiom schemes in which 'x ₁', · · ·, 'x_m ' stand for arbitrary obs.

We seek to define, for arbitrary M, x ₁, · · ·, x_m, an X such that (3) holds. The X so defined will be [x ₁,· · ·, x_m ]M ; this means the same thing as λx ₁· · ·x_mM but is a defined, not a postulated, concept. One way of defining it is to use an induction on m, as above, and then, for m = 1, an induction on the structure of M. The latter can be obtained, for instance, by defining X to be K M when M does not contain x, to be I when M is x, and to be S X ₁X ₂ when M ≡ M ₁M ₂ and we have already defined X ₁ ≡ [x ]M ₁, X ₂ ≡ [x ]M ₂. Such an algorithm defines all combinators in terms of I, K, S as atoms; the definitions are very long, but suitable modifications improve matters. The fourth column of the table gives some definitions obtained by suitably modified algorithms. Other modifications give definitions in terms of I, B, C, S for all cases where M actually contains x ; these are suitable for an analogue of λ I-conversion.

Thus, we get a definition for [x ]M compatible with any of the forms of λ-conversion if we postulate schemes (3) as stated, together with the properties of equality. The analogues (with [x ]M in place of λxM ) of (α) and (β ) will then hold. But we do not have the analogue of (ξ ), nor do we have an extensionality principle
(ζ)U ₁x = U ₂x → U ₁ = U ₂
even under the restrictions that are appropriate for λβ -conversion. One can obtain these properties by adjoining a finite number of combinatory axioms. Examples of these axioms are
(4)      SK = KI ,
(5)      ΨSK = BK .
Given a form of λ -conversion, we can choose these axioms so that there is a many–one mapping of the resulting system into the λ -conversion and another one vice versa, such that an equation in either system is a theorem exactly when its image is in the other. Thus, λ -conversion and the synthetic theory are equivalent. Bruce Lercher, in 1963, extended these considerations to include (δ ).

It is possible to define, in several ways, a combinator Y such that for any X, Y X = X (Y X ). If Γ means negation, then Y Γ means the same as its own negation. For Y ≡ WS (BWB ), this is the notion at the root of the Russell paradox. Thus, in a combinatorially complete system one cannot exclude the paradoxes; one must explain them in the illative theory.

In the foregoing, equality can be taken as primitive. Then the axioms consist of the combinatory axioms, all instances of the reflexive law, and (3) (for atomic combinators); the rules are the usual rules for equality. When we press the analysis deeper so as to define equality by (2), the schemes (3) become rules; for example, that for S gives the pair of rules (one in each sense)
(6)      ⊦ U (S XYZ ) ⇄ ⊦ U (XZ (YZ )),
whereas reflexivity can come from an axiom. The result is a system with a finite number of axioms (no axiom schemes) and about a dozen rules, each with one or two premises and otherwise no more complex than (6) and such that the premises uniquely determine the conclusion. There are also only a finite number of atoms—variables are used only in the metatheory—and the single operation of application. The structure is therefore very simple. But all functions of variables can be performed therein, and with suitable illative additions it can form a basis for almost any logical system.

combinatory arithmetic

From the formal standpoint the natural numbers are constructions from a single atom, 0, by a single unary operation, σ. On this basis one can develop the usual recursive arithmetic, and one can explain how to count. Assume that such a system is given, represented, say, in the words in some alphabet

with only one letter. These words we shall call the natural numbers. Further, let σ be the successor function, δ the predecessor function, τ the ordered-pair function, and μ the operation such that for any numerical function ƒ, μƒ is the least n for which ƒ (n ) = 0 and is undefined if there is no such n.

One can find a representation of the natural numbers as combinators; indeed, there are many choices. For any such choice let angle brackets "〈 〉" symbolize the combinatory analogues of the arithmetic notions indicated within them. Thus, 〈n 〉 is, for any numeral n, the combinatory numeral which represents it, 〈+〉 the analogue of addition, etc. The analogues are often not uniquely determined.

The first representation, by Church in 1933, chose 〈n 〉 so that 〈n 〉ƒ is the n th iterate of ƒ (the first iterate being ƒ itself). If one has K , then 〈0〉 is KI and 〈σ 〉 is SB . Then 〈n 〉 is the Z _n of H. B. Curry and Robert Feys (Combinatory Logic ). Further, 〈+〉, 〈·〉, and 〈e 〉>, where e (x,y ) = x^y, have simple definitions (for example, ϕB, B , and CI , respectively) from which their arithmetical properties follow. There are other proposals for combinatory numerals; one, made by Dana Scott in 1963, has a simple 〈δ 〉. For the sake of generality, 〈n 〉 is here unspecified, but a Z is postulated such that Z 〈n 〉 = Z _n. If 〈n 〉 ≡ Z _n, then Z ≡ I .

Next one can define combinators D (≡ 〈τ 〉), D ₁, D ₂ such that
D ₁(D xy ) = x, D ₂(D xy ) = y.
For instance (as Paul Bernays suggested in 1936),
D = [x,y,z ].Z z (K y )x.
For this
(7)      D xy 〈0〉 = x, D xy 〈σn 〉 = y,
so that D ₁ and D ₂ can be [x ]x 〈0〉 and [x ]x 〈1〈, respectively. One can also define D in terms of 〈δ 〉 rather than Z .

Next a combinator R can be defined such that
(8)      R xy 〈0〉 = x, R xy 〈σ 〉 = y 〈n 〉(R xy 〈n 〉).
If x = 〈g 〉 and y = 〈h 〉, where g and h are, respectively, k -place and (k + 2)-place numerical functions, R xy can be taken as 〈ƒ 〉, where ƒ is the (k + 1)-place numerical function defined by the "primitive recursion scheme" from g and h. Since the other processes of forming primitive recursive functions have combinatory analogues, definition of R will ensure that 〈ƒ 〉 is defined for any primitive recursive ƒ.

Several definitions of R exist. The first (given by Bernays in 1936) depends on the fact that ƒ (n ) can be obtained (for k = 0, as an example) by iterating n times, starting with τ (0,g ), the function ϕ such that ϕ (τ (x,y )) = t (σx,h (x,y )) and taking the second member. This leads to the definition (in two stages)
Y ≡ [u ]D (〈σ 〉(D ₂u )) (y (D ₁u ) (D ₂u )),
R ≡ [x,y,z ](D ₂(Z zY (D 〈0〉x ))).
Another possibility is to define a combinator Ω such that for given obs p, q, r, the ob t = Ωpqr satisfies the conditions

thus:

Y ≡ D (K p )([u ](q ([z ](u (rz )uz )))),
Ω ≡ [p,q,r,x ](Y (rx )Y x ).
For p ≡ K x, q ≡ [u,z ](y (〈δ 〉z )(u (〈δ 〉z ))), r = I , the ob [x,y ]Ωpqr is an R , different from the foregoing, satisfying (8). There are still other ways of defining R . Since 〈δ 〉 can be defined as R 〈0〉K and Z as R (KI )(K (SB )), we have any primitive recursive function as soon as we have either Z or 〈δ 〉 and a discrimination for 〈0〉.

We can go further. If we take p ≡ I , q ≡ [u,z ] (u (〈σ 〉z )), while r is a given function 〈g 〉, then Ωpqr is an 〈ƒ 〉 such that ƒ (n ) = n if g (n ) = 0 and otherwise ƒ (n ) = ƒ (σn ). This shows that we can define 〈μ 〉 in terms of the above q as [x ](ΩIqx 〈0〉). Consequently, every partial recursive numerical function is definable by combinators. The converse of this thesis follows by the usual arguments involving Gödel numeration.

These conclusions are not greatly affected if one restricts the system to correspond with restricted forms of λ -conversion. The passage from η -conversion to β -conversion hardly makes any difference. The omission of K complicates things somewhat—one needs ordered triples instead of ordered pairs. But the main conclusion, that every partial recursive function is definable by combinators and vice versa, stands.

Some generalizations are known. One can define by combinators certain transformations between obs and their Gödel numbers. An extension to recursive functionals of certain types can be obtained by using an analogue of (δ ). There is also an extension to certain transfinite ordinal numbers.

illative theory

By definition illative combinatory logic includes all considerations where there are atoms which neither are combinators nor are necessary to express equality. We consider here those cases in which the new atoms mean ordinary logical notions—for example, II (absolute universality), P (implication), Ξ (relative universality or formal implication), F (functionality—F XYZ means that Z is a function from X into Y ), Σ (instantiality), Λ (conjunction), Γ (negation), Θ (descriptive quantifier), etc. In addition, we need obs meaning semantical categories, such as E (the category of all obs—E is definable, for example, as WQ ), H (propositions), J (individuals), M (sets), N (numbers), etc.

The meaning of these obs is expressed more precisely by the rules associated with them. For the first four obs these are

rule Π:     ⊦ΠX & ⊦EU → ⊦XU.
rule P :     ⊦P XY & ⊦X → ⊦Y.
rule Ξ :     ⊦Ξ XY & ⊦XU → ⊦YU.
rule F :     ⊦F XYZ & ⊦XU → ⊦Y (ZU ).
These rules, when relevant, are to be postulated in addition to the combinatory rules given earlier; the latter can be summarized as
rule Eq:
⊦X & X = Y → ⊦Y.

These notions are, of course, interdefinable; in fact, one can take as atoms either F , Ξ, or Π and P and define the others as follows (there are two possible definitions for Ξ in terms of F ):
F ≡ [x,y,z ](Ξx (B yz )),
Ξ ≡ [x,y ](Π([z ](P (xz )(yz )))),
Π ≡ ΞE ,
P ≡ ΨΞK = [x,y ](Ξ(K x )(K y )),
Ξ′ ≡ [x,y ](F xy I ),
Ξ″ ≡ [x,y ](F x I y ).
The system based on F as primitive is called ℱ₁, or the theory of functionality ; that on Ξ as ℱ₂, or the theory of restricted generality ; and that on Π and P as ℱ₃. With reasonable axioms, these are listed in order of increasing strength.

Although the Church–Rosser theorem shows that pure combinatory logic is consistent, in the illative theory one easily runs into contradictions. Thus, if one were to assume
(10)      ⊦P (P α(P αβ))(P αβ)
as an axiom scheme, with the Greek letters standing for arbitrary obs, the theory would be inconsistent in the sense that (1) would hold for any X. But (10) is a thesis of the absolute (that is, positive intuitionistic) propositional algebra. Thus, it is necessary, if the theory is to contain this algebra, that (10) be a theorem scheme with a restricted range for the Greek letters. In its early stages illative combinatory logic will have axiom schemes with such restrictions. Later, perhaps, these schemes will be reduced to axioms by quantifying over a suitable category.

This requires some sort of machinery of categories or types. Such machinery is taken for granted in the usual systems of mathematical logic. It consists of four items: (a ) a list of primitive categories (such as those listed above), (b ) devices for forming derived categories, (c ) assignments of the primitive notions to categories, (d ) means for determining the categories of composite notions. Of these items (a ) and (c ) are special to the theory considered, but (b ) and (d ) are general processes which are appropriate for study in combinatory logic. Since composite obs are formed by application alone, one would expect a means of assigning a category to XY when those for X and Y are known; the general principle is that if X is a function from α to β and Y belongs to α, then XY belongs to β. This principle is expressed by Rule F , so the basis for this generalized theory of types is ℱ₁.

From the illative standpoint one would expect that each combinator would be assigned a category depending on parameters expressing that it is a function transforming from certain sorts of categories to categories of certain other sorts. Such functional characters for some basic combinators of the table are listed there in the fifth column. Assignments of these characters to the atomic combinators would then be axiom (or at least theorem) schemes of ℱ₁. However, these schemes cannot be accepted with the Greek letters standing for arbitrary obs, for if one so accepts FW , the theory is again inconsistent. Even ℱ₁ has to be formulated with restrictions on the Greek letters.

The most radical restriction is the requirement that the Greek letters range over an inductive class of F-obs generated from certain otherwise unspecified atoms θ ₁, θ ₂, · · · by the operation of forming F αβ from α and β. One further restricts Rule Eq thus:
rule Eq′:
⊦ξX & X = Y → ⊦ξY.
The resulting theory is called the basic theory of functionality. In this theory every elementary statement will be of the form
(11)      ⊦ξX,
where ξ is an F-ob and X is a combinator. The theory is demonstrably consistent. If X is a stratified combinator—that is, if X satisfies (3) and one can derive ⊦ηM by Rule F alone from the axiom schemes and assignments of categories to the variables—then one can derive a statement of the form (11) stating that X has the appropriate functional character. There is a converse to this which is somewhat difficult to state, but it shows that the X 's for which (11) can be derived are greatly restricted; in particular, they have a normal form.

There are several "stronger" theories of functionality with less drastic restrictions. A theory in which one uses only combinators that do not repeat variables can be constructively proved consistent without restrictions on the Greek letters. Constructive consistency proofs have been obtained for some other theories of ℱ₁.

All these systems of ℱ₁ are extremely weak. To obtain stronger and natural theories one proceeds to ℱ₂ (or adds assumptions to ℱ₁ which are equivalent to this). In ℱ₂ reasonable schemes ΞI , ΞK , etc., with Greek letters restricted to a class of "canonical obs," can be formulated from which the corresponding FI, FK , · · · can be derived. Thus, ℱ₂ has a deduction theorem; it also includes the absolute propositional calculus of pure implication. There is a Gentzen-like theory of "verifiability" from which it follows that certain weak forms of the illative theory are consistent.

The study of illative combinatory logic is still in its preliminary stages. Little is known, for example, about ℱ₃. It is clear that ordinary logical systems can be founded on a combinatory basis, but little has been published along this line. On such a basis E. J. Cogan, in 1955, analyzed the foundations of Gödel's set theory and also the predicate calculus and some other calculuses; owing to an unfortunate oversight in the definition of "class," the system was inconsistent, as Rainer Titgemeyer showed in 1961, but the necessary changes are rather minor. Other investigations of this sort are in the process of development or publication. Some authors, such as F. B. Fitch, go in a somewhat different direction.

In illative combinatory logic we are dealing with concepts of such generality that we have little intuition in regard to them. This explains why proposals by competent logicians beginning with Gottlob Frege (not all combinatory, but the principle applies) have later proved inconsistent. We must, indeed, proceed by trial and error. No doubt we shall continue to find both inconsistencies in weaker systems and consistency proofs of stronger systems. In due course nonfinitary methods will be used, and much is to be expected of them. But the possibility remains that we may always be interested in systems for which neither consistency nor inconsistency is known.

Combinatory logic was inaugurated by Moses Schönfinkel in 1924. He introduced the notion of application, the combinators B, C, I, K, S (his Z, T, I, C, S ), and an illative notion U. He showed how statements of logic could be expressed in terms of these notions, but he gave no deductive theory of them. He became ill shortly after writing the paper and was unable to do anything further in the subject. Curry, beginning in 1929, produced the first deductive synthetic theory and introduced the terminology used here. The theory of λ-conversion was developed by Church from 1932. Subsequent improvements were made by these authors and by Rosser, S. C. Kleene, Bernays, Fitch, and Paul Rosenbloom. The present state of the subject is the result of an interaction of the work of these authors and their students.

See also Church, Alonzo; Frege, Gottlob; Logical Paradoxes; Logic, History of; Quantifiers in Formal Logic.

Bibliography

Items listed here either are of broad scope or treat aspects of the subject not included in the text. For sources, details, etc., see the bibliographies in the works cited.

Church, Alonzo. The Calculi of Lambda-Conversion. Princeton, NJ: Princeton University Press, 1941; 2nd ed., 1951. The standard work on λ-conversion, with references.

Church, Alonzo. "The Richard Paradox." American Mathematical Monthly 41 (1934): 356–361. Expounds a system modeling illative notions on the pure theory.

Cogan, E. J. "A Formalization of the Theory of Sets from the Point of View of Combinatory Logic." Zeitschrift für mathematische Logik und Grundlagen der Mathematik 1 (1955): 198–240. Contains a readable introduction and some information on illative theory going beyond Curry and Feys (below). For an inconsistency, see text, section on illative theory.

Curry, H. B. "The Elimination of Variables by Regular Combinators." In The Critical Approach to Science and Philosophy, in honor of Karl R. Popper, edited by Mario Bunge, pp. 127–143. New York: Free Press of Glencoe, 1964. Contains, on pp. 128–131, a discussion of the "ontology" of combinatory logic, partly in answer to Quine (below).

Curry, H. B., and Robert Feys. Combinatory Logic, Vol. I. Amsterdam: North-Holland, 1958. A monograph, with full bibliography, historical sketch, etc.

Fitch, F. B. "The System CΔ of Combinatory Logic." Journal of Symbolic Logic 28 (1963): 87–97. A nonfinitary system with consistency proof. Refers to Fitch's other papers.

Quine, W. V. "Variables Explained Away." Proceedings of the American Philosophical Society 104 (1960): 343–347. An alternative formulation of combinatory logic, to be used in combination with first-order predicate calculus, which, Quine claims, involves fewer ontological presuppositions.

Rosenbloom, Paul. The Elements of Mathematical Logic. New York: Dover, 1950. Very compact. Departures from standard notations hinder reading.

Rosser, J. B. Deux Esquisses de logique. Paris: Gauthier-Villars, 1955. A masterly exposition of certain parts of the pure theory.

Schönfinkel, Moses. "Über die Bausteine der mathematischen Logik." Mathematische Annalen 92 (1924): 305–316. Still readable and interesting for motivation. The statement in the postscript (by Heinrich Behmann) to the effect that parentheses can be eliminated by Z (that is, B ) alone is erroneous.

Haskell B. Curry (1967)