Independence of premise for intuitionistic Zermelo-Fraenkel set theory
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…
Comments and reviews
No comments yet.
API
curl /api/v1/records/arxiv/2610.11753
curl -X POST /api/v1/records/arxiv/2610.11753/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/arxiv/2610.11753/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'