arXiv Science⌕ Search
Home/Archive/arXiv

arXiv · 2610.11753

Independence of premise for intuitionistic Zermelo-Fraenkel set theory

Patrick Uftring
View original source ↗Read source document ↗Export metadata ↓

Abstract

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.

Explore related subjects

math.LO

Keep this discovery

Explore connections, maps & timelines

BibTeXRIS

Patrick Uftring. 2026-10-08. Independence of premise for intuitionistic Zermelo-Fraenkel set theory. https://arxiv.org/abs/2610.11753

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related papers

arXiv2026

Complexity of deep computations via topology of function spaces

We use topological methods to study complexity of deep computations and limit computations. We use topology of function spaces, specifically, the classification of Rosenthal compacta, to identify new complexity classes. We use the language of model theory, specifically, the concept of \emph{independence} from Shelah's classification theory, to translate between topology and computation. We use the theory of Rosenthal compacta to characterize approximablility of deep computations, both deterministically and probabilistically.

math.LO↗
arXiv2026

Quotient codings and the descriptive complexity of algebraic and analytic structures

We study the descriptive complexity of algebraic and analytic properties by presenting structures as quotients of fixed generators. For separable Banach-type structures, admissible kernels form Polish spaces and quotient norms are continuous in the Wijsman topology. For countable algebraic structures, congruence spaces are compact and atomic predicates are clopen. In the unital $C^*$-algebra coding, commutativity, MF-ness, stable finiteness and existence of a tracial state are $Π^0_1$-complete. AF-ness, nuclearity, simplicity, property~(SP), approximate divisibility, fixed real- and stable-rank bounds, and fixed nuclear-dimension and decomposition-rank bounds are $Π^0_2$-complete. Finiteness of each of these four ranks is $Σ^0_3$-complete. Finite dimensionality and existence of a non-zero finite-dimensional representation are $Σ^0_2$-complete. Residual finite dimensionality is $Π^0_3$-complete, already among AF algebras, while quasidiagonality is $Π^0_3$. For countable abelian groups, slenderness is $Π^0_3$-complete even within the torsion-free locus. We also obtain a $Σ^0_3$ upper bound for uniformly open multiplication in Banach algebras. An internal $K_0$ presentation has $F_σ$ membership coordinates and is $Σ^0_3$-measurable. We establish Borel tensor-ideal assignments, continuity for a fixed nuclear tensor factor, and a $G_δ$ bound for absorption of a strongly self-absorbing algebra. Finally, separability of the dual is $Π^1_1$-complete in the full unital $C^*$-quotient coding, already among commutative AF quotients; superatomicity of countable Boolean algebras is also $Π^1_1$-complete.

math.LO↗
arXiv2026

Kaplansky decompositions of Polish modules

Let $R$ be a countable ring. Given an $R$-module $A$, we call a decomposition $A = \bigoplus_{i \in I} N_i$ a Kaplansky decomposition if each $N_i$ is countable. We characterize the uncountable Polish $R$-modules that admit a Kaplansky decomposition: they are exactly the modules of the form $B \oplus M^ω$, where $B$ and $M$ are countable and $M$ is $Σ$-algebraically compact. The countable summand $B$ may moreover be taken to be an elementary submodule satisfying a closure condition, which makes $M^ω$ unique up to isomorphism, and hence an invariant of $A$. We use this to characterize the countable rings admitting a free uncountable Polish $R$-module, generalizing results of Shelah and Solecki. This class of rings has a purely ring-theoretic description: it consists exactly of the countable left perfect and right coherent rings, i.e. the rings identified by Chase's theorem on products of projective modules. We observe that these are also exactly the countable $F$-rings, i.e. those countable rings $R$ for which $R^ω$ is free. Finally, we give a ring-theoretic characterization of the countable rings $R$ for which there exists an uncountable projective Polish $R$-module.

math.LO↗