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.

  • $\begingroup$ Can you define (and give references for the definitions) the Mahlo Universe? $\endgroup$
    – J..y B..y
    Commented Sep 12, 2022 at 10:49
  • $\begingroup$ @J..yB..y I'm talking about Anton Setzer's Mahlo Universe. References have been added. $\endgroup$ Commented Sep 12, 2022 at 11:57
  • 1
    $\begingroup$ 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. $\endgroup$
    – cody
    Commented Sep 12, 2022 at 17:26
  • $\begingroup$ @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. $\endgroup$ Commented Sep 12, 2022 at 22:39
  • $\begingroup$ 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? $\endgroup$
    – cody
    Commented Sep 14, 2022 at 18:27

1 Answer 1


It's awkward to ask yourself questions, but...

Rathjen, M. (2003). Realizing Mahlo set theory in type theory. Archive for Mathematical Logic, 42(1), 89-101.

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.

  • $\begingroup$ Neat! Ideally detailing the construction in a few words here would be really useful for future reference. $\endgroup$
    – cody
    Commented Feb 25, 2023 at 4:28

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.