What’s the logic behind not making this concept symmetric, though?
It’s nice if the opens of X can be internalized as the continuous functions X→TV for some space of truth values TV with a distinguished point ⊤ such that x∈O⇔O(x)=⊤. For this, it is necessary (and sufficient) for the open sets of TV to be generated by {⊤}. I could instead ask for a distinguished point ⊥ such that x∉O⇔O(x)=⊥, and for this it is necessary and sufficient for the open sets of TV to be generated by TV∖{⊥}. Put them together, and you get that TV must be the Sierpiński space: a “true” result (⊤∈TV) is finitely observable ({⊤} is open), but a “false” result is not ({⊥} is not open).
perhaps there’s some kind of intuitionist/constructivist justification
Yes, constructively we do not know a proposition until we find a proof. If we find a proof, it is definitely true. If we do not find a proof, maybe it is false, or maybe we have not searched hard enough—we don’t know.
Also related is that the Sierpiński space is the smallest model of intuitionistic propositional logic (with its topological semantics) that rejects LEM, and any classical tautology rejected by Sierpiński space is intuitionistically equivalent to LEM. There’s a sense in which the difference between classical logic and intuitionistic logic is precisely the assumption that all open sets of possibility-space are clopen (which, if we further assume T0, leads to an ontology where possibility-space is necessarily discrete). (Of course it’s not literally a theorem of classical logic that all open sets are clopen; this is a metatheoretic claim about semantic models, not about objects internal to either logic.) See A Semantic Hierarchy for Intuitionistic Logic.
It’s nice if the opens of X can be internalized as the continuous functions X→TV for some space of truth values TV with a distinguished point ⊤ such that x∈O⇔O(x)=⊤. For this, it is necessary (and sufficient) for the open sets of TV to be generated by {⊤}. I could instead ask for a distinguished point ⊥ such that x∉O⇔O(x)=⊥, and for this it is necessary and sufficient for the open sets of TV to be generated by TV∖{⊥}. Put them together, and you get that TV must be the Sierpiński space: a “true” result (⊤∈TV) is finitely observable ({⊤} is open), but a “false” result is not ({⊥} is not open).
Yes, constructively we do not know a proposition until we find a proof. If we find a proof, it is definitely true. If we do not find a proof, maybe it is false, or maybe we have not searched hard enough—we don’t know.
Also related is that the Sierpiński space is the smallest model of intuitionistic propositional logic (with its topological semantics) that rejects LEM, and any classical tautology rejected by Sierpiński space is intuitionistically equivalent to LEM. There’s a sense in which the difference between classical logic and intuitionistic logic is precisely the assumption that all open sets of possibility-space are clopen (which, if we further assume T0, leads to an ontology where possibility-space is necessarily discrete). (Of course it’s not literally a theorem of classical logic that all open sets are clopen; this is a metatheoretic claim about semantic models, not about objects internal to either logic.) See A Semantic Hierarchy for Intuitionistic Logic.