The Logic of Types

Abstract

By the logic of types (TL) we mean systems of type transformation. The formulae of these systems are simply types or type transformation rules. For example, the system introduced by Ajdukiewicz (1935) (under the influence of Leśniewski’s doctrine of semantic categories) employs the schema:

$$({\text{ab}}){\text{a}} \to {\text{b,}}$$

((A.1))

which can be interpreted as a law or rule of type reduction. The much stronger system of Lambek (1935) also admits the schemata:

$$({\text{ab}})({\text{cb)}} \to ({\text{cb) (rediscovered by Geach 1986),}}$$

((1))

$$({\text{ab}}) \to (({\text{ca)(cb)),}}$$

((2))

, and many others. The system of van Benthem (1983a, 1985) affixes to the latter:

$${\text{a}} \to (({\text{ab)b) (implicit in Montague 1973)}}{\text{.}}$$

((3))

.