I like specialization preorder as a setting for formulating these concepts. In a topological space, point y is stronger (more specialized) than point x iff all opens containing x also contain y. If opens are thought of as propositions, and specialization order as a kind of (“logical”) time, with stronger points being in the future of weaker points, then this says that propositions must be valid with respect to time (that is, we want to only allow propositions that don’t get invalidated). This setting motivates thinking of points not as objects of study, but as partial observations of objects of study, their shadows that develop according to specialization preorder. If a proposition is true about some partial observation of an object (a point of the space), it remains true when it develops further (in the future, for stronger points). The best we can capture objects of study is with neighborhood filters, but the conceptual distinction suggests that even in a sober space the objects of study are not necessarily points, they are merely observed through points.
This is just what Scott domains or more generally algebraic dcpos with Scott topology talk about, when we start with a poset of finite observations (about computations, the elusive objects of study), which is the specialization preorder of its Alexandrov topology, which then becomes Scott topology after soberification, adding points for partial observations that can be expressed in terms of Alexandrov opens on finite observations. Specialization order follows a computation, and opens formulate semidecidable properties. There are two different ways in which a computation is approximated: with a weaker observation/point, and with a weaker specification/proposition/open. One nice thing here is that we can recover points from opens, and then finite observations from the specialization poset of all partial observations/theories/ideals (as compact elements of a poset). So the different concepts fit together well, the rhetoric of observations and logical time has technical content that can be extracted just from the opens/propositions. This becomes even more concrete for coherent spaces, where finite observations are finite cliques on webs (of “atomic observations”).
(This is mostly a keyword dump, pointing to standard theory that offers a way of making sense of logical time. The interesting questions are about how to make use of this to formulate FDT and avoid spurious proofs, possibly by reasoning at a particular point of a space, the logical moment of decision, without making use of its future. A distinction this point of view enforces that is usually missing in discussions of decision theory or reasoning about programs is between approximation with weaker observations vs. with weaker propositions. This is the distinction between different logical times and different states of knowledge about a computation.)
If opens are thought of as propositions, and specialization order as a kind of (“logical”) time,
Up to here made sense.
with stronger points being in the future of weaker points, then this says that propositions must be valid with respect to time (that is, we want to only allow propositions that don’t get invalidated).
After here I was lost. Which propositions are valid with respect to time? How can we only allow propositions which don’t get invalidated (EG if we don’t know yet which will and will not be), and also, why do we want that?
This setting motivates thinking of points not as objects of study, but as partial observations of objects of study, their shadows that develop according to specialization preorder. [...] The best we can capture objects of study is with neighborhood filters, [...] start with a poset of finite observations (about computations, the elusive objects of study),
You’re saying a lot about what the “objects of study” are and aren’t, but not very concretely, and I’m not getting the intuition for why this is important. I’m used to the idea that the points aren’t really the objects of study in topology; the opens are the more central structure.
But the important question for a proposed modeling language is how well it models what we’re after.
This is mostly a keyword dump, pointing to standard theory that offers a way of making sense of logical time.
It seems like you are trying to do something similar to what cartesian frames and finite factored sets are doing, when they reconstruct time-like relationships from other (purportedly more basic) terms. Would you care to compare the reconstructions of time you’re gesturing at to those provided by cartesian frames and/or finite factored sets?
Which propositions are valid with respect to time? How can we only allow propositions which don’t get invalidated (EG if we don’t know yet which will and will not be), and also, why do we want that?
This was just defining/motivating terms (including “validity”) for this context, the technical answer is to look at the definition of specialization preorder, when it’s being suggestively called “logical time”. If an open is a “proposition”, and a point being contained in an open is “proposition is true at that point”, and a point stronger in specialization order than another point is “in the future of the other point”, then in these terms we can say that “if a proposition is true at a point, it’s also true at a future point”, or that “propositions are valid with respect to time going forward”, in the sense that their truth is preserved when moving from a point to a future point.
Logical time is intended to capture decision making, with future decisions advancing the agent’s point of view in logical time. So if an agent reasons only in terms of propositions valid with respect to advancement of logical time, then any knowledge it accumulated remains valid as it makes decisions, that’s some of the motivation for looking into reasoning in terms of such propositions.
You’re saying a lot about what the “objects of study” are and aren’t, but not very concretely, and I’m not getting the intuition for why this is important.
This is mostly about how domain theory describes computations, the interesting thing is how the computations are not necessarily in the domains at all, they only leave observations there, and it’s the observations that the opens are ostensibly talking about, yet the goal might be to understand the computations, not just the observations (in program semantics, the goal is often to understand just the observations though, and a computation might be defined to only be its observed behavior). So one point I wanted to make is to push against the perspective where points of a space are what the logic of opens is intended to reason about, when the topology is not Frechet (has nontrivial specialization preorder).
But the important question for a proposed modeling language is how well it models what we’re after.
Yeah, I’ve got nothing, just a sense of direction and a lot of theory to study, or else there would’ve been a post, not just a comment triggered by something on a vaguely similar topic. So this thread is in the same spirit as a comment I left a few months ago to a crackpot post, but that one was even more speculative, somewhat appropriate in a place like that...
I like specialization preorder as a setting for formulating these concepts. In a topological space, point y is stronger (more specialized) than point x iff all opens containing x also contain y. If opens are thought of as propositions, and specialization order as a kind of (“logical”) time, with stronger points being in the future of weaker points, then this says that propositions must be valid with respect to time (that is, we want to only allow propositions that don’t get invalidated). This setting motivates thinking of points not as objects of study, but as partial observations of objects of study, their shadows that develop according to specialization preorder. If a proposition is true about some partial observation of an object (a point of the space), it remains true when it develops further (in the future, for stronger points). The best we can capture objects of study is with neighborhood filters, but the conceptual distinction suggests that even in a sober space the objects of study are not necessarily points, they are merely observed through points.
This is just what Scott domains or more generally algebraic dcpos with Scott topology talk about, when we start with a poset of finite observations (about computations, the elusive objects of study), which is the specialization preorder of its Alexandrov topology, which then becomes Scott topology after soberification, adding points for partial observations that can be expressed in terms of Alexandrov opens on finite observations. Specialization order follows a computation, and opens formulate semidecidable properties. There are two different ways in which a computation is approximated: with a weaker observation/point, and with a weaker specification/proposition/open. One nice thing here is that we can recover points from opens, and then finite observations from the specialization poset of all partial observations/theories/ideals (as compact elements of a poset). So the different concepts fit together well, the rhetoric of observations and logical time has technical content that can be extracted just from the opens/propositions. This becomes even more concrete for coherent spaces, where finite observations are finite cliques on webs (of “atomic observations”).
(This is mostly a keyword dump, pointing to standard theory that offers a way of making sense of logical time. The interesting questions are about how to make use of this to formulate FDT and avoid spurious proofs, possibly by reasoning at a particular point of a space, the logical moment of decision, without making use of its future. A distinction this point of view enforces that is usually missing in discussions of decision theory or reasoning about programs is between approximation with weaker observations vs. with weaker propositions. This is the distinction between different logical times and different states of knowledge about a computation.)
Up to here made sense.
After here I was lost. Which propositions are valid with respect to time? How can we only allow propositions which don’t get invalidated (EG if we don’t know yet which will and will not be), and also, why do we want that?
You’re saying a lot about what the “objects of study” are and aren’t, but not very concretely, and I’m not getting the intuition for why this is important. I’m used to the idea that the points aren’t really the objects of study in topology; the opens are the more central structure.
But the important question for a proposed modeling language is how well it models what we’re after.
It seems like you are trying to do something similar to what cartesian frames and finite factored sets are doing, when they reconstruct time-like relationships from other (purportedly more basic) terms. Would you care to compare the reconstructions of time you’re gesturing at to those provided by cartesian frames and/or finite factored sets?
This was just defining/motivating terms (including “validity”) for this context, the technical answer is to look at the definition of specialization preorder, when it’s being suggestively called “logical time”. If an open is a “proposition”, and a point being contained in an open is “proposition is true at that point”, and a point stronger in specialization order than another point is “in the future of the other point”, then in these terms we can say that “if a proposition is true at a point, it’s also true at a future point”, or that “propositions are valid with respect to time going forward”, in the sense that their truth is preserved when moving from a point to a future point.
Logical time is intended to capture decision making, with future decisions advancing the agent’s point of view in logical time. So if an agent reasons only in terms of propositions valid with respect to advancement of logical time, then any knowledge it accumulated remains valid as it makes decisions, that’s some of the motivation for looking into reasoning in terms of such propositions.
This is mostly about how domain theory describes computations, the interesting thing is how the computations are not necessarily in the domains at all, they only leave observations there, and it’s the observations that the opens are ostensibly talking about, yet the goal might be to understand the computations, not just the observations (in program semantics, the goal is often to understand just the observations though, and a computation might be defined to only be its observed behavior). So one point I wanted to make is to push against the perspective where points of a space are what the logic of opens is intended to reason about, when the topology is not Frechet (has nontrivial specialization preorder).
Yeah, I’ve got nothing, just a sense of direction and a lot of theory to study, or else there would’ve been a post, not just a comment triggered by something on a vaguely similar topic. So this thread is in the same spirit as a comment I left a few months ago to a crackpot post, but that one was even more speculative, somewhat appropriate in a place like that...