Paradoxes and Type Theory

Mathematical Logic Philosophy of Mathematics

David Baños Abril

12 de July de 2026 16 min read

In the previous article, we explained two of the paradoxes that had the greatest impact on early 20th-century mathematics: Russell's Paradox and Cantor's Paradox. These paradoxes posed a challenge to the logicist project. The Theory of Types developed by Russell would go on to resolve these problems.

The Concept of Paradox

One of the most elementary principles of any formal language, such as those used in every branch of mathematics, is the ability to distinguish true theorems from false ones. Every closed mathematical expression has one and only one truth value: true or false. Paradoxes challenge this principle. Without entering into technical definitions, a paradox or antinomy involves starting from an assertion that we unquestionably take to be true, but which ultimately leads us to a deduction that appears to deny it. Constructing such an assertion forces us to assign it incompatible values, revealing a defect in the premises or in the language being used.

The Liar Paradox

Let us consider what is perhaps the most famous example of a paradox: the Liar Paradox, also known as the Paradox of Epimenides. Epimenides was a prophet of Ancient Greece. Horrified by the blasphemies of the Cretans, he proclaimed that they were all liars. However, Epimenides was himself a native of Crete, so his statement applied to him as well.

In simplified form, the Liar Paradox can be stated as follows: “what I am saying is false.” If the statement is true and what it says is indeed false, then it is false. If we initially take it to be false, it can only be true.

Logical Paradoxes

A distinction is commonly made between two types of paradoxes: semantic paradoxes, such as the Liar Paradox discussed above, and logical-mathematical paradoxes. The latter are those examined in the previous article and concern sets and classes: Russell’s Paradox, involving sets that do not contain themselves; the Burali-Forti Paradox, involving the set of all ordinals; and Cantor’s Paradox, involving the set of all cardinals. We shall see that both types of paradox have a similar origin related to self-reference.

Impredicative Definitions

Paradoxes involve problematic definitions that fall into what the mathematician Henri Poincaré called a vicious circle. A vicious circle involves self-reference: defining an element by referring to the totality of which it forms a part. Definitions that involve a vicious circle are known as impredicative. A predicative definition, by contrast, establishes independence between the properties that define an element and the domain of objects to which it belongs.

In 1905, Julius König published a semantic paradox that we shall use here to show how impredicative definitions can generate paradoxes.

König’s Paradox

König observed that numbers could be defined in natural language using a finite number of words, as in “the number after three” or “the number obtained by adding two and fifteen.” König concluded that the number of possible finite combinations of words is countable—that is, it has the infinity of the natural numbers—and therefore that any subset of these combinations, such as the strings that uniquely define a number, is also countable, with cardinality $\aleph_0$.

Cantor’s discoveries showed that the real numbers form a set of greater cardinality, so there must necessarily be numbers that cannot be described verbally. Yet we can construct a definition such as “the least number that cannot be defined using a finite number of words,” which is contradictory because this very definition contains only finitely many words.

Vicious Circle

When we analyse König’s Paradox, the vicious circle becomes clear. “The least number that cannot be defined using a finite number of words” is a definition that presupposes a completed totality of word strings. From this totality, we construct an impredicative property by including within it a reference to the very totality in which we intend to include the definition. The paradox arises from this self-reference.

The Paradox of Epimenides also contains a vicious circle. We begin with an apparently complete totality—everything asserted by the Cretans—and then introduce a new element that also belongs to that totality because Epimenides is himself a Cretan.

Russell’s Theory of Types

The large number of paradoxes discovered at the beginning of the twentieth century forced the logicist proposals to be reconsidered. Russell emphasised restricting the Comprehension Principle as a solution to the paradoxes. Recall that this principle asserted that every propositional function determines a class or, equivalently, that every property determines a set—possibly an empty one—of elements satisfying that property. Since paradoxical properties exist, however, Russell maintained that some propositional functions, specifically those that are impredicative, do not correspond to a class, or at least not to a class of the same order.

Functions and Propositions

