Hacker Newsnew | past | comments | ask | show | jobs | submitlogin

Ironically, large-cardinals and related devices give set theory a rather type-theoretic "flavor". One can definitely explore the very same questions of 'consistency/existence, size or "order" of objects, and raw mathematical explanatory power of theories' with type-theoretic tools, and arguably do it quite more elegantly, because the related formal devices (e.g. "universes") arise more naturally in a type-theoretic context.


Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: