ABSTRACT

CL proved to be quite powerful in itself, as we have already seen in chapters 2 and 3. The original motivations to develop CL were not primarily the goal to capture the notion of computable functions, but to eliminate bound variables and to provide a framework for the foundations of mathematics. Curry and his students created illative combinatory logic, that we briefly outlined in chapter 8. Scho¨nfinkel had not had a chance to expand the elimination of bound variables to higher-order logics, or to investigate the consequences of the addition to CL of sentential or predicate logic. However, the early systems that were proposed to provide a general framework for the foundations of mathematics proved to be inconsistent. Still, some of the ideas behind the theory of functionality, that was invented by Curry in this context, proved very fruitful both theoretically and in applications.