types, simple theory of

Theory developed by Bertrand Russell (1872-1970) to deal with paradoxes like his paradox of classes: is the class of all classes that are not members of themselves a member of itself? If yes, no; if no, yes.

Russell said there is no such class. Classes (and also properties) cannot all be lumped together, but form a hierarchy. Objects are of type zero. Classes of objects are of type one. Classes of type one classes are of type two, and so on. The class of all type n classes is of type n+1, but there is no class of all classes (or property which applies to all properties).

This is the simple theory, which Russell developed only as part of the ramified theory (see ramified theory of types). This latter (which also applies to propositions) resolves the various paradoxes, but lets us speak only of classes and so on of a given level; notions like class-membership, property, and truth (in the case of propositions) become systematically ambiguous over the hierarchy of levels of classes, properties, or propositions.

Other solutions have therefore been sought, but Russell’s paradox and similar ones revolutionized logic early in the 20th century.

Source:
I M Copi, The Theory of Logical Types (1971)

In mathematics, logic, and computer science, a type system is a formal system in which every term has a “type” which defines its meaning and the operations that may be performed on it. Type theory is the academic study of type systems.

Some type theories serve as alternatives to set theory as a foundation of mathematics. Two well-known such theories are Alonzo Church’s typed λ-calculus and Per Martin-Löf’s intuitionistic type theory.

Type theory was created to avoid paradoxes in previous foundations such as naive set theory, formal logics and rewrite systems.

Type theory is closely related to, and in some cases overlaps with, computational type systems, which are a programming language feature used to reduce bugs.