|logic||category theory||type theory|
|true||terminal object/(-2)-truncated object||h-level 0-type/unit type|
|false||initial object||empty type|
|proposition||(-1)-truncated object||h-level 1-type/h-prop|
|cut elimination for implication||counit for hom-tensor adjunction||beta reduction|
|introduction rule for implication||unit for hom-tensor adjunction||eta conversion|
|disjunction||coproduct ((-1)-truncation of)||sum type (bracket type of)|
|implication||internal hom||function type|
|negation||internal hom into initial object||function type into empty type|
|universal quantification||dependent product||dependent product type|
|existential quantification||dependent sum ((-1)-truncation of)||dependent sum type (bracket type of)|
|equivalence||path space object||identity type|
|equivalence class||quotient||quotient type|
|induction||colimit||inductive type, W-type, M-type|
|higher induction||higher colimit||higher inductive type|
|completely presented set||discrete object/0-truncated object||h-level 2-type/preset/h-set|
|set||internal 0-groupoid||Bishop set/setoid|
|universe||object classifier||type of types|
|modality||closure operator monad||modal type theory, monad (in computer science)|
|linear logic||(symmetric, closed) monoidal category||linear type theory/quantum computation|
|proof net||string diagram||quantum circuit|
|(absence of) contraction rule||(absence of) diagonal||no-cloning theorem|
One then asks: is ? If so, then by definition, whereas if not, then by definition. Thus we have both and , a contradiction.
Russell’s paradox is closely related to the liar paradox (“this sentence is false”), to Gödel’s incompleteness theorem, and to the halting problem — all use diagonalization? to produce an object which talks about itself in a contradictory or close-to-contradictory way.
There are a number of possible resolutions of Russell’s paradox.
The “classical” solution, adopted in ZFC and thus by most mainstream mathematicians, is to restrict the axiom of comprehension so as to disallow the formation of the set : 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.
Essentially the same resolution is used in class theories such as NBG. Here we may write down the definition of , but from we may conclude only if we already know that is a set; the in the definition must be a set. So we have no contradiction, but only a proof that 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 is not stratifiable, the set cannot be formed. A similar (but more complicated) resolution was developed by Russell himself in his theory of ramified type?s.
In most structural set theories, there is no need to artificially restrict the set-formation rules: if sets cannot be elements of other sets, then the “definition” of 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 or ), without using excluded middle we can obtain that is both not in and not not in , 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 implies and vice versa, but we can never get both and at the same time to produce a paradox.
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 exists, being both a member of itself and not a member of itself.