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?