The Cost of Types

Russell's paradox begins with a phrase that looks grammatical: “the set of all sets that do not contain themselves.” One response is to ask whether the phrase should have been allowed into a mathematical statement at all. Type theory develops that response. It offers a disciplined grammar, then asks how much ordinary mathematics can still be expressed within it.

A grammar with levels

In a simplified picture of simple type theory, individuals occupy one type; collections of individuals occupy a second; collections of those collections occupy a third. A membership statement is well formed only when its right-hand side has the appropriate higher type:

$$\operatorname{type}(b)=\operatorname{type}(a)+1 \qquad\text{for }a\in b.$$

An expression such as $x\in x$ would require $x$ to be both one type and the next. It is rejected before we ask whether it is true. The proposed Russell set cannot be assembled from a condition that is not well formed.

This ladder is a modern teaching model, not a literal transcription of every detail of Principia Mathematica. Russell and Whitehead worked with propositional functions as well as classes, and their full system used more than one kind of hierarchy. The simple picture isolates the protective idea: a rule about a whole collection should not automatically be applicable to itself.

The vicious-circle principle

Russell and Whitehead described the problem in terms of a vicious circle. A definition becomes suspect when it quantifies over a totality that is supposed to include the very object being defined. Such a definition is called impredicative. The familiar sentence “this sentence is false” shows why self-reference can be troubling, although semantic paradoxes require their own careful treatment of truth and language.

An impredicative definition is not automatically contradictory. In ordinary mathematics we often define an object by reference to a larger totality. For example, the least upper bound of a bounded nonempty set $E$ of real numbers is a real number $s$ satisfying

$$\bigl(\forall x\in E\;x\leq s\bigr) \;\land\; \bigl(\forall y\,[(\forall x\in E\;x\leq y)\Rightarrow s\leq y]\bigr).$$

The second clause compares $s$ with every upper bound. It is mathematically useful. A foundational system must explain why the required quantification is legitimate rather than simply banning every definition with a broad range.

Why ramification became difficult

The ramified theory of types added orders to the hierarchy. Roughly, the order of a propositional function records the quantifiers over other functions that enter its definition. A property defined by quantifying over a wide range of properties may therefore belong to a higher order than the properties it discusses.

This is where analysis became awkward. Standard arguments about real numbers use classes and properties defined through quantification over already available real-number properties. Ramification can keep the resulting classes at different orders, interrupting arguments that ordinarily treat them together. The issue is about the order of definitions and propositional functions. It does not mean that taking a supremum literally turns a real number into a “higher-order real number.”

Russell and Whitehead wanted the restrictions that block paradox and the expressive power needed for classical mathematics. They added further principles to connect the two.

Three additional commitments

Reducibility

The axiom of reducibility says that a propositional function of any order has a coextensive predicative function of the appropriate lowest order. They agree on which arguments satisfy them:

$$\forall x\bigl(\varphi(x)\leftrightarrow\psi(x)\bigr).$$

This is a schematic explanation; the actual axiom in Principia keeps track of argument types and orders. Reducibility allows higher-order descriptions to be represented where ordinary mathematical reasoning can use them. It also raises a philosophical challenge. If this powerful extra principle is needed, what makes the resulting arithmetic a consequence of logic alone?

Infinity and choice

An axiom of infinity supplies an infinite population at the relevant base type. Logic by itself does not assert that there are infinitely many individuals. This is a claim about the system's domain, not a claim that physical space contains infinitely many objects.

The multiplicative axiom plays a role analogous to a form of the axiom of choice: it supports the selection of one member from each of a family of nonempty classes. These two assumptions address different needs from reducibility. One supplies enough individuals; the other permits certain selections.

What the trade-off reveals

Principia Mathematica showed how far a carefully stratified language could take the logicist program. Its additional axioms and intricate syntax also made the cost visible. A secure grammar may demand substantial work to recover familiar mathematics.

This is no verdict against type theory as such. Later type theories differ greatly from Russell and Whitehead's system and remain active foundations for mathematics and computing. In the early twentieth-century debate, however, another route offered a striking contrast: keep one kind of set variable, and place the restrictions on the axioms that assert sets exist.

Sources

• Russell and Whitehead, Principia Mathematica, Introduction, Chapter II (1910), on types, the vicious-circle principle, and reducibility.
• Russell, Introduction to Mathematical Philosophy (1919), especially the chapters on classes and the logicist program.