4 ms·
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-pos
by lacker 3y 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.
- blueberry87 3y agoWhat are your other options? A type-based proof system implies dependent types, implies universe levels if you want it to be consistent.
- lacker 3y agoYou 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.
- JonChesterfield 3y agoWhy 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.
- deltasepsilon 3y agoI 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 https://en.wikipedia.org/wiki/System_U#Girard's_paradox
- cjfd 3y agoThey do not really require it but note my other answer in this subthread.
- blueberry87 3y agoYou 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.
- cjfd 3y agoWell, 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.