Apartness, compactness and nearness (Q949606)

The paper investigates the possibility of introducing a notion of compactness for apartness spaces. The latter have been proposed as a suitable framework for doing topology constructively, and correspond to the classical theory of proximity spaces. The authors set out to find a definition of compactness that, for uniform spaces, is equivalent to totally boundedness together with completeness, and that is classically equivalent to the usual Heine-Borel definition. The chosen approach is to reconstruct a base of entourages from a given apartness relation. It is shown that this approach almost succeeds and that many interesting properties hold. Unfortunately it is not shown that a uniform space that is compact with respect to the reconstructed uniformity is totally bounded or complete. The paper is of relevance to anybody interested in constructive topology, compactness, and foundations of mathematics.