Random thing I wanted to check, figured I might as well write it up:
Claim:V is observable in the frame ExternalV(C).
Proof sketch: Every column of ExternalV(C) is of the form (b,e), and every world involving the same b has the same v by construction of B. Thus, if our agent can condition on subsets of B, then our agent can condition on V as well. We’ll denote a subset of B by ^b.
Given two agent options q1,q2 in ExternalV(C), we can implement the conditional policy “if ^b then q1 else q2” by defining q(x)=q1(x) if x∈⋃^b else q2(x). (This can easily be generalized to partitions.) Thus we can implement all conditional policies, and so V is observable.
I think this is correct, though I’ve done enough handwaving and skipping of proof steps that I’m not confident.
This is not correct. It is true, however that V is observable in ExternalV(InternalV(C)).
A counter example is the 2 by 2 matrix where A chooses whether to carry and umbrella and E chooses whether or not it rains. Externalizing whether or not it rains has no effect on the frame, but the agent still cannot observe the rain.
Random thing I wanted to check, figured I might as well write it up:
Claim: V is observable in the frame ExternalV(C).
Proof sketch: Every column of ExternalV(C) is of the form (b,e), and every world involving the same b has the same v by construction of B. Thus, if our agent can condition on subsets of B, then our agent can condition on V as well. We’ll denote a subset of B by ^b.
Given two agent options q1,q2 in ExternalV(C), we can implement the conditional policy “if ^b then q1 else q2” by defining q(x)=q1(x) if x∈⋃^b else q2(x). (This can easily be generalized to partitions.) Thus we can implement all conditional policies, and so V is observable.
I think this is correct, though I’ve done enough handwaving and skipping of proof steps that I’m not confident.
This is not correct. It is true, however that V is observable in ExternalV(InternalV(C)).
A counter example is the 2 by 2 matrix where A chooses whether to carry and umbrella and E chooses whether or not it rains. Externalizing whether or not it rains has no effect on the frame, but the agent still cannot observe the rain.
Hmm, I’m not seeing it. Taking your example, let’s say that A={u,n}, E={r,s}, and W={ur,us,nr,ns}, all in the obvious way.
Whether or not it rains would be formalized by the partition V={{ur,nr},{us,ns}}.
Plugging this in to the definition from worlds, I get that B={{u},{n}}.
Plugging this in to the definition of a quotient, I get that A/B={id} (the singleton containing the identity function).
Since ExternalB(C)=(A/B,B×E,⋆), we get out a Cartesian frame whose agent has only one option, for which all properties are trivially observable.
I think B={{u,n}}.
Oh yup I was misinterpreting how B was defined, and that would also mess up my proof. Thanks!