# Type-Free Combinatory Logics (L)

## Illative Combinatory Logic

Schönfields original paper on Combinatory Logic
(*On the building blocks of
mathematical logic*
)
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).

©
created 1995/12/9 modified 1995/12/10