PreprintarXiv licencearXiv
Independence of premise for intuitionistic Zermelo-Fraenkel set theory
Abstract
We answer the following question by Frittaion, Nemoto, and Rathjen positively: "Is [independence of premise] an admissible rule of textsfCZF or any other familiar constructive/intuitionistic set theory T?" To be more precise, we show that whenever textsfIZF (or textsfCZF with full separation) derives a statement of the form lnotψ→ ∃ y φ(y) where y does not occur in ψ, then textsfIZF (or textsfCZF with full separation) also derives ∃ y (lnotψ→ φ(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.
Related
- A Proof of Fraenkel's Conjecture
- The Premise Is the Problem: Exchangeability Failure in Self-Monitored Test-Time Adaptation
- Fine Selection for Intuitionistic Modal Logic
- Failure of Higher-Order Truth within Intuitionistic Propositional Logic
- Exponential Gaps Between Intuitionistic Linear Extended Frege Systems
BibTeX
@misc{uftring2026independence,
title = {{Independence of premise for intuitionistic Zermelo-Fraenkel set theory}},
author = {Patrick Uftring},
howpublished = {arXiv},
year = {2026},
month = oct,
doi = {10.48550/arxiv.2610.11753},
eprint = {2610.11753},
archivePrefix = {arXiv},
url = {https://arxiv.org/abs/2610.11753},
}
RIS
TY - UNPB
TI - Independence of premise for intuitionistic Zermelo-Fraenkel set theory
AU - Patrick Uftring
PY - 2026
DA - 2026/10/08
PB - arXiv
DO - 10.48550/arxiv.2610.11753
UR - https://arxiv.org/abs/2610.11753
AB - We answer the following question by Frittaion, Nemoto, and Rathjen positively: "Is [independence of premise] an admissible rule of textsfCZF or any other familiar constructive/intuitionistic set theory T?" To be more precise, we show that whenever textsfIZF (or textsfCZF with full separation) derives a statement of the form lnotψ→ ∃ y φ(y) where y does not occur in ψ, then textsfIZF (or textsfCZF with full separation) also derives ∃ y (lnotψ→ φ(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.
ER -