Machine Space I: Weak exponentials and quantification over compact spaces
Peter F. Faul and Graham Manuell
拓扑学可以解释为可验证性的研究，其中开集对应于半可判定属性。在本文中，我们区分了可验证属性本身和执行验证过程的过程。前者是简单的开集，而我们将后者称为机器。给定一个框架表示 𝒪 X = ⟨ G | R⟩，我们构造了一个机器空间 Σ^Σ^G，其点由对应于 G 中生成器的基本机器的形式组合给出。这配备了一个"评估"映射，使其成为以 Σ 为底、X 为指数的弱指数。当存在时，真正的指数 Σ^X 作为机器空间的收缩出现。我们认为这有助于解释为什么某些空间是指数化的而其他空间不是。然后，我们使用机器空间通过给出 Escardó 算法在有限时间内对紧空间进行全称量化的纯拓扑版本来研究紧性。最后，我们将机器空间的研究与域理论和域嵌入联系起来。
Topology may be interpreted as the study of verifiability, where opens correspond to semi-decidable properties. In this paper we make a distinction between verifiable properties themselves and processes which carry out the verification procedure. The former are simply opens, while we call the latter machines. Given a frame presentation 𝒪 X = ⟨ G | R⟩ we construct a space of machines Σ^Σ^G whose points are given by formal combinations of basic machines corresponding to generators in G. This come...