Russell distinguishes between propositions and propositional functions. He defines a propositional function as a function containing one or more propositional variables, which refer to an undetermined value. A function is an unsaturated expression that contains variables and does not by itself constitute a true or false proposition. The function becomes a proposition when that variable is replaced by a specific value within a given range, a value that we shall call a term of that proposition. Unlike functions, propositions are regarded as saturated statements or closed statements with a specific truth value.

In this image, lowercase letters denote the different possible arguments ($a$, $b$, etc.) of the function (\P\)). The values produced by the function, shown on the right, are the different propositions ($P(a)$, $P(b)$), and so on.

Range of Significance

A function such as “$x$ is an astronomical object” cannot accept just any type of argument. We want to avoid expressions such as “‘$x$ is an object beyond the atmosphere’ is an astronomical object” or “‘Jupiter is an object beyond the atmosphere’ is an astronomical object.” In the first case, the function takes another function as its argument, while in the second it takes a proposition. In neither case does it make sense to ask whether the resulting expressions are true or false; they are simply meaningless, and we therefore want to exclude them from our logical language. We can, however, allow legitimate functions that take other functions as arguments, for example, “Jupiter is an object that satisfies the properties $X$.” The arguments accepted by a function of this kind cannot be the same as those in the preceding examples.

This distinction justifies the first hierarchy introduced by Russell in his Theory of Types: a function cannot take any arbitrary value as an argument but instead has a range of significance, that is, a range of arguments for which the function yields a legitimate value or proposition, regardless of whether it is true or false. Two functions that share the same range of significance cannot serve as arguments to one another.

Logical Types

Types form a hierarchy in which each new level depends on the preceding levels having been properly defined. At the first level are individuals $x$, which are neither functions nor propositions. We denote them using letters such as $a$, $b$, and $c$, or $x$ and $y$ when referring to an arbitrary individual. They are elementary objects without internal structure. They form the first type.

Functions whose arguments are individuals are called propositional functions and express properties of individuals. They form the second level of the hierarchy. Some examples are:

$$P(x) \quad R(x,y) \quad \forall x\lbrack Q(x,y)\rbrack \quad X(x)$$

These functions give rise to propositions when their variables are replaced by determinate objects. This can be done in two ways. The first is simply to assign specific objects to them. Thus, $P(a)$ or $P(a,b)$ would be closed or saturated propositions. Another possibility is to bind the variable with a quantifier. For example, $\forall x\lbrack Q(x,y)\rbrack$ still contains the free variable $y$, but if we quantify it, as in $\forall x \exists y \lbrack Q(x,y)\rbrack$, we obtain a proposition. The expression $ \forall x \neg (x \neq x)$ is likewise regarded as a closed proposition because $x$ is quantified. Every variable in a proposition must be bound or assigned a value for the expression to count as a proposition.

The next level consists of functions that attribute a property to other properties. Examples of third-type propositional functions include:

$$ \phi(X) \quad \rho(X,Y) \quad \forall X \lbrack \theta (X, Y) \rbrack \quad \chi(X) \quad \neg (X \neq X)$$

Once again, these functions become propositions when their variables are replaced by determinate values:

$$ \phi(P) \quad \rho(P,Q) \quad \forall X \exists Y \lbrack \theta (X, Y) \rbrack \quad \lambda(Q) \quad \forall X \neg (X \neq X)$$

We thus obtain a succession of levels: individuals, properties of individuals, properties of properties, and so on.

These levels of types already existed as such in the logical system proposed by Frege. Russell’s innovation was intended to resolve the problem of impredicative definitions and the paradoxes that follow from them.

Theory of Types and Paradoxes

Russell’s Paradox concerns whether the class comprising all classes that do not contain themselves contains itself. In the previous article, we represented it as:

$$\forall X[(X \in \xi) \leftrightarrow (X \notin X)]$$

The paradox arises when one of those classes $X$ is the class $\xi$ itself, since $\forall X$ refers to the totality of classes. According to the Theory of Types, however, $\xi$ does not fall within its own range of arguments. It is a class of a higher type than the classes $X$. The class $\xi$ is not included in the totality of classes referred to by $\forall X$, and substituting it into the expression therefore produces nonsense. Under the Theory of Types, a statement such as $x \in y$ is meaningful only when $y$ belongs to a type higher than $x$.

