I have something suggestive of a negative result in this direction:
Let C be the prime-detector situation from Section 2.1 of the coarse worlds post, and let p:W→W be the (non-surjective) function that “heats” the outcome (changes any “C” to an “H”). The frame p∘(C) is clearly in some sense equivalent to the one from the example (which deletes the temperature from the outcome) -- I am using my version just to stay within the same category when comparing frames. As a reminder, primality is not observable in C but is observable in p∘(C). Claim: No frame of the form ExternalV(C) is biextensionally equivalent to p∘(C) Proof Idea: Image(ExternalV(C))=Image(C)≠Image(p∘(C))
The kind of additional observability we get from coarsening the world seems in this case to be very different from the kind that comes from externalising part of the agent’s decision.
I have something suggestive of a negative result in this direction:
Let C be the prime-detector situation from Section 2.1 of the coarse worlds post, and let p:W→W be the (non-surjective) function that “heats” the outcome (changes any “C” to an “H”). The frame p∘(C) is clearly in some sense equivalent to the one from the example (which deletes the temperature from the outcome) -- I am using my version just to stay within the same category when comparing frames. As a reminder, primality is not observable in C but is observable in p∘(C).
Claim: No frame of the form ExternalV(C) is biextensionally equivalent to p∘(C)
Proof Idea: Image(ExternalV(C))=Image(C)≠Image(p∘(C))
The kind of additional observability we get from coarsening the world seems in this case to be very different from the kind that comes from externalising part of the agent’s decision.