Interpretation of Inaccessible Sets in Martin-L\"of Type Theory with One Mahlo Universe
<|reference_start|>Interpretation of Inaccessible Sets in Martin-L\"of Type Theory with One Mahlo Universe: 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.<|reference_end|>
@article{takahashi2024interpretation,
    title={Interpretation of Inaccessible Sets in Martin-L\"{o}f Type Theory with
  One Mahlo Universe},
    author={Yuta Takahashi},
    journal={arXiv preprint arXiv:2402.15074},
    year={2024},
    archivePrefix={arXiv},
    eprint={2402.15074},
    primaryClass={cs.LO math.LO}
}