This is incorrect. The set paradox it’s analogous to is the inability to make the set of all ordinals. Russel’s paradox is the inability to make the set of all sets.
Perhaps I overstated how related the two were. I was pulling mostly from the Lean documentation on Universes [0]
> The formal argument for this is known as Girard's Paradox. It is related to a better-known paradox known as Russell's Paradox, which was used to show that early versions of set theory were inconsistent. In these set theories, a set can be defined by a property.
srcreigh|28 days ago
kibwen|28 days ago
enricozb|27 days ago
> The formal argument for this is known as Girard's Paradox. It is related to a better-known paradox known as Russell's Paradox, which was used to show that early versions of set theory were inconsistent. In these set theories, a set can be defined by a property.
[0]: https://lean-lang.org/functional_programming_in_lean/Functor...