Comment by blueberry87
2 years ago
What are your other options? A type-based proof system implies dependent types, implies universe levels if you want it to be consistent.
2 years ago
What are your other options? A type-based proof system implies dependent types, implies universe levels if you want it to be consistent.
Why do dependent types require universe levels to be consistent? I mostly see that in the context of the type of all types and similar, which doesn't seem especially necessary to express. A variable that denotes a type could have type 'any' or 'unspecified', as opposed to a type T^1 or similar.
I believe the parent was referring to Girard's paradox [1], but it's been a while and I'm not a specialist in this area.
[1] https://en.wikipedia.org/wiki/System_U#Girard's_paradox
You lose a very large amount of expressive power if you don't. Any formalisation of the reals requires at least 3 levels, if I remember correctly.
They do not really require it but note my other answer in this subthread.
You would have to not use a type-based proof system. I think those are not going to be the "as simple as possible" ones. Consider metamath for example.