Machine Space I: Weak exponentials and quantification over compact spaces

Abstract

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=⟨G\mid R⟩$ we construct a space of machines $\hat{I}{\pounds }^{\hat{I}{\pounds }^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 $\hat{I}\pounds$ and exponent $X$. When it exists, the true exponential $\hat{I}{\pounds }^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.