I think that much of the meat of what I want Cartesian frames to do is connected to time, and I have only really touched the surface of that. I think that there is a lot more to say about time, and I think there are options we have about how to think about time in Cartesian frames. The one I presented is my favorite at the moment, but I am uncertain.
For example, one might want to think about an agent, and the collection of pairs of partitions U and V of W, such that the agent has a (multiplicative?) subagent that could choose U, while observing V. This collection of pairs is closed under coarsening in both arguments, and so one could talk about a sort of Pareto frontier of how refined you can make U given V or vice versa. I think this Pareto frontier looks a lot like time.
“subagent [C] that could choose U”—do you mean U⊆Ctrl(C) or U⊆Ensure(C) or neither of these? Since Ctrl is not closed under unions, I don’t think the controllables version of “could choose” is closed under coarsening the partition. (I can prove that the ensurables version is closed; but it would have been nice if the controllables version worked.)
ETA: Actually controllables do work out if I ignore the degenerate case of a singleton partition of the world. This is because, when considering partitions of the world, ensurables and controllables are almost the same thing.
Formalizing time
I think that much of the meat of what I want Cartesian frames to do is connected to time, and I have only really touched the surface of that. I think that there is a lot more to say about time, and I think there are options we have about how to think about time in Cartesian frames. The one I presented is my favorite at the moment, but I am uncertain.
For example, one might want to think about an agent, and the collection of pairs of partitions U and V of W, such that the agent has a (multiplicative?) subagent that could choose U, while observing V. This collection of pairs is closed under coarsening in both arguments, and so one could talk about a sort of Pareto frontier of how refined you can make U given V or vice versa. I think this Pareto frontier looks a lot like time.
“subagent [C] that could choose U”—do you mean U⊆Ctrl(C) or U⊆Ensure(C) or neither of these? Since Ctrl is not closed under unions, I don’t think the controllables version of “could choose” is closed under coarsening the partition. (I can prove that the ensurables version is closed; but it would have been nice if the controllables version worked.)
ETA: Actually controllables do work out if I ignore the degenerate case of a singleton partition of the world. This is because, when considering partitions of the world, ensurables and controllables are almost the same thing.