On the Existence and Disjunction Properties in Structural Set Theory

Fuente: arXiv
Salvato in:
Dettagli Bibliografici
Autore principale: Saving, Mark
Natura: Preprint
Pubblicazione: 2023
Soggetti:
Accesso online:
Tags: Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
_version_ 1866909675123900416
author Saving, Mark
author_facet Saving, Mark
contents 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.
format Preprint
id arxiv_https___arxiv_org_abs_2312_03717
institution arXiv
publishDate 2023
record_format arxiv
spellingShingle On the Existence and Disjunction Properties in Structural Set Theory
Saving, Mark
Logic
Category Theory
03F50 (Primary) 03G30, 03E70 (Secondary)
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.
title On the Existence and Disjunction Properties in Structural Set Theory
topic Logic
Category Theory
03F50 (Primary) 03G30, 03E70 (Secondary)
url https://arxiv.org/abs/2312.03717