Do we lose much by restricting attention to finite Cartesian frames (i.e., with finite agent and environment)? I ask because I’m formalising these results in higher-order logic (HOL), and the category Chu(w) is too big to represent if it really must contain frames with infinite agents and also for any pair of frames the frame whose agents are the morphisms between them. The root problem is probably that I require any category’s class of objects to be a set, but it’s hard to avoid this requirement in HOL in a nice way. Everything should work out for finite frames though. (I haven’t come across any compelling examples of infinite frames, but I haven’t tried hard to think of them.)
I don’t think you lose much by focusing on finite Cartesian frames. I have mostly only been imagining finite cases.
I think there is some potential for later extending the theory to encompass game theory and probabilistic strategies, and then we might want to think of the infinite space of mixed strategies as the agent, but it wouldn’t surprise me if in doing this, we also put continuity into the system and want to assume compactness.
To see that some restriction is required here (not imposed by HOL), consider that if Chu(w) may contain arbitrary Cartesian frames over w then we would have an injection 2Chu(w)→Chu(w) that, for example, encodes a set S⊆Chu(w) as the Cartesian frame CS with Agent(CS)=S (the environment and evaluation function are unimportant), which runs afoul of Cantor’s theorem regarding the cardinality of Chu(w).
I wouldn’t be surprised if a similar encoding/injection could be made using just the operations used to construct Cartesian frames that appear in this sequence—though I have not found one explicitly myself yet.
Do we lose much by restricting attention to finite Cartesian frames (i.e., with finite agent and environment)? I ask because I’m formalising these results in higher-order logic (HOL), and the category Chu(w) is too big to represent if it really must contain frames with infinite agents and also for any pair of frames the frame whose agents are the morphisms between them. The root problem is probably that I require any category’s class of objects to be a set, but it’s hard to avoid this requirement in HOL in a nice way. Everything should work out for finite frames though. (I haven’t come across any compelling examples of infinite frames, but I haven’t tried hard to think of them.)
I don’t think you lose much by focusing on finite Cartesian frames. I have mostly only been imagining finite cases.
I think there is some potential for later extending the theory to encompass game theory and probabilistic strategies, and then we might want to think of the infinite space of mixed strategies as the agent, but it wouldn’t surprise me if in doing this, we also put continuity into the system and want to assume compactness.
To see that some restriction is required here (not imposed by HOL), consider that if Chu(w) may contain arbitrary Cartesian frames over w then we would have an injection 2Chu(w)→Chu(w) that, for example, encodes a set S⊆Chu(w) as the Cartesian frame CS with Agent(CS)=S (the environment and evaluation function are unimportant), which runs afoul of Cantor’s theorem regarding the cardinality of Chu(w).
I wouldn’t be surprised if a similar encoding/injection could be made using just the operations used to construct Cartesian frames that appear in this sequence—though I have not found one explicitly myself yet.