On the Existence and Disjunction Properties in Structural Set Theory
Logic
2025-07-08 v2 Category Theory
Abstract
We formulate a definition of the existence property that works with "structural" set theories, in the mode of ETCS (the elementary theory of the category of sets). We show that a range of structural set theories, when formulated using constructive logic, satisfy the disjunction, numerical existence, and existence properties; in particular, intuitionist ETCS, formulated with separation and Shulman's replacement of contexts axiom, satisfies these properties. As a consequence of this, we show that, working constructively, replacement of contexts is strictly weaker than collection.
Keywords
Cite
@article{arxiv.2312.03717,
title = {On the Existence and Disjunction Properties in Structural Set Theory},
author = {Mark Saving},
journal= {arXiv preprint arXiv:2312.03717},
year = {2025}
}