# Typed Combinatory Calculi (Tc)

## Pure Typed Combinatory Logic

There are two main historical reasons for the introduction of types.

The first type system was that devised by Russell for use in *Principia Mathematica*,
and published in a paper entitled *Mathematical Logic as based on
the Theory of Types*.
Russell's motivation in introducing this theory was to overcome the problems causing inconsistency in Frege's previous
attempt to reduce mathematics to logic, in a way which was both technically and philosophically satisfactory.

The motivation for introducing types into the systems of the Lambda-SKI cube is similar.
The introduction of type constraints *reduces* the expressiveness of the systems sufficiently to make it possible
to introduce quantifiers without rendering the systems inconsistent.
In particular, the introduction of a type system constrains the domains over which functions may be defined in a manner
similar to the constraints which are necessary in set theory for the theory to be consistent with the semantics of the
iterative heirarchy of sets.

We will consider in the systems around the Lambda-SKI cube the very simple type system introduced by Church for his
*Simple Theory of Types*, together with some small elaborations of that system which have proven desirable in practical
implementations and which were introduced in LCF and inherited by
HOL.

©
created 1995-12-9 modified 2005-12-28