Ramana Kumar

Time in Cartesian Frames

"subagent [] that could choose " -- do you mean or or neither of these? Since 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.

Time in Cartesian Frames

I have something suggestive of a negative result in this direction:

Let be the prime-detector situation from Section 2.1 of the coarse worlds post, and let be the (non-surjective) function that "heats" the outcome (changes any "C" to an "H"). The frame 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 but is observable in .**Claim:** No frame of the form is biextensionally equivalent to **Proof Idea**:

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.

Eight Definitions of Observability

With the other problem resolved, I can confirm that adding an escape clause to the multiplicative definitions works out.

Eight Definitions of Observability

Using the idea we talked about offline, I was able to fix the proof - thanks Rohin!

Summary of the fix:

When and are defined, additionally assume they are biextensional (take their biextensional collapse), which is fine since we are trying to prove a biextensional equivalence. (By the way this is why we can't take , since we might have after biextensional collapse.) Then to prove , observe that for all , which means , hence since a biextensional frame has no duplicate columns.

Eight Definitions of Observability

I presume the fix here will be to add an explicit escape clause to the multiplicative definitions. I haven't been able to confirm this works out yet (trying to work around this), but it at least removes the counterexample.

Eight Definitions of Observability

How is this supposed to work (focusing on the claim specifically)?

and so

Thus, .

Earlier, was defined as follows:

given by and

but there is no reason to suppose above.

Time in Cartesian Frames

It suffices to establish that

I think the and here are supposed to be and

Eight Definitions of Observability

Indeed I think the case may be the basis of a counterexample to the claim in 4.2. I can prove for any (finite) with that there is a finite partition of such that 's agent observes according to the assuming definition but does *not* observe according to the constructive multiplicative definition, if I take

Eight Definitions of Observability

Let

nit: should be here

and let be an element of .

and the second should be . I think for these and to exist you might need to deal with the case separately (as in Section 5). (Also couldn't you just use the same twice?)

A formalisation of the ideas in this sequence in higher-order logic, including machine verified proofs of all the theorems, is available here.