一句话:在构造性无点拓扑中提出无点连续性原则,用基间关系诱导连续操作,并联系空间性与紧致性。
本文在构造性无点拓扑中研究 Brouwer 连续性原则的严格表述。作者引入无点拓扑间的连续操作:若点间操作由拓扑基间的关系诱导,则称其连续;相应的无点连续性原则断言,对无点拓扑 S、T,任何诱导连续操作的关系都是 S 到 T 的态射。工作以 Minimalist Foundation 为基础,采用 positive topology,区分理想对象与构造性对象,并将选择序列解释为形式 Baire 空间的点。主要结果:当 S 具有双空间性时原则成立;当 S 为形式 Baire 空间或形式单位区间、T 为自然数形式拓扑时,该原则等价于相应空间性。空间性、bar induction 与单位区间紧致性的若干联系由此被重新表述。
In the setting of constructive pointfree topology, we introduce a notion of continuous operation between pointfree topologies and the corresponding principle of pointfree continuity. An operation between points of pointfree topologies is continuous if it is induced by a relation between the bases of the topologies; this gives a rigorous condition for Brouwer's continuity principle to hold. The principle of pointfree continuity for pointfree topologies $\mathcal{S}$ and $\mathcal{T}$ says that any relation which induces a continuous operation between points is a morphism from $\mathcal{S}$ to $\mathcal{T}$. The principle holds under the assumption of bi-spatiality of $\mathcal{S}$. When $\mathcal{S}$ is the formal Baire space or the formal unit interval and $\mathcal{T}$ is the formal topology of natural numbers, the principle is equivalent to spatiality of the formal Baire space and formal unit interval, respectively. Some of the well-known connections between spatiality, bar induction, and compactness of the unit interval are recast in terms of our principle of continuity. We adopt the Minimalist Foundation as our constructive foundation, and positive topology as the notion of pointfree topology. This allows us to distinguish ideal objects from constructive ones, and in particular, to interpret choice sequences as points of the formal Baire space.