nLab Russell's paradox

Russells paradox

Context

Foundations

foundations

The basis of it all

 Set theory

set theory

Foundational axioms

foundational axioms

Removing axioms

Type theory

natural deduction metalanguage, practical foundations

  1. type formation rule
  2. term introduction rule
  3. term elimination rule
  4. computation rule

type theory (dependent, intensional, observational type theory, homotopy type theory)

syntax object language

computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory

logicset theory (internal logic of)category theorytype theory
propositionsetobjecttype
predicatefamily of setsdisplay morphismdependent type
proofelementgeneralized elementterm/program
cut rulecomposition of classifying morphisms / pullback of display mapssubstitution
introduction rule for implicationcounit for hom-tensor adjunctionlambda
elimination rule for implicationunit for hom-tensor adjunctionapplication
cut elimination for implicationone of the zigzag identities for hom-tensor adjunctionbeta reduction
identity elimination for implicationthe other zigzag identity for hom-tensor adjunctioneta conversion
truesingletonterminal object/(-2)-truncated objecth-level 0-type/unit type
falseempty setinitial objectempty type
proposition, truth valuesubsingletonsubterminal object/(-1)-truncated objecth-proposition, mere proposition
logical conjunctioncartesian productproductproduct type
disjunctiondisjoint union (support of)coproduct ((-1)-truncation of)sum type (bracket type of)
implicationfunction set (into subsingleton)internal hom (into subterminal object)function type (into h-proposition)
negationfunction set into empty setinternal hom into initial objectfunction type into empty type
universal quantificationindexed cartesian product (of family of subsingletons)dependent product (of family of subterminal objects)dependent product type (of family of h-propositions)
existential quantificationindexed disjoint union (support of)dependent sum ((-1)-truncation of)dependent sum type (bracket type of)
logical equivalencebijection setobject of isomorphismsequivalence type
support setsupport object/(-1)-truncationpropositional truncation/bracket type
n-image of morphism into terminal object/n-truncationn-truncation modality
equalitydiagonal function/diagonal subset/diagonal relationpath space objectidentity type/path type
completely presented setsetdiscrete object/0-truncated objecth-level 2-type/set/h-set
setset with equivalence relationinternal 0-groupoidBishop set/setoid with its pseudo-equivalence relation an actual equivalence relation
equivalence class/quotient setquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
-0-truncated higher colimitquotient inductive type
coinductionlimitcoinductive type
presettype without identity types
set of truth valuessubobject classifiertype of propositions
domain of discourseuniverseobject classifiertype universe
modalityclosure operator, (idempotent) monadmodal type theory, monad (in computer science)
linear logic(symmetric, closed) monoidal categorylinear type theory/quantum computation
proof netstring diagramquantum circuit
(absence of) contraction rule(absence of) diagonalno-cloning theorem
synthetic mathematicsdomain specific embedded programming language

homotopy levels

semantics

Russell's paradox

Idea

Russell’s paradox is a famous paradox of set theory1 that was observed around 1902 by Ernst Zermelo2 and, independently, by the logician Bertrand Russell. The paradox received instantly wide attention as it lead to a contradiction in Frege’s monumental “Foundations of Arithmetic” (1893/1903) whose second volume was just about to go to print when Frege was informed about the inconsistency by Russell.

The paradox entangles a concept with its own extension in a vicious circle. The attempt to overcome this circularity in set formation had a huge impact on subsequent forms of axiomatic set theory and in the aftermath mathematical logic became heavily focussed on consistency proofs for fully specified formal theories: the paradoxes triggered a shift in the foundation of mathematics away from the mathematics to the foundation itself.

Doch zur Sache selbst! Herr Russell hat einen Widerspruch aufgefunden, der nun dargelegt werden mag.3

Statement

If one assumes a naive axiom of full comprehension, one can form the set

R={x|xx}. R = \{ x | x \notin x \}.

One then asks: is RRR\in R? If so, then RRR\notin R by definition, whereas if not, then RRR\in R by definition. Thus we have both RRR\in R and RRR\notin R, a contradiction.

Russell’s paradox is closely related to the classical liar paradox (“this sentence is false”), to Gödel’s incompleteness theorem, and to the halting problem — all use a diagonalization argument to produce an object which talks about itself in a contradictory or close-to-contradictory way.

On the other hand, Cantor's paradox can be said to “beta-reduce” to Russell’s paradox when we apply Cantor's theorem to the supposed set of all sets. See Cantor's paradox for explanation.

Also related:

Resolutions

