On the Existence and Disjunction Properties in Structural Set Theory

2023/11/23 by Saving, Mark
#03E70 (Secondary) #03F50 (Primary) 03G30 #Category Theory (math.CT) #FOS: Mathematics #Logic (math.LO)

paper · doi:10.48550/arxiv.2312.03717

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.

Related

• Constructivist and Structuralist Foundations: Bishop's and Lawvere's Theories of Sets
• Logics and Admissible Rules of Constructive Set Theories
• The independence of premise rule in intuitionistic set theories
• A construction of set theory
• Choice and independence of premise rules in intuitionistic set theory