2
$\begingroup$

Is the Russell paradox formalizable in type theories?

The paradox: There is no set of all sets that don't contain themselves. For if there is such a set, it must either contain itself or not contain itself. But both possibilities lead to the opposite. That's a contradiction.

In type theory, every object has a particular type, and operations and relations are restricted to objects having the appropriate type. This prevents the formation of "junk theorems". It seems to me that the formation of the "set of all sets that don't contain themselves" is not allowed in type theory. Is this correct? I would say 'yes', because there shouldn't be a general type "set", but for each type X another type "sets of objects from X". Hence Russell's paradox is ill-formed in type theory. Am I right?

Improve this question
$\endgroup$
  • 2
    $\begingroup$ Type Theory was originally introduced by Russell in 1903 exactly in order to cope with the contradictions he found. $\endgroup$ – Mauro ALLEGRANZA Oct 10 '16 at 13:09
  • 1
    $\begingroup$ Obviously, this is not what I mean with type theory. $\endgroup$ – user377006 Oct 10 '16 at 13:13
  • 1
    $\begingroup$ I mean something like the type theory of Martin-Löf or Homotopy type theory. $\endgroup$ – user377006 Oct 10 '16 at 13:14
2
$\begingroup$

While a naïve encoding of Russel's paradox will fail, there is a related phenomenon called Girard's Paradox which does exist, although not in a sufficiently-well stratified version of type theory.

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.