Comment by lacker
2 years ago
Once you have an infinite hierarchy of types, including universe levels, can the proof assistant really be "as simple as possible"?
I feel like a simple-as-possible proof assistant would be more like, proving things about programs written in a minimal Lisp dialect, where the proof validator is itself written in that Lisp dialect.
That said, I personally would rather have an extremely usable proof assistant, rather than a simple-as-possible one. In many ways those things point in opposite directions; consider the usability and simplicity of Python vs the lambda calculus.
Well, I tried to have only one universe level but I found that I could not do some rather simple constructions without proof irrelevance. And that generally proof irrelevance seems to make quite a few things quite a bit easier, also requiring fewer axioms. The thing with proof irrelevance is, though, that it more or less forces one to have universe levels. If there is only one universe level then Prop and Set have to share that. In fact, in that kind of simple setup Prop and Set are just the same thing and one can just use two words as a syntactic sugar but not as anything meaningful. However, proof irrelevance then implies that every set only has one element, which is no good. So, then we we have at least two universe levels. But impredicativity is only consistent in the lowest universe level so then one is more or less automatically led to an infinite tower of universes.
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.