Machine Space I: Weak exponentials and quantification over compact spaces
This work addresses foundational issues in topology and domain theory, offering insights into exponentiability and compactness, but it is incremental as it builds on existing concepts like weak exponentials and Escardó's algorithm.
The paper tackles the problem of distinguishing between verifiable properties and verification processes in topology by constructing a 'machine space' as a weak exponential, which helps explain why some spaces are exponentiable and others are not, and applies this to study compactness with a topological version of an algorithm for universal quantification over compact spaces in finite time.
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 \emph{machines}. Given a frame presentation $\mathcal{O} X = \langle G \mid R\rangle$ we construct a space of machines $Σ^{Σ^G}$ whose points are given by formal combinations of basic machines corresponding to generators in $G$. This comes equipped with an `evaluation' map making it a weak exponential with base $Σ$ and exponent $X$. When it exists, the true exponential $Σ^X$ occurs as a retract of machine space. We argue this helps explain why some spaces are exponentiable and others not. We then use machine space to study compactness by giving a purely topological version of Escardó's algorithm for universal quantification over compact spaces in finite time. Finally, we relate our study of machine space to domain theory and domain embeddings.