4 ms·
> To some extend this can be encoded in set theory, but only with ridiculously large (Mahlo) cardinals. I don't see why the size of Mahlo cardinals is ridiculo
by lgandersen 10y ago
> To some extend this can be encoded in set theory, but only with ridiculously large (Mahlo) cardinals.
I don't see why the size of Mahlo cardinals is ridiculous. Considering all the strongly inaccessible cardinals that have been discovered, Mahlo cardinals is rather weak. Also, the definition of a Grothendieck universe strongly resembles the definition of a strongly inaccessible cardinal, imho. That they are equivalent are (relatively) straightforward.
Harvey Friedmans work on provable equivalences between large cardinals way larger than Mahlo cardinals and theorems about objects in the domain of the rationals further substantiates this. Very fascinating.
- fmap 10y agoWhat do you mean exactly? Grothendieck universes correspond to the some inaccessible cardinals, but the axiom that every set is contained in a Grothendieck universe (which is stronger than just saying that there are omega-many inaccessible cardinals of increasing size) is itself weaker than the existence of a single Mahlo cardinal... And (afaik) you need a Mahlo cardinal for every type theoretic universe that is closed under induction-recursion. My point is that induction-recursion is a very intuitive notion from a computational perspective, yet its encoding in set theory is anything but intuitive...