[Drup]

A self-contained type-system is called "a logic". There are plenty of logics, many of which are not related to set algebra. Furthermore, many type systems are not directly related to set algebra (for instance, Rust's ownership). There are also more profound reasons (what is the type of a type, cf the notion of impredicativity and questions about decidability), but those are usually of little practical consequences for "mainstream" languages.

With only a logic, you can't show properties about the language. In particular, we like to show that programs that are well typed avoid some errors (like segfaults), or that if an expression ( `log2(length(s))`) has a type (`int`), when you evaluate it to a value, the value (`4`) has the same type. If you want to consider such (nice!) properties, you need to consider the type system and the language together.