作为几乎离散locale的重叠代数
Overlap Algebras as Almost Discrete Locales
AI总结：
本文探讨在构造性逻辑下“几乎离散locale”的概念，指出Sambin的重叠代数因包含离散locale类、作为最小强稠密子locale且在排中律下与Boolean locale重合，是构造性视角下几乎离散locale的恰当表征。
摘要：
Boolean locale是“几乎离散的”，意指空间型Boolean locale就是离散locale（即对应于离散空间的开放子集frame，也就是某集合的幂集）。然而，这一基本事实无法在直觉主义逻辑上构造性地证明，因为它需要完整的排中律（LEM）。事实上，构造性地看，除平凡locale外，离散locale绝非Boolean。那么，构造性地，什么是几乎离散的locale？我们的主张是，Sambin的重叠代数具备足够良好的特征，足以被称为几乎离散locale。即：它们包含离散locale类，作为（overt locale的）最小强稠密子locale出现，因此若LEM成立，它们便与Boolean locale重合。
英文摘要：
Boolean locales are "almost discrete", in the sense that a spatial Boolean locale is just a discrete locale (that is, it corresponds to the frame of open subsets of a discrete space, namely the powerset of a set). This basic fact, however, cannot be proven constructively, that is, over intuitionistic logic, as it requires the full law of excluded middle (LEM). In fact, discrete locales are never Boolean constructively, except for the trivial locale. So, what is an almost discrete locale constructively? Our claim is that Sambin's overlap algebras have good enough features to deserve to be called that. Namely, they include the class of discrete locales, they arise as smallest strongly dense sublocales (of overt locales), and hence they coincide with the Boolean locales if LEM holds.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
