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...
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...