<p>It's awkward to ask yourself questions, but...</p>
<p>Rathjen, M. (2003). Realizing Mahlo set theory in type theory. Archive for Mathematical Logic, 42(1), 89-101.</p>
<p>The chapter 5, &quot;Realizing set theory in Mahlo type theory&quot; is the required construction for <code>CZF + Mahlo Cardinal</code>. The previous section shows why this construction does satisfy the definition of Mahlo Cardinal.</p>

CC BY-SA 4.0
2023-02-25T04:28:27.840Z
Neat! Ideally detailing the construction in a few words here would be really useful for future reference.
cody
CC BY-SA 4.0
2023-02-22T17:00:26.307Z
2023-02-22T17:00:26.307Z
Ember Edison
<p>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.</p>
<p>More explicitly, I would like to know what condition is missing between <code>CIC + a Mahlo Universe</code> and <code>IZF + a Mahlo Cardinal</code>?</p>
<p>[1] Setzer, A. (2000). Extending Martin-Löf type theory by one Mahlo-universe. Archive for Mathematical Logic, 39(3), 155-181.</p>
<p>[2] Kahle, R., &amp; Setzer, A. (2010). An extended predicative definition of the Mahlo universe. Ways of Proof Theory. De Gruyter. doi, 10(9783110324907), 315.</p>

CC BY-SA 4.0
2022-09-12T10:49:02.333Z
Can you define (and give references for the definitions) the Mahlo Universe?
J.y B.y
CC BY-SA 4.0
2022-09-12T11:57:58.377Z
@J..yB..y I'm talking about Anton Setzer's Mahlo Universe. References have been added.
Ember Edison
CC BY-SA 4.0
2022-09-12T17:26:38.777Z
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
CC BY-SA 4.0
2022-09-12T22:39:10.193Z
@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.
Ember Edison
CC BY-SA 4.0
2022-09-14T18:27:31.260Z
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
CC BY-SA 4.0
2022-09-15T04:12:28.520Z
@cody just consistency strength about `CIC + a Mahlo Universe`.
Ember Edison
<lo.logic><type-theory><proof-theory>
How far is the distance between Mahlo Universe and Mahlo Cardinal?
Ember Edison
# How far is the distance between Mahlo Universe and Mahlo Cardinal?

(Asked by: username_0 on 2022-09-11)

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.

**Tags:** lo.logic, type-theory, proof-theory
> **Comments:**
> **username_1**: Can you define (and give references for the definitions) the Mahlo Universe?  
> **username_0**: @J..yB..y I'm talking about Anton Setzer's Mahlo Universe. References have been added.  
> **username_2**: 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.  
> **username_0**: @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.  
> **username_2**: 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?  
> **username_0**: @cody just consistency strength about `CIC + a Mahlo Universe`.  

---

## 1 answers

### Answer by username_0 on 2023-02-22. Score: 3 | Accepted answer

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.

> **Comments:**
> **username_2**: Neat! Ideally detailing the construction in a few words here would be really useful for future reference.  

---

