Topology and semidecidability
A popular answer on math.stackexchange explains that the concept of open set axiomatizes the notion of semidecidable property, where the latter is in turn — via a link to Wikipedia — explained informally as "a well-defined method whose result ... arrives as positive, [if the property holds of a given datum]". Semi, because if the property does not hold, we have no guarantee of finding out.
This point of view, which has long been emphasized by the likes of Abramsky, Vickers, and Smyth, is very appealing to me as a computer scientist. But when trying to explain this recently, I realized it contains a subtlety (which upon closer inspection of math.stackexchange, has also been raised by the commenters).
Recall why open sets are said to axiomatize semidecidable properties: this is reflected in the basic asymmetry between unions and intersections.
-
Finite intersections are again semidecidable, because $x \in X_1 \cap ... \cap X_n$ if and only if $x \in X_i$ for all $i$. Thus we can simply run the semidecision procedure for $X_1$, then if it terminates, run that for $X_2$ and so on: this is again a semidecision procedure for the intersection. For an infinite intersection, we'd have to run an infinite number of semidecision procedures, which is not a semidecision procedure.
-
Arbitrary unions of semidecidable properties are semidecidable, because $\cup_{i \in I} X_i$ if and only if $x \in X_i$ for some $i$.
Of course,
But here the subtlety bites: in the infinite case, the implicit semidecision procedure is run an infinite number of semidecision procedures in parallel. Is this really a "well-defined method"? As long as "semidecidable" remains defined by intuition, I suppose this is subject to debate.
The first thing to consider is that, in case $I$ is countable, then given a bijection with $\mathbb{N}$ we can ``zig-zag'' the semidecision procedures by interleaving them à la enumerating the positive rationals.
The class of topological spaces for which arbitrary unions reduce to countable unions are called hereditarily Lindelöf, and I'm pretty sure this class contains all the topological spaces I might ever care about.
Anyway, as Abramsky points out, we can only rescue "open = semidecidable", with the precise sense of semidecidability given by computability theory, if we take our mathematical universe to be an effective one, such as the effective topos, in which everything in sight is computable.
Abramsky coins semi-observable as the neutral term: "we say that a property is observable if we can tell whether or not it holds of a process on the basis of only a finite amount of information about that process". With this informal definition, indeed, arbitrary unions are semi-observable.
Martín Escardó in his monograph on synthetic topology addresses the discrepancy in several ways.