paperbot · PL 论文追踪

全部论文 待读 收藏

P2 $\sigma$-locales in Formal Topology

形式拓扑中的 σ-locale
LMCS vol.Volume 18, Issue 12022匹配度 1/10 · 该论文属于构造性形式拓扑/σ-locale 的理论研究,关注无点拓扑与构造性数学基础,未涉及程序分析、LLM/Agent、浮点程序分析或贝叶斯程序分析等用户核心方向。引用 0 inbox
Francesco Ciraulo
crossref: 2026-09-10

AI 速览

一句话:证明 σ-frame/σ-locale 可归入形式拓扑,并构造性地刻画最小强稠密 σ-子locale。

本文研究 σ-frame 与 σ-locale 在构造性、无点拓扑中的位置。σ-frame 是具有可数并和有限交、且二元交对可数并分配的偏序集。作者证明 σ-frame(更准确地说是 σ-locale)可视为形式拓扑的一个分支,即直觉主义与直谓式的无点拓扑。具体地,每个 σ-frame L 都可实现为某类特殊形式拓扑中 Lindelöf 元素(其每个覆盖都有可数子覆盖)构成的格,而该形式拓扑又是 L 上自由 frame 的一个表示。随后,文章给出给定 σ-locale 的最小(强)稠密 σ-子locale 的构造性刻画,从而得到 Boolean locale 的“σ-版本”。该发展依赖于可数选择公理。

问题
如何将 σ-frame/σ-locale 纳入直觉主义、直谓式的形式拓扑,并在构造性框架下刻画其稠密子locale。
方法
将每个 σ-frame L 表示为某类形式拓扑的 Lindelöf 元素格,该形式拓扑作为 L 上自由 frame 的表示,并据此构造最小(强)稠密 σ-子locale。
评估
给出构造性特征与 Boolean locale 的 σ-版本;理论结果依赖可数选择公理,未涉及实验评估。
原文摘要(Abstract)

A $\sigma$-frame is a poset with countable joins and finite meets in which binary meets distribute over countable joins. The aim of this paper is to show that $\sigma$-frames, actually $\sigma$-locales, can be seen as a branch of Formal Topology, that is, intuitionistic and predicative point-free topology. Every $\sigma$-frame $L$ is the lattice of Lindel\"of elements (those for which each of their covers admits a countable subcover) of a formal topology of a specific kind which, in its turn, is a presentation of the free frame over $L$. We then give a constructive characterization of the smallest (strongly) dense $\sigma$-sublocale of a given $\sigma$-locale, thus providing a "$\sigma$-version" of a Boolean locale. Our development depends on the axiom of countable choice.

链接与引用

DOI 原文 · PDF(开放获取) ·

BibTeX
@article{paperbot1748,
  title = {$\sigma$-locales in Formal Topology},
  author = {Francesco Ciraulo},
  journal = {Logical Methods in Computer Science},
  volume = {Volume 18, Issue 1},
  year = {2022},
  doi = {10.46298/lmcs-18(1:7)2022}
}