The Paradox of Epimenides could be resolved in the same way. The expression “what I am saying is false” refers to a totality: “what I am saying.” The expression itself therefore cannot belong to that totality; it must fall outside it, thereby preventing the paradoxical statement “‘what I am saying is false’ is false.”

Types and Orders

The Theory of Types seeks to avoid vicious circles and thereby block the antinomies caused by certain forms of self-reference. It does so by preventing an entity defined through reference to a totality from belonging to that same totality. The defined entity must be placed at a higher level. Our logical language must therefore distinguish between referring to an arbitrary object in a given domain and referring to all such objects as an already constituted totality.

Suppose that $\chi(X)$ expresses that the propositional function $X$ is one of the characteristic properties of a certain class of individuals. Since $\chi$ attributes a property to propositional functions of individuals, it is a predicate of the second type. We could then define a property $P$ of individuals as follows:

$$P(x)\leftrightarrow\forall X\bigl(\chi(X)\rightarrow X(x)\bigr)$$

This expression defines a propositional function of $x$, since $x$ is its only free variable. Its definition, however, quantifies over a totality of propositional functions $X$. Therefore, although $P$ applies to individuals just as the functions $X$ do, it cannot belong to the same order as all the functions over which it quantifies. It must be placed in a higher order.

This distinction separates the two hierarchies involved in Russell’s theory. The type of a function depends on the type of arguments it accepts. Its order, by contrast, depends on the totalities of functions over which its definition quantifies. Two functions may apply to the same type of objects yet belong to different orders.

Predicative Expressions

Within a single type, we can find functions belonging to different orders. Russell calls a predicative function one that belongs to the lowest order compatible with the type and order of its arguments. This does not mean that a predicative function must contain no quantifiers. A function such as $\exists y\,R(x,y)$ can be predicative even though it quantifies over individuals, provided that it is not defined by quantifying over a totality of functions that could include the function being defined.

By contrast, the function $P(x)$ defined above by

$$P(x)\leftrightarrow\forall X\bigl(\chi(X)\rightarrow X(x)\bigr)$$

does not belong to the lowest order of functions applicable to individuals, because its definition quantifies over propositional functions $X$ of that same type. It is therefore a function of a higher order.

The same distinction recurs at the following levels.

Ramified Theory of Types

Applying the vicious-circle principle does not prohibit every reference to a totality of functions. What it prohibits is using a totality to define a function that would have to belong to the same order as the functions contained within that totality. It is legitimate to quantify only over previously constituted totalities of functions belonging to lower orders.

The distinction between orders and types produces two different kinds of hierarchy. This additional hierarchy of orders is known as the Ramified Theory of Types.

Russell uses everyday examples to illustrate the problem. Napoleon is an individual, represented by $n$, who satisfies properties such as “$x$ is a flexible leader,” “$x$ is a daring military commander,” and “$x$ can recognise the weaknesses of his enemies.” These can be expressed through propositional functions of individuals such as $F(x)$, $A(x)$, and $D(x)$.

A property such as “possessing all the skills characteristic of a great general,” however, refers to a totality of properties. If $\varrho(X)$ expresses that $X$ is a property characteristic of a great general, we can write:

$$G(n)\leftrightarrow\forall X\bigl(\varrho(X)\rightarrow X(n)\bigr)$$

The property $G$ applies to individuals, but its definition quantifies over properties $X$. To avoid the vicious circle, the quantifier cannot range over a totality that includes the property $G$ itself. It must be restricted to previously defined properties belonging to lower orders. Therefore, $G$ is placed in an order higher than that of the properties $X$ over which it quantifies.

The Axiom of Reducibility

The ramified hierarchy imposed significant expressive limitations. To mitigate them, Russell proposed the so-called Axiom of Reducibility. In general terms, this axiom states that every propositional function, whatever its order, is coextensive with some predicative function of the same type. The two functions have the same truth value for every admissible argument, even though they need not share the same definition or necessarily express the same content.

If $P(x)$ is a function of any order, the axiom guarantees the existence of a predicative function $Q(x)$ such that:

