# How far is the distance between Mahlo Universe and Mahlo Cardinal?

There seems to be some literature stating that Mahlo Universe[1][2] is the counterpart of Mahlo Cardinal in type theory, but I don't fully understand this point of knowledge.

More explicitly, I would like to know what condition is missing between CIC + a Mahlo Universe and IZF + a Mahlo Cardinal?

[1] Setzer, A. (2000). Extending Martin-Löf type theory by one Mahlo-universe. Archive for Mathematical Logic, 39(3), 155-181.

[2] Kahle, R., & Setzer, A. (2010). An extended predicative definition of the Mahlo universe. Ways of Proof Theory. De Gruyter. doi, 10(9783110324907), 315.

• Can you define (and give references for the definitions) the Mahlo Universe? Sep 12, 2022 at 10:49
• @J..yB..y I'm talking about Anton Setzer's Mahlo Universe. References have been added. Sep 12, 2022 at 11:57
• Already a bit painful is the fact that the CIC <-> IZF relationship is not entirely trivial. I think things get easier when considering CIC + EM vs ZF.
– cody
Sep 12, 2022 at 17:26
• @cody I would welcome this if it would alleviate your distress. The key to this question is the combination of the universe and the cardinal pair, not CIC and IZF. Sep 12, 2022 at 22:39
• I'm not entirely sure that the Mahlo-ness washes out the difference in foundation (maybe it does). What result would you like/expect to prove?
– cody
Sep 14, 2022 at 18:27

The chapter 5, "Realizing set theory in Mahlo type theory" is the required construction for CZF + Mahlo Cardinal. The previous section shows why this construction does satisfy the definition of Mahlo Cardinal.