That’s right. A partial function can be thought of as a subset (of its domain) and a total function on that subset. And a (total) function can be thought of as a partition (of its domain): the parts are the inverse images of each point in the function’s image.
Blackwell’s theorem says that the conditions under which κ1 can be said to be more generally useful than κ2 are precisely the situations where κ1 is a post-garbling of κ2.
Are the indices the wrong way around here?
A formalisation of the ideas in this sequence in higher-order logic, including machine verified proofs of all the theorems, is available here.
“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.
because whereas math-proof data-centers might result in our inadvertent death, something that refers to what humans want might result in deliberate torture.
I want to note that either case of screwing up this badly currently feels pretty implausible to me.
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.
With the other problem resolved, I can confirm that adding an A=∅ escape clause to the multiplicative definitions works out.
Using the idea we talked about offline, I was able to fix the proof—thanks Rohin!Summary of the fix:When D1 and D2 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 b1=b2, since we might have A⊇B1≠B2⊆A after biextensional collapse.) Then to prove h=hf1, observe that for all b∈B1, b∙1h(b′2)=b∙1h(b2) which means b⋆1h(b′2)=b⋆1f1, hence h(b′2)=f1 since a biextensional frame has no duplicate columns.
I presume the fix here will be to add an explicit A=∅ 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 null counterexample.
How is this supposed to work (focusing on the h=hf1 claim specifically)?
Earlier, hf1 was defined as follows:
given by gf1(b1)=b1⋅1f1 and hf1(b2)=f1
but there is no reason to suppose f1=r above.
It suffices to establish that Ensure(CTi)⊇Ensure(CTj)
I think the Ti and Tj here are supposed to be V and U
Indeed I think the A=∅ case may be the basis of a counterexample to the claim in 4.2. I can prove for any (finite) W with |W|>1 that there is a finite partition V of W such that C’s agent observes V according to the assuming definition but does not observe V according to the constructive multiplicative definition, if I take C=null.
nit: B1 should be D1 here
and let b2 be an element of b2.
and the second b2 should be B2. I think for these b1 and b2 to exist you might need to deal with the A=∅ case separately (as in Section 5). (Also couldn’t you just use the same b twice?)
UPDATE: I was able to prove AssumeS1(C)&AssumeS2(C)≃AssumeS1∪S2(C) in general whenever S1 and S2 are disjoint and both in Obs(C), with help from Rohin Shah, following the “restrict attention to world S1∪S2” approach I hinted at earlier.
this is clearly isomorphic to D1&…&Dm, where Di=(Bi,F,⋆i), where b⋆if=b⋆f. Thus, C’s agent can observe V according to the nonconstructive additive definition of observables.
I think this is only true if VB partitions W, or, equivalently, if vB is surjective. This isn’t shown in the proof. Is it supposed to be obvious?
EDIT: may be able to fix this by assigning any s∈V that is not in VB to the frame ⊤ so it is harmless in the product of Dis—I will try this.
And it seems we do actually need AssumeS1(C)&AssumeS2(C)≃AssumeS1∪S2(C) in the proof to justify:
Thus it suffices to show that (D1&1R2∪R3)⊗(D2&1R1∪R3)≃D1&D2&1R3.
Without it, we have to show (D1&1R2∪R3)⊗(D2&1R1∪R3)≃AssumeS1∪S2(C)&1R3 instead.
Because S1 and S2 are not a partition of the world here.
EDIT: but what we actually need in the proof is AssumeS1(C)&AssumeS2(C)&⋯≃AssumeS1∪S2(C)&… where the … do result in a partition, so I think this will work out the same as the other comment. I’m still not convinced about biextensional equivalence between the frames without the rest of the product.
I haven’t yet figured out why it’s true under ≃ - I’ll keep trying, but let me know if there’s a quick argument for why this holds. (Default next step for me would be to see if I can restrict attention to the world S1∪S2 then do something similar to my other comment.)
and observe that AssumeS1∪S2(C)≅D1&D2
This cannot be true. I can prove in general AssumeS1∪S2(C)≆AssumeS1(C)&AssumeS2(C) whenever |Agent(C)|>1 by observing that the agent cardinalities on each side differ.