H. Curry (1958) has observed that there is a close correspondence between axioms of positive implicational propositional logic, on the one hand, and basic combinators on the other hand. For example, the combinator corresponds to the axiom .

The following notion of construction, for positive implicational propositional logic, was motivated by Curry’s observation. More precisely, Curry’s observation provided *half* the motivation. The other half was provided by W. Tait’s discovery of the close correspondence between cut elimination and reduction of -terms (W. W. Tait, 1965). It is convenient to use -terms rather than combinators. This corresponds to the sequent formulation of propositiona1 logic^{1}.

**Footnotes**

- http://red.ap.teacup.com/stromdorf/74.html