UP Lambda-SKI cube

Type-Free Combinatory Logics (L)

Illative Combinatory Logic

Schönfields original paper on Combinatory Logic (On the building blocks of mathematical logic notes) presented the first account of a Combinatory Logic proper, since it incorporated a generalised Scheffer stroke.

While this provided a way of translating formulae of the predicate calculus into combinatorial notation, no independent account of the semantics of the notation was provided. A semantics derived from the predicate calculus would fail to determine the meaning of those terms of the calculus which could not be obtained by translation from the predicate calculus. The notational change is by itself of doubtful value if the more economic notations are not underpiinned by a sympathetic semantic treatment.

Considerable further work was undertaken by H.B.Curry and his collaborators, in an edeavour to establish type-free combinatory logics suitable for use as a foundation for mathematics. The results of Curry's programme were published in Combinatory Logic, Vols 1 & 2.

These systems have not however proved popular. While mathematicians work as if in a first order set theory, logicians (and increasingly computer scientists) have turned to a variety of typed systems (for the simplest of which, see typed combinatory and lambda logics).

up home © RBJ created 1995/12/9 modified 1995/12/10