Is there an "open sets style" formulation of Topology that makes the connection to semidecidability precise?

199 Views Asked by At

Once pointed out, the connection between Topology - the definition of what open sets are - and semidecidability (as used in Computer Science) is clear. $\emptyset$ and $\mathbb{N}$ are semidecidable, and any finite intersection of semidecidable sets is also semidecidable - run the semidecision process for each set in sequence. But it is not the case that an arbitrary union of semidecidable sets is also a semidecidable set. We come close; "recursively enumerable unions" ($RE$) of semidecidable sets are also a semidecidable set.

So my goal with this question is to obtain a generalized definition of open sets, one that relaxes the "arbitrary" closure condition in the regular definition to something that accepts semidecidability. In principle, we could just replace that with $RE$ as suggested before, but that would give us a definition that isn't really applicable to general topology.

The reference text for this seems to be Martin Escardó's work, specifically Synthetic topology of data types and classical spaces. But as a beginner in Topology myself, i've found the paper difficult to understand. His approach - using continuous functions as the primary component, upon which the rest of definitions are laid out - makes it hard to appreciate the connection. Which is why i'm asking specifically for an "open sets style" definition.