一句话：证明仅需一个 Mahlo 宇宙加可及性谓词，即可自底向上解释 CZF 的全部超限阶不可达集，并在 Agda 中形式化。
Rathjen 曾证明，Aczel 的构造集合论 CZF 加上所有超限阶不可达集，可在 Martin-Löf 类型论 MLTT 中解释，但需假设 Setzer 的 Mahlo 宇宙及其上的另一个宇宙。本文取消这一更高宇宙假设，给出自底向上的解释：在 MLTT 中仅保留一个 Mahlo 宇宙并加入可及性谓词，即可解释全部超限阶不可达集。若类型论带 extensional identity types，该可及性谓词可由 W-types 定义。作者用证明助手 Agda 形式化了该解释的主要部分，从而为这一相对一致性结果提供了机器检查。
Rathjen proved that Aczel's constructive set theory $\mathbf{CZF}$ extended with inaccessible sets of all transfinite orders can be interpreted in Martin-Löf type theory $\mathbf{MLTT}$ extended with Setzer's Mahlo universe and another universe above it. In this paper we show that this interpretation can be carried out bottom-up without the universe above the Mahlo universe, provided we add an accessibility predicate instead. If we work in Martin-Löf type theory with extensional identity types the accessibility predicate can be defined in terms of $\mathrm{W}$-types. The main part of our interpretation has been formalised in the proof assistant Agda.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{abs-2402-15074,
title = {Interpretation of Inaccessible Sets in Martin-Löf Type Theory with One Mahlo Universe},
author = {Yuta Takahashi},
journal = {Logical Methods in Computer Science},
volume = {Volume 21, Issue 4},
year = {2025},
doi = {10.46298/lmcs-21(4:16)2025}
}