The Constant Domain Axiom in Toposes
arXiv:2607.13327
summary
The paper shows that the constant domain axiom for intuitionistic logic can be modeled in any topos using objects that are covert and Hausdorff as discrete locales, and proves that these objects form a Boolean pretopos.
Abstract
Constant domain intuitionistic logic admits a complete semantics in presheaf toposes, by interpreting sorts as constant presheaves and predicates as arbitrary sub-presheaves. The goal of this note is to point out how this fits in topos theory, replacing constant presheaves with objects that are covert and Hausdorff when considered as discrete locales. We call these objects "CD" and we show that they form a Boolean pretopos in any topos.
3 pages
Topics & keywords
#constant domain logic#intuitionistic logic#topos theory#presheaf toposes#discrete locales#boolean pretoposconstant domain axiompresheaf toposcovert objectsHausdorff localesBoolean pretopos