$$\forall x\bigl(P(x)\leftrightarrow Q(x)\bigr)$$

Following the example of Napoleon, the property $G(x)$, defined by quantifying over properties, would belong to a higher order. The Axiom of Reducibility postulates the existence of some predicative property $H(x)$ that selects exactly the same individuals:

$$\forall x\bigl(G(x)\leftrightarrow H(x)\bigr)$$

The two properties are extensionally equivalent: if represented by Venn diagrams, they would delimit the same region. They need not, however, have the same meaning or be defined using the same resources.

The Axiom of Reducibility can be interpreted as partially restoring the extensional effect of the Comprehension Principle. It does not directly assert that every property determines an autonomous class, but rather that every higher-order function is equivalent, with respect to its truth values, to a predicative function. In extensional notation, the latter can be represented by an expression such as “$x$ belongs to $\alpha$,” where $\alpha$ collects the objects that satisfy the function. In Principia Mathematica, however, class expressions are treated contextually rather than as names of independent objects.

Problems with the Theory of Types

Russell’s Ramified Theory of Types was received with scepticism. The first hierarchy distinguished functions according to the type of arguments they admitted. The second reorganised them into different orders according to the functional variables over which their definitions quantified. Some critics regarded this ramification as an excessively complex and ad hoc solution to the newly discovered paradoxes.

The inclusion of the Axiom of Reducibility was no more convincing. Russell first introduced a hierarchy of orders to avoid vicious circles, but then postulated that every higher-order function was coextensive with some predicative function. The axiom did not formally eliminate the hierarchy, but it rendered many of its distinctions irrelevant from an extensional perspective. It seemed to recover by postulate precisely what the vicious-circle principle had restricted.

Russell defended his proposal by noting that some fundamental principles of logic and mathematics use impredicative quantification. This occurs in certain formulations of the Principle of Induction, which is central to arithmetic:

$$\bigl(P(0)\land\forall n\bigl(P(n)\rightarrow P(n+1)\bigr)\bigr)\rightarrow\forall n\,P(n)$$

This formulation is intended to apply to any property $P$, including properties whose definitions may quantify over totalities of properties. Ramification requires us to specify the order to which the variable $P$ belongs.

Something similar occurs in the characterisation of identity through the indiscernibility of properties. Two objects $x$ and $y$ are identical if and only if they satisfy exactly the same properties:

$$x=y\leftrightarrow\forall X\bigl(X(x)\leftrightarrow X(y)\bigr)$$

Here too, the expression quantifies over a totality of properties $X$, so the ramified theory must determine which orders of properties are included in that totality.

Conclusion

Russell’s Theory of Types, constructed to resolve the many paradoxes that had arisen in logic and naïve class theory—including the contradiction affecting Frege’s system—did not dispel doubts about the viability of the logicist project. Russell’s work sought, as Frege’s had before it, to integrate within a single theoretical framework the intensional perspective characteristic of logic and the extensional or set-theoretic perspective to which the first articles in this series were devoted.

The intensional perspective considers properties and the way in which they are defined. The extensional perspective, by contrast, considers the objects satisfying those properties. The Axiom of Reducibility was Russell’s proposed means of connecting the two levels: every property, however complex and impredicative its definition, was to be coextensive with some predicative property.

The proposal did not settle the debate. Russell later expressed serious reservations about the Axiom of Reducibility, while much of the subsequent development tended to replace ramified type theory with simpler theories of types. Ramification consequently lost much of its central role, although the distinction between logical levels remained a fundamental tool.

The Theory of Types introduces a question that will be relevant in later articles: the expressive limits of logical systems. Logic aspires to great generality and can be applied to everyday reasoning, scientific work, or even purely imaginary systems. Paradoxes show, however, that certain resources cannot be used without restriction without endangering consistency.

Natural language makes it easy to formulate self-referential expressions and apparently unrestricted references to “all things” or “all statements.” This flexibility does not imply superior logical powers: it comes with ambiguities that formal languages seek to avoid. The Theory of Types shows how a logical language can sacrifice some of that flexibility in order to gain precision and control the emergence of contradictions.