分离性、锐元素与域的 Scott 拓扑
逻辑
2023-09-13 v5 计算机科学中的逻辑
摘要
在构造性框架下,我们研究连续定向完备偏序集(dcpos)与 Scott 拓扑。我们的两个主要创新点是内在分离性(intrinsic apartness)概念与锐元素(sharp elements)概念。分离是“不相等”的肯定性表述,类似于“有元素”是“非空”的肯定性表述。作为锐性的示例,我们注意到下实数是锐的当且仅当它是定位的(located)。我们的第一个主要结果是:对于一大类连续 dcpos,Bridges-Vîţă 分离拓扑与 Scott 拓扑重合。尽管我们不能期望在非平凡 dcpos 上存在紧或余传递的分离关系,我们证明了当限制于连续 dcpo 的锐元素时,内在分离性既是紧的也是余传递的。这些元素包括 Smyth 与 Heckmann 所研究的强极大元素。我们发展了强极大元素的理论,突出其与锐性以及 Lawson 拓扑的联系。最后,我们通过考察若干自然的连续 dcpos 实例来说明内在分离性、锐性与强极大性:Cantor 与 Baire 域、部分 Dedekind 实数、下实数,以及 Cantor 空间到提升集的指数中的嵌入。
引用
@article{arxiv.2106.05064,
title = {Apartness, sharp elements, and the Scott topology of domains},
author = {Tom de Jong},
journal= {arXiv preprint arXiv:2106.05064},
year = {2023}
}
备注
v5: Revised (changed title) and published in MSCS