3
$\begingroup$

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.

Improve this question
$\endgroup$
6
  • $\begingroup$ Can you define (and give references for the definitions) the Mahlo Universe? $\endgroup$
    – J..y B..y
    Sep 12, 2022 at 10:49
  • $\begingroup$ @J..yB..y I'm talking about Anton Setzer's Mahlo Universe. References have been added. $\endgroup$
    – Ember Edison
    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
    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$
    – Ember Edison
    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
    Sep 14, 2022 at 18:27

1 Answer 1

Reset to default
2
$\begingroup$

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.

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

Your Answer

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

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