News for hackers. Stuff that matters.

A comment on What do we mean by "the foundations of mathematics"?. Parent comment

Re:What do we mean by "the foundations of mathematics"? by JonChesterfield on Wednesday November 01, 2023 @08:42PM (#38107428)
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.
[ Parent | on HN ]
Re:What do we mean by "the foundations of mathematics"? by deltasepsilon on Wednesday November 01, 2023 @09:41PM (#38107907)
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

[ Parent | on HN ]
Re:What do we mean by "the foundations of mathematics"? by cjfd on Thursday November 02, 2023 @05:05AM (#38110758)
They do not really require it but note my other answer in this subthread.
[ Parent | on HN ]
Re:What do we mean by "the foundations of mathematics"? by blueberry87 on Thursday November 02, 2023 @11:57PM (#38124321)
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.
[ Parent | on HN ]