تقرير
Interpretation of Inaccessible Sets in Martin-L\'{o}f Type Theory with One Mahlo Universe
العنوان: | Interpretation of Inaccessible Sets in Martin-L\'{o}f Type Theory with One Mahlo Universe |
---|---|
المؤلفون: | Takahashi, Yuta |
سنة النشر: | 2024 |
المجموعة: | Computer Science Mathematics |
مصطلحات موضوعية: | Computer Science - Logic in Computer Science, Mathematics - Logic, F.4.1 |
الوصف: | Martin-L\"{o}f type theory $\mathbf{MLTT}$ was extended by Setzer with the so-called Mahlo universe types. This extension is called $\mathbf{MLM}$ and was introduced to develop a variant of $\mathbf{MLTT}$ equipped with an analogue of a large cardinal. Another instance of constructive systems extended with an analogue of a large set was formulated in the context of Aczel's constructive set theory: $\mathbf{CZF}$. Rathjen, Griffor and Palmgren extended $\mathbf{CZF}$ with inaccessible sets of all transfinite orders. It is unknown whether this extension of $\mathbf{CZF}$ is directly interpretable by Mahlo universes. In particular, how to construct the transfinite hierarchy of inaccessible sets using the reflection property of the Mahlo universe in $\mathbf{MLM}$ is not well understood. We extend $\mathbf{MLM}$ further by adding the accessibility predicate to it and show that the above extension of $\mathbf{CZF}$ is directly interpretable in $\mathbf{MLM}$ using the accessibility predicate. |
نوع الوثيقة: | Working Paper |
URL الوصول: | http://arxiv.org/abs/2402.15074 |
رقم الأكسشن: | edsarx.2402.15074 |
قاعدة البيانات: | arXiv |
الوصف غير متاح. |