(I agree with your last paragraph—this thread is interesting but unfortunately beside the point since probabilistic theories are obviously trying to “say more” than just their merely nondeterministic shadows.)
Negations of finitely observable predicates are typically not finitely observable. [0,0.5) is finitely observable as a subset of [0,1], because if the true value is in [0,0.5) then there necessarily exists a finite precision with which we can know that. But its negation, [0.5,1], is not finitely observable, because if the true value is exactly 0.5, no finite-precision measurement can establish with certainty that the value is in [0.5,1], even though it is.
The general case of why observables form a topology is more interesting. Finite intersections of finite observables are finitely observable because I can check each one in series and still need only finite observation in total. Countable unions of finite observables are finitely observable because I can check them in parallel, and if any are true then its check will succeed after only finite observation in total.
Uncountable unions are thornier, but arguably unnecessary (they’re redundant with countable unions if the space is hereditarily Lindelöf, for which being Polish is sufficient, or more generally second-countable), and can be accommodated by allowing the observer to hypercompute. This is very much beside the point, but if you are still interested anyway, check out Escardó′s monograph on the topic.
Negations of finitely observable predicates are typically not finitely observable. [0,0.5) is finitely observable as a subset of [0,1], because if the true value is in [0,0.5) then there necessarily exists a finite precision with which we can know that. But its negation, [0.5,1], is not finitely observable, because I’d the true value is exactly 0.5, no finite-precision measurement can establish with certainty that the value is in [0.5,1], even though it is.
Ah, I didn’t realize that’s what you mean by “finitely observable”—something like “if the proposition is true then there is a finite precision measurement which will show that it’s true”. That does correspond to the opens of a metric space if that’s how you formalize “precision”, but it seems like a concept that’s not too useful in practice because you actually can’t measure things to arbitrary precision in the real world. [0, 0.5) is not going to actually be observable as long as your apparatus of observation has some small but nonzero lower bound on its precision.
What’s the logic behind not making this concept symmetric, though? Why don’t we ask also for “if the proposition is false then there is a finite precision measurement which will show that it’s false”, i.e. why don’t we ask for observables to be clopens? I’m guessing it’s because this concept is too restrictive, but perhaps there’s some kind of intuitionist/constructivist justification for why you’d not want to make it symmetric like this.
Uncountable unions are thornier, but arguably unnecessary, and can be accommodated by allowing the observer to hypercompute. This is very much beside the point, but if you are still interested anyway, check out Escardó′s monograph on the topic.
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.
(I agree with your last paragraph—this thread is interesting but unfortunately beside the point since probabilistic theories are obviously trying to “say more” than just their merely nondeterministic shadows.)
Negations of finitely observable predicates are typically not finitely observable. [0,0.5) is finitely observable as a subset of [0,1], because if the true value is in [0,0.5) then there necessarily exists a finite precision with which we can know that. But its negation, [0.5,1], is not finitely observable, because if the true value is exactly 0.5, no finite-precision measurement can establish with certainty that the value is in [0.5,1], even though it is.
The general case of why observables form a topology is more interesting. Finite intersections of finite observables are finitely observable because I can check each one in series and still need only finite observation in total. Countable unions of finite observables are finitely observable because I can check them in parallel, and if any are true then its check will succeed after only finite observation in total.
Uncountable unions are thornier, but arguably unnecessary (they’re redundant with countable unions if the space is hereditarily Lindelöf, for which being Polish is sufficient, or more generally second-countable), and can be accommodated by allowing the observer to hypercompute. This is very much beside the point, but if you are still interested anyway, check out Escardó′s monograph on the topic.
Ah, I didn’t realize that’s what you mean by “finitely observable”—something like “if the proposition is true then there is a finite precision measurement which will show that it’s true”. That does correspond to the opens of a metric space if that’s how you formalize “precision”, but it seems like a concept that’s not too useful in practice because you actually can’t measure things to arbitrary precision in the real world. [0, 0.5) is not going to actually be observable as long as your apparatus of observation has some small but nonzero lower bound on its precision.
What’s the logic behind not making this concept symmetric, though? Why don’t we ask also for “if the proposition is false then there is a finite precision measurement which will show that it’s false”, i.e. why don’t we ask for observables to be clopens? I’m guessing it’s because this concept is too restrictive, but perhaps there’s some kind of intuitionist/constructivist justification for why you’d not want to make it symmetric like this.
I’ll check it out, thanks.
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.