Type Theory |
Type theory, in one sense, is the view that some category of abstract entities—sets, in the simplest example, but there are analogous views of properties, relations, concepts, and functions—come in a hierarchy of levels, with an entity of one level applying to (having as members, or having as instances, or ...) entities only of a lower level.
Such a view gives an intuitively comprehensible picture of the universe of abstracta and provides a principled way of avoiding Bertrand Arthur William Russell’s Paradox and its analogues. In a second sense, the term refers to any of a wide range of formal axiomatic systems embodying some form of the view. The present entry gives a short history of the view and a brief survey of the systems.
The systems are generally formulated in many-sorted quantificational logic, with a separate alphabet of quantified variables ranging over each type of entity. Axiomatically, they incorporate the rules of propositional logic (usually though not always classical) and of quantifier logic, the latter reduplicated for each alphabet of variables.