I. INTUITIONISTIC PROPOSITIONAL CALCULUS

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 $K = \lambda X. \lambda Y.X$ corresponds to the axiom $\alpha \supset \  (\beta \  \supset \  \alpha )$.

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 $\lambda $-terms (W. W. Tait, 1965). It is convenient to use $\lambda $-terms rather than combinators. This corresponds to the sequent formulation of propositiona1 logic1.

Footnotes

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