发表机构
Chalmers University of Technology; University of Gothenburg（查尔姆斯理工大学; 哥德堡大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本文证明在仅含排中律且无选择公理的 Lean 类型论中，通过可达性谓词的大消除构造良基树，可证明 ZF 的一致性，无需选择算子。
AI 中文摘要
集合的树形解释在带一个非直谓命题宇宙的依赖类型论中验证了策梅洛集合论，并且如果类型论具有选择算子或描述算子（将函数关系转化为函数），则它还验证了替换公理。人们自然预期，在没有这种算子的情况下，类型论的强度会远低于 $\mathrm{ZF}$。我们证明并非如此。在 Lean 的类型论中，使用两个直谓宇宙，仅以排中律为假设且无任何公理（无选择公理、无命题外延性、无商类型），我们证明了 $\mathrm{ZF}$ 的一致性，该一致性是针对一阶证明系统直接陈述的。该证明已被形式化。其机制是对一个与集合类型同大的类型上的可达性谓词进行大消除：一种对可达性的递归，其递归调用由命题保护，且后续调用的索引由先前调用的值决定，从而将任何由命题通过某种形状的良基树指定的序数计算为一个项。我们给出一个规则，为每个序数生成这样的树，除非某个 $V_\rho$ 已经是 $\mathrm{ZF}$ 的模型；该规则不选择共尾映射进入极限序数，而是同时取所有可定义者。在第一种情况下，集合的树形解释对任意命题关系满足替换公理。无论哪种情况，$\mathrm{ZF}$ 都有模型。最后，排中律的双重否定就足够了，而其余部分恰好是：在集合的稳定解读下，属于关系并非不良基；这进而蕴含马尔可夫原则的双重否定。
英文摘要
The sets-as-trees interpretation of set theory in a dependent type theory with an impredicative universe of propositions validates Zermelo set theory, and it validates Replacement if the type theory has a choice or description operator, which turns a functional relation into a function. It has been natural to expect that without such an operator the strength of the type theory drops well below that of $\mathrm{ZF}$. We show that it does not. In the type theory of Lean with two predicative universes, from excluded middle as the only assumption and with no axiom (no choice, no propositional extensionality, no quotients), we prove the consistency of $\mathrm{ZF}$, stated outright for a first-order proof system. The proof is formalized. The mechanism is the large elimination of the accessibility predicate over a type as large as the type of sets: a recursion on accessibility whose recursive calls are guarded by propositions, and whose later calls are indexed by the value of an earlier call, computes as a term any ordinal that is specified by a proposition through a well-founded tree of a certain shape. We give a rule that produces such a tree for every ordinal, unless some $V_ρ$ is already a model of $\mathrm{ZF}$; the rule does not choose a cofinal map into a limit ordinal but takes all definable ones at once. In the first case the sets-as-trees satisfy Replacement for arbitrary propositional relations. Either way $\mathrm{ZF}$ has a model. Finally, the double negation of excluded middle suffices, and what remains of it is exactly that membership is not not well-founded in the stable reading of sets; this in turn implies the double negation of Markov's principle.
Comments13 pages. Lean 4 formalization at https://github.com/digama0/ConZF
