Apartness spaces as a framework for constructive topology (Q1861535)

It is known that some proofs from classical mathematics are constructive, and some are not. One of the main objectives of constructive mathematics is to find out which results of classical mathematics have a constructive meaning. To be able to do that, we must first come up with a reasonable constructive version of the corresponding mathematical theory. For metric spaces and for the corresponding topology, such a theory has been successfully developed many decades ago; however, describing a reasonable constructive version of general (not necessarily metric) topology has always been a challenge, so that even E. Bishop in some of his papers claimed that constructive non-metric topology is simply impossible. The authors show that a reasonable constructive version of non-metric topology can be constructed if instead of trying to constructivize the traditional definitions of topology (as many researchers tried in the past), one bases the formalization on a new (non-traditional) notion of apartness. Apartness between points \(x\neq y\) is a strong (constructive) version of non-equality \(\neg(x=y)\): e.g., for real numbers, \(\neg (x=y)\) means that \(\neg\neg\exists r>0\,(| x-y| \geq r)\) (where \(r\) goes over all rational numbers), while apartness means that \(\exists r>0\,(| x-y| \geq r)\). To describe a topological space, we need the notion of apartness \(\text{ apart}(x,A)\) between a point \(x\) and a set \(A\). For example, for metric spaces, one can define such apartness as \(\exists r>0\,\forall y\in A\, (\rho(x,y)\geq r)\). The authors show that if one introduces reasonable axioms for apartness, one gets a reasonable constructive topology. For example, continuity can be defined as \(\text{ apart}(fx,fA)\supset \text{ apart}(x,A)\) for all points \(x\) and for all sets \(A\). Quantifying over all sets does not sound like a very constructive definition; to make this definition more constructive, the authors propose a more constructive version of this definition in which they fix a constructive family of sets and only consider sets \(A\) from this family.