Russell’s theory of types


After the discovery of the paradoxes of set theory (notably Russell’s paradoxMathworldPlanetmath), it become apparent that naive set theory must be replaced by something in which the paradoxes can’t arise. Two solutions were proposed: type theoryPlanetmathPlanetmath and axiomatic set theory based on a limitation of size principle (see the entries class and von Neumann-Bernays-Gödel set theoryMathworldPlanetmath).

Type theory is based on the idea that impredicative definitions are the root of all evil. Bertrand Russell and various other logicians in the beginning of the 20th century proposed an analysis of the paradoxes that singled out so called vicious circles as the culprits. A vicious circle arises when one attempts to define a class by quantifying over a totality of classes including the class being defined. For example, Russell’s class R={xxx} contains a variable x that ranges over all classes.

Russell’s type theory, which is found in its mature form in the momentous Principia Mathematica avoids the paradoxes by two devices. First, Frege’s fifth axiom is abandoned entirely: the extensionsPlanetmathPlanetmathPlanetmathPlanetmath of predicatesMathworldPlanetmath do not appear among the objects. Secondly, the predicates themselves are ordered into a ramified hierarchy so that the predicates at the lowest level can be defined by speaking of objects only, the predicates at the next level by speaking of objects and of predicates at the previous level and so forth.

The first of these principles has drastic implicationsMathworldPlanetmath to mathematics. For example, the predicate “has the same cardinality” seemingly can’t be defined at all. For predicates apply only to objects, and not to other predicates. In Frege’s system this is easy to overcome: the equicardinality predicate is defined for extensions of predicates, which are objects. In order to overcome this, Russell introduced the notion of types (which are today known as degrees). Predicates of degree 1 apply only to objects, predicates of degree 2 apply to predicates of degree 1, and so forth.

Type theoretic universePlanetmathPlanetmath may seem quite odd to someone familiar with the cumulative hierarchy of set theory. For example, the empty setMathworldPlanetmath appears anew in all degrees, as do various other familiar structuresMathworldPlanetmath, such as the natural numbersMathworldPlanetmath. Because of this, it is common to indicate only the relative differences in degrees when writing down a formulaMathworldPlanetmathPlanetmath of type theory, instead of the absolute degrees. Thus instead of writing

P1x0(x0P1x0x0)

one writes

Pi+1xi(xiPi+1xixi)

to indicate that the formula holds for any i. Another possibility is simply to drop the subscripts indicating degree and let the degrees be determined implicitly (this can usually be done since we know that xy implies that if y is of degree n, then x is of degree n+1). A formula for which there is an assignment of types (degrees) to the variables and constants so that it accords to the restrictionsPlanetmathPlanetmathPlanetmath of type theory is said to be stratified.

The second device implies another dimension in which the predicates are ordered. In any given degree, there appears a hierarchy of levels. At first level of degree n+1 one has predicates that apply to elements of degree n and which can be defined with reference only to predicates of degree n. At second level there appear all the predicates that can be defined with reference to predicates of degree n and to predicates of degree n+1 of level 1, and so forth.

This second principle makes virtually all mathematics break down. For example, when speaking of real number system and its completeness, one wishes to quantify over all predicates of real numbers (this is possible at degree n+1 if the predicates of real numbers appear at degree n), not only of those of a given level. In order to overcome this, Russell and Whitehead introduced in PM the so-called axiom of reducibility, which states that if a predicate Pn occurs at some level k (i.e. Pn = Pnk), it occurs already on the first level.

The philosopher and logician Frank Plumpton Ramsey (1903-1930) was the first to notice that the axiom of reducibility in effect collapses the hierarchy of levels, so that the hierarchy is entirely superfluous in presence of the axiom. The original form of type theory is known as ramified type theory, and the simpler alternative with no second hierarchy of levels is known as unramified type theory or simply as simple type theory.

One descendantPlanetmathPlanetmath of type theory is W. v. Quine’s system of set theory known as NF (New Foundations), which differs considerably from the more familiar set theories (ZFC, NBG, Morse-Kelley). In NF there is a class comprehension axiom saying that to any stratified formula there corresponds a set of elements satisfying the formula. The Russell class is not a set, since it contains the formula xx, which can’t be stratified, but the universalPlanetmathPlanetmathPlanetmath class is a set: x=x is perfectly legal in type theory, as we can assign to x any degree and get a well-formed formula of type theory. It is not known if NF axiomatises any extensor (see the entry class) based on a limitation of size principle, like the more familiar set theories do.

In the modern variants of type theory, one usually has a more general supply of types. Beginning with some set τ of types (presumably a division of the simple objects into some natural categoriesMathworldPlanetmath), one defines the set of types T by setting

  • if a,bT, then (ab)T

  • for all tτ, tT

One way to proceed to get something familiar is to have τ contain a type t for truth values. Then sentencesMathworldPlanetmath are objects of type t, open formulae of one variable are of type 𝐎𝐛𝐣𝐞𝐜𝐭t and so forth. This sort of type system is often found in the study of typed lambda calculus and also in intensional logics, which are often based on the former.

Title Russell’s theory of types
Canonical name RussellsTheoryOfTypes
Date of creation 2013-03-22 13:49:27
Last modified on 2013-03-22 13:49:27
Owner Aatu (2569)
Last modified by Aatu (2569)
Numerical id 10
Author Aatu (2569)
Entry type Definition
Classification msc 03B15
Related topic Class
Related topic HilbertsVarepsilonOperator
Defines type theory
Defines ramified type theory
Defines simple type theory
Defines axiom of reducibility
Defines stratification
Defines NF
Defines theory of types
Defines simple theory of types
Defines ramified theory of types