Double Identity Combinators Combinatorial logic was invented independently by M. Schönfinkel and HB Curry in the 1920s (Cf. Schönfinkel 1924, Curry 1930.). The impulse was to reduce the number of primitive notions needed for a logical system, especially for first-order logic. Schönfinkel used functions to provide a translation of a closed first-order formula into a functional expression, thus eliminating the bound variables of first-order logic. On the success of this attempt, see Curry & Feys 1968: In addition to this originally intended connection between first-order logic and combinatorial (illative) logic, there is another connection between the two, the so-called Curry-Howard isomorphism (Curry & Feys 1968, Howard 1980). This links combinators to implicational formulas. From Curry-Howard isomorphism it is a short step to putting combinatorial bases (possibly combinatorially incomplete) in correspondence with logical systems. It is known, for example, that the related system R® corresponds in the aforementioned sense to the combinatorial basis {B, C, W, I}. Naturally these combinatorial bases are not unique just as the axiomatizations are not unique. For example, the combinatorial basis {B', C, S, I} is equally suitable. (See Dunn 1986.)1. Double combinators. Pure combinators operate on left-bound sequences of objects. The result of an application of a combinator is a sequence composed of some of the objects on the left (possibly with repetitions) and sparse brackets:( . . . ( ( Q x1 ) . . . ) xn ) º ( xi 1 . xi m ) where any xi j (1£ j £ m) is xk (1£ k £ n) for some k , and the sequence on the right could be arbitrarily associated. The parentheses to the left of the identity are often omitted, as left binding is considered the default. To recall the more familiar combinatorics as an illustration of the general statement above we have: Sxyz º xz(yz), Kxy º x, Ix º x, Bxyz º x(yz), Cxyz º xzy, Wxy º xyy.Using the combinatorics Axioms above we can define the notions of one-step reduction (4 1), reduction (4 ), and weak equality (=w) as usual. (For an introduction to combinatorial logic see e.g. Hindley & Seldin 1986.) In case one is interested in a combinatorial basis that is not combinatorially complete, it might be useful to point out that the above notions are limited to the particular combinatorial basis.