{"id":"arxiv/2610.11753","url":"https://arxiv.org/abs/2610.11753","tags":["math.LO"],"score":0,"title":"Independence of premise for intuitionistic Zermelo-Fraenkel set theory","domain":"math.LO","source":"arxiv","authors":["Patrick Uftring"],"reviews":0,"subject":"math.LO","summary":"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\\ \\varphi(y)$ where $y$ does not occur in $ψ$, then $\\textsf{IZF}$ (or $\\textsf{CZF}$ with full separation) also derives $\\exists y\\ (\\lnotψ\\to \\varphi(y))$. Our proof method is a variant of the famous Friedman-Dragalin $A$-translation…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"discussed":0,"published":"2026-10-08","reactions":{}}