There are a number of possible resolutions of Russell’s paradox.

  • Russell himself (1903,1908,1910) proposed the introduction of type theory as a solution e.g. in Principia Mathematica (1910) an intricate system of ramified types tracks the variables of propositional functions in order to prevent circular propositions. This is inspired by Poincaré‘s ideas on impredicativity and can be viewed as a radical generalisation of Frege’s ontological distinction between an argument as a satured object and a function or concept as an unsaturated object.

  • The “classical” solution, adopted in ZFC and thus by the mathematical “mainstream”, is to restrict the axiom of comprehension so as to disallow the formation of the set RR: one requires that the set being constructed be a subset of some already existing set. The restricted axiom is usually given a different name such as the axiom of separation.

  • Another solution is to distinguish between sets and proper classes (= collections that are “too big” to be sets) as e.g. in NBG “set” theory.4 Here we may write down the definition of RR, but from RRR \notin R we may conclude RRR \in R only if we already know that RR is a set; the xx in the definition must be a set. So we have no contradiction, but only a proof that RR is a proper class.

  • In the set theory called New Foundations, the axiom of comprehension is restricted in a rather different way, by requiring the set-defining formula to be “stratifiable”. Since the formula xxx\notin x is not stratifiable, the set RR cannot be formed. This related to Russell’s ideas on ramified types.

  • In most structural set theories, the featurelessness of the elements of the structural sets secures the consistency of set formation. If sets cannot be elements of other sets, then the “definition” of RR is just a type error. The same is true in other structural foundational systems such as (modern, non-Russellian) type theory. However, Russell’s paradox can be recreated in structural foundations with inconsistent universes by constructing pure sets within them.

  • Alternatively, one can change the underlying logic. Passing to constructive logic does not help: although there is a seeming appeal to excluded middle (either RRR\in R or RRR\notin R), without using excluded middle we can obtain that RR is both not in RR and not not in RR, which is also a contradiction. However, passing to linear logic (or even affine logic) does help: there is an unavoidable use of contraction in the paradox. There exist consistent linear set theories? with the full comprehension axiom, in which RRR\in R implies RRR\notin R and vice versa, but we can never get both RRR\in R and RRR\notin R at the same time to produce a paradox. (See the Ph.D. thesis Linear Set Theory of Masaru Shirahata, completed under Grigori Mints supervision, Stanford University, 1994.)

  • Finally, and perhaps most radically, one can decide to allow contradictions, choosing to use a paraconsistent logic. There exist nontrivial paraconsistent set theories with full comprehension in which the set RR exists, being both a member of itself and not a member of itself.

References

Zermelo’s observation which is mentioned in a footnote of his 1908 paper on the well-ordering theorem is analyzed in

together with a transcription of a note dated 16 April 1902 by Husserl describing Zermelo’s proof.

Russell indicated the contradiction leading to the inconsistency of G. Frege’s system of “Grundgesetze der Arithmetik” in a famous letter to the latter on June 16th 1902 which together with Frege’s reply is reprinted pp.124-128 in

  • J. van Heijenoort (ed.), From Frege to Gödel - A Source Book in Mathematical Logic 1879-1931 , Harvard UP 1967.

A re-typed version is available from the blog post here.

For an account of Russell’s encounter with the paradox:

  • I. Grattan-Guinness, How Russell Discovered his Paradox , Hist. Math. 5 no.2 (1978) pp.127-137.

The first published account is presumably in the appendix of

  • G. Frege, Grundgesetze der Arithmetik II , Pohle Jena 1903.

Russell discusses the paradox extensively in chapter X of

  • B. Russell, The Principles of Mathematics , Cambridge UP 1903.

The influence of Poincaré‘s views shows in

  • B. Russell, Les paradoxes de la logique , Revue de métaphysique et de morale 14 no.5 (1906) pp.627-650. (gallica)

See also

  • P. Várdy, Some Remarks on the Relationship between Russell’s Vicious-Circle Principle and Russell’s Paradox , Dialectica 33 (1979) pp.3-19.

Discussion of a paradox similar to Russell’s in type theory with W-types is in

category: paradox

  1. naive material set theory that is!

  2. Zermelo was apparently led to the paradox by considering a purported proof of Ernst Schröder in his Algebra der Logik (1890) that Boole’s concept of a universal class 1 was contradictory. Interestingly, the solution suggested by Schröder is reminiscent of type theory or even nested universes where a universal class 1 recurs at each level.

  3. Frege (1903, p.253).

  4. This solution proposed by J. von Neumann in the 1920s can be viewed as related to ideas of G. Cantor. The latter knew about similar phenomena concerning “the set of all sets” (in fact, Russell hit upon the paradox in a reflection on Cantor’s proof of the inexistence of a largest cardinal number), and had already pointed out in 1885 in a review of Frege’s “Grundlagen der Arithmetik” that not every concept has an extension. Therefore Cantor proposed in letters to Dedekind and Jourdain to differentiate between ‘consistent multiplicities’ (“compossible” multiplicities one could say) where things can coexist or compose to a consistent whole - ‘ensemble’ (fr.) which correspond to sets in the usual sense and, as completed collections, can in turn be elements in other sets, from ‘inconsistent multiplicities’ whose elements cannot consistently completed to a whole and cannot be member of other collections due to this lack of ‘unity’.

Last revised on November 19, 2022 at 12:40:42. See the history of this page for a list of all contributions to it.