发表机构
University of the Bundeswehr Munich（慕尼黑联邦国防大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
针对Frittaion等人提出的直觉主义策梅洛-弗兰克尔集合论中前提独立性是否为可容许规则的问题，通过适配集合论语境的Friedman-Dragalin翻译变体，证明该规则成立。
AI 中文摘要
我们对Frittaion、Nemoto和Rathjen提出的下述问题给出肯定回答：“[前提独立性]是$\textsf{CZF}$或其他常见的构造性/直觉主义集合论$T$的可容许规则吗？”更准确地说，我们证明当$\textsf{IZF}$（或带完全分离公理的$\textsf{CZF}$）导出形如$\lnot\psi \to \exists y\ \varphi(y)$的陈述，且$y$不在$\psi$中出现时，$\textsf{IZF}$（或带完全分离公理的$\textsf{CZF}$）也会导出$\exists y\ (\lnot\psi \to \varphi(y))$。我们的证明方法是著名的Friedman-Dragalin $A$翻译的变体，以遗传方式适配到集合论语境中。
英文摘要
We answer the following question by Frittaion, Nemoto, and Rathjen positively: "Is [independence of premise] an admissible rule of $\textsf{CZF}$ or any other familiar constructive/intuitionistic set theory $T$?" To be more precise, we show that whenever $\textsf{IZF}$ (or $\textsf{CZF}$ with full separation) derives a statement of the form $\lnotψ\to \exists y\ φ(y)$ where $y$ does not occur in $ψ$, then $\textsf{IZF}$ (or $\textsf{CZF}$ with full separation) also derives $\exists y\ (\lnotψ\to φ(y))$. Our proof method is a variant of the famous Friedman-Dragalin $A$-translation adapted to the context of set theory in a hereditary manner.
