تقرير
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 |
| الوصف غير متاح. |