This is the tenth post in the Cartesian frames sequence.

Here, we define a bunch of ways to construct new (additive/multiplicative) (sub/super)-(agents/environments) from a given Cartesian frame. Throughout this post, we will start with a single Cartesian frame over .

We will start by defining operations from taking subsets and partitions of  and . We will then define similar operations from taking subsets and partitions of .

 

1. Definitions from Agents and Environments

1.1. Committing

Definition: Given a subset , let  denote the Cartesian frame , with  given by . Let  denote the Cartesian frame , with  given by .

 represents the perspective you get when the agent of  makes a commitment to choose an element of , while  represents the perspective you get when the agent of  makes a commitment to choose an element outside of .

Claim: For all  and . Further,  and  are brothers in .

Proof: That  and  is trivial from the committing definition of additive subagent.

Observe that , where  is given by  if , and  if . Let  be the diagonal, . We clearly have that  is in , where  is the restriction of  to , and that ; so  and  are brothers in 

Claim: 

Proof: Trivial. 

 

1.2. Assuming

Assuming is the dual operation to committing.

Definition: Given a subset , let  denote the Cartesian frame , with  given by . Let  denote the Cartesian frame , with  given by .

 represents the perspective you get when you assume the environment is chosen from , while  represents the perspective you get when you assume the environment is chosen from outside of .

In "Introduction to Cartesian Frames" §3.2 (Examples of Controllables), I noted the counter-intuitive result that agents have no control in worlds where a meteor (or other event) could have prevented their existence:

.

Here, we see that we can use  to recover the more intuitive idea of "control." The subagent modified by the assumption "there's no meteor" can have controllables, even though the original agent has no controllables:

.

Claim: For all  and . Similarly, for all  and .

Proof: Trivial. 

Claim: For all  and 

Proof: Trivial. 

 

1.3. Externalizing

Note that for the following definitions, when we say " is a partition of ," we mean that  is a set of nonempty subsets of , such that for each , there exists a unique  such that 

Definition: Given a partition  of , let  denote the set of all functions  from  to  such that  for all .

Definition: Given a partition  of , let  denote the Cartesian Frame , where  is given by . Let  denote the Cartesian Frame , where  is given by .

We say "externalizing " for  and "externalizing mod " for .

 can be thought of the result of the agent of  first factoring its choice into choosing an equivalence class in , and choosing an element of each equivalence class, and then externalizing the part of itself that chooses an equivalence class. I.e., we are drawing a new Cartesian frame which treats the choice of equivalence class as part of the environment, rather than part of the agent.

Similarly,  can be thought of the result of the agent of  factoring as above, then externalizing the part of itself that chooses an element of each equivalence class.

Claim: For all partitions  of  and . Further,  and  are sisters in .

Proof: Let  and .

First, observe that for every , there exists a morphism , with  given by , and  given by . To see that this is a morphism, observe that for all  and ,

Let  be given by , and let , where

Our goal is to show that , and that .

To see , we define  and  as follows.

First,  is given by . We first need to confirm that  is surjective. Given any , we can let  be the set with  and construct a function  by saying , and for each , choosing an , and saying . Observing that , we have that  is surjective and thus has a right inverse.

We choose  to be any right inverse to . Similarly, we define  by , which is clearly surjective, and define  to be any right inverse to . (Indeed,  is bijective as long as  is nonempty.)

Then, for all  and , we have

so  is a morphism. This also gives us that for all  and  we have

so  is a morphism. We know  is homotopic to the identity on , since  is the identity on , and we know that  is homotopic to the identity on , since  is the identity on . Thus, .

To show that , it suffices to show that

and

where  and  are given by

Indeed, we show that if  is nonempty, , and .

If  is nonempty, then the function from  to  given by  is a bijection, since it is clearly surjective, and is injective because  is uniquely defined by . This gives a bijection between  and , and we have that for all , and ,

Similarly, we have a bijection between  and , and for all , and ,

If  is empty, then  is empty, and  is a singleton empty function, so , and we either have  or , depending on whether or not  is empty.

Thus, , so  and  are sisters in 

 

1.4. Internalizing

Definition: Given a partition  of , let  denote the Cartesian Frame , where  is given by . Let   denote the Cartesian Frame , where  is given by 

We say "internalizing " for  and "internalizing mod " for .

Claim: For all partitions  of  and . Similarly, for all partitions  of  and 

Proof: Trivial. 

Claim: For all partitions  of  and .

Proof: This follows from the fact that  and , and the fact that multiplicative subagent is equivalent to multiplicative sub-environment. 

 

2. Definitions from Worlds

The above definitions are dependent on subsets and partitions of a given  and , and thus do not represent a single operation that can be applied to an arbitrary Cartesian frame over . We will now use the above eight definitions to define another eight operations that instead use subsets and partitions of .

Once we have the following definitions in hand, our future references to committing, assuming, externalizing, and internalizing will use the definitions from worlds unless noted otherwise.

 

2.1. Committing

Definition: Given a set , we define  and , where  is given by .

Claim: For all  and . Further,  and  are brothers in .

Proof: Trivial. 

Unlike before, it is not necessarily the case that . This is because there might be rows that contains both elements of  and elements of .

 

2.2. Assuming

Definition: Given , we define  and , where  is given by 

Claim: For all  and  and .

Proof: Trivial. 

Claim: For all  and .

Proof: Trivial. 

 

2.3. Externalizing

Definition: Given a partition  of , let  send each element  to the part that contains it. We define  and , where .

Claim: For all partitions  of  and . Further,  and  are sisters in .

Proof: Trivial. 

 

2.4. Internalizing

Definition: Given a partition  of , let  send each element  to the part that contains it. We define  and , where .

Claim: For all partitions  of  and 

Proof: Trivial. 

Claim: For all partitions  of , and 

Proof: Trivial. 

 

3. Basic Properties

3.1. Biextensional Equivalence

Committing and assuming are well-defined up to biextensional equivalence.

Claim: If  are Cartesian frames over , then for any subset ,, and .

Proof: Let , and let  and  compose to something homotopic to the identity in both orders. Let  be defined by .

Observe that if , then for all , so . Similarly, if , then . Thus, if we let  be given by , we get morphisms , which are clearly morphisms, since they are restrictions of our original morphisms .

Since  and  compose to something homotopic to the identity in both orders,  is a morphism, so  is a morphism, so  and  compose to something homotopic to the identity in both orders. Thus .

Similarly, if , then there exists an  such that . But then

, so . Similarly, if , then . Thus, if we let  be given by , we get morphisms , which (similarly to above) compose to something homotopic to the identity in both orders. Thus, .

We know that  and , because

and

Externalizing and internalizing are also well-defined up to biextensional equivalence.

Claim: If  are Cartesian frames over , then for all partitions  of , and .

Proof: Let , and let  and  compose to something homotopic to the identity in both orders. Let  be a partition of W, and let  send each element  to the part that contains it. Let  be the partition of  defined by 

Let , send each element of  to its part in , so . Since  is surjective, it has a right inverse. Let  be any choice of right inverse to . This gives a pair of functions  given by .

We start by showing that  and  are inverses, and thus bijections between  and . We do this by showing that , and that  , and thus we will have

which is the identity on .

To see that , observe that for all , we have that for all , so, . Thus, .

To see that , first observe that for all , we have that , and thus, for all ,

Thus, . Thus, we have

This also gives us functions , by . To ehow that these functions are well-defined, we need to show that for all ,   is in fact in , by showing that for all ,  , or equivalently that  is the identity on . Since , we already have that  is the identity of . Thus, we have that

is the identity on .

We are now ready to demonstrate that .

Let , and define

by , while  is given by .

To see that  is a morphism, observe that for all , and  we have

To see that  is homotopic to the identity, we show that

is a morphism. Indeed, for all  and ,

Thus, 

Similarly, let , and define

by , and  is given by .

To see that  is a morphism, observe that for all , and , we have 

Clearly,  is homotopic to the identity, since  is the identity on . Thus, .

We know that  and , because

and

 

3.2. Committing and Assuming Can Be Defined Using Lollipop and Tensor

Claim:  and .

Proof: Let , and let 

Let , where , and 

Let , where

We construct an isomorphism , by defining  by , and by defining  by .

First, we need to show that  is a well-defined function into . Observe that for all , and for all ,

, and so .

Next, we show that  is a morphism, by showing that for all  and ,

Finally, to show that , we need to show that  and  are bijections. Clearly,  is a bijection. To see that  is injective, observe that if , then , so . Further, for all 

so . Thus  is injective. To see that  is surjective, observe that for all , there exists a morphism , given by , and . This is a morphism because, for all  and ,

Since

we have that  is surjective, and thus  is an isomorphism between  and .

To see that , observe that

Recall that we can think of  as a powerless agent that has been promised , then, is a team consisting of  alongside an agent that has been promised .

In order for these two to form a team, the promise  must still hold for the team as a whole; and since  is powerless, the resultant team is exactly  joined with the promise, i.e., .

 is less intuitive.  is " with a hole in it shaped like a promise that  happens." In effect, an agent-and-hole can only "fit" such a promise into itself by being the kind of agent-and-hole that always guarantees  will happen.

It will sometimes be helpful to think about assuming and committing in terms of , as this highlights the close relationship between these operations and the other objects and operations we've been working with.1

 

4. Idempotence

We will show that all eight of the new definition from worlds are idempotent (up to isomorphism). We will do this by in each case describing the subset of Cartesian frames over  that each operation projects onto, and showing that the operation is indeed fixed on that subset.

 

4.1. Committing and Assuming

Claim: For any Cartesian frame  over  and subset  of  and .

Proof: Trivial. 

Claim: For any Cartesian frame  over  and subset  of , with .

Proof: Trivial. 

Corollary: For any subset  of  and  are idempotent.

Proof: Trivial. 

Claim: For any Cartesian frame  over  and subset  of , if , then for all , there exists an  such that .

Proof: Trivial. 

Claim: For any Cartesian frame  over  and subset  of , if for all , there exists an  such that , then .

Proof: Trivial. 

Corollary: For any subset  of  is idempotent.

Proof: Trivial. 

Claim: For any Cartesian frame  over  and subset  of , if , then for all , there exists an  such that .

Proof: Trivial. 

Claim: For any Cartesian frame  over  and subset  of , if for all , there exists an  such that , then .

Proof: Trivial. 

Corollary: For any subset  of  is idempotent.

Proof: Trivial. 

 

4.2. Externalizing

Claim: For any Cartesian frame  over  and partition  of , let  send each element of  to its part in . If , then  is nonempty and for all  and , we have .

Proof: Let  be defined, as in the definition of , as  is , the set of functions from  to  that sends each part in  to an element of that part, and  is clearly nonempty. Consider an arbitrary  and . Since  are in the same part, we have that , and thus 

Claim: For any Cartesian frame  over  and partition  of , let  send each element of  to its part in . If  is nonempty and for all  and  we have , then .

Proof: Let  be defined, as in the definition of , as . If  is nonempty and for all  and , we have , then  has only one part, . Thus, , where  is given by .

Let  be given by , and . This is trivially a morphism, and both  and  are trivially bijections, so .

Corollary: For any partition  of  is idempotent.

Proof: Trivial. 

Claim: For any Cartesian frame  over  and partition  of , let  send each element of  to its part in . If , then for all  there exists an , such that .

Proof: Let  be defined once again as  and . Since  is clearly nonempty, fix any . Observe that if , then  and  are in different parts in B, so there exists an  such that . Thus 

Claim: For any Cartesian frame  over  and partition  of , let  send each element of  to its part in . If for all  there exists an , such that , then .

Proof: Again, let  be defined again as . If for all  there exists an  such that , then every element of  is a singleton. Thus  is a singleton, and  is a bijection.

, where  is given by . Let  be given by , and . This is trivially a morphism and both  and  are trivially bijections, so 

Corollary: For any partition  of  is idempotent.

Proof: Trivial. 

 

4.3. Internalizing

Using duality, we also get all of the following analogous results for internalizing.

Claim: For any Cartesian frame  over  and partition  of , let  send each element of  to its part in . If , then  is nonempty and for all  and , we have .

Proof: Trivial. 

Claim: For any Cartesian frame  over  and partition  of , let  send each element of  to its part in . If for all  and  we have , then .

Proof: Trivial. 

Corollary: For any partition  of  is idempotent.

Proof: Trivial. 

Claim: For any Cartesian frame  over  and partition  of , let  send each element of  to its part in . If , then for all  there exists an , such that .

Proof: Trivial. 

Claim: For any Cartesian frame  over  and partition  of , let  send each element of  to its part in . If for all  there exists an , such that , then .

Proof: Trivial. 

Corollary: For any partition  of  is idempotent.

Proof: Trivial. 

 

Our new assuming, internalizing, and externalizing operations will also provide a new lens for us to better understand observables. We turn to this in our next post, "Eight Definitions of Observability."


Footnotes

1. This section is a good distillation of  as it relates to multiplicative operations. The additive role of  is quite different from this, and quite varied. There isn't a single interpretation for  in additive contexts, beyond the basic interpretation we provided in "Biextensional Equivalence" that  is "a powerless, all-knowing agent... plus a promise from the environment that the world will be in ."

New Comment
25 comments, sorted by Click to highlight new comments since:

Random thing I wanted to check, figured I might as well write it up:

Claim:  is observable in the frame .

Proof sketch: Every column of  is of the form , and every world involving the same  has the same  by construction of . Thus, if our agent can condition on subsets of , then our agent can condition on  as well. We'll denote a subset of  by .

Given two agent options  in , we can implement the conditional policy "if  then  else " by defining . (This can easily be generalized to partitions.) Thus we can implement all conditional policies, and so  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  is observable in .

A counter example is the 2 by 2 matrix where  chooses whether to carry and umbrella and  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 , and , all in the obvious way.

Whether or not it rains would be formalized by the partition .

Plugging this in to the definition from worlds, I get that .

Plugging this in to the definition of a quotient, I get that  (the singleton containing the identity function).

Since , we get out a Cartesian frame whose agent has only one option, for which all properties are trivially observable.

I think .

Oh yup I was misinterpreting how B was defined, and that would also mess up my proof. Thanks!

while  is given by 

 should be applied to  above, I think

Fixed, thanks.

Let , send each element of  to its part in , so .

Presuming the  here should be a 

Fixed, thanks.

So, the interpretation of isn't super clear in the text, and had me confused for a sec, but I believe it basically means that the agent is committing to take actions such that the environment can avoid the state of the world ending up in - which makes sense as a commitment to make!

From the first proof in 1.1:

We clearly have that (A,D,∙′) is CommitB(C)⊞Commit∖B(C),

Should this instead read "We clearly have that (A,D,∙′) is in CommitB(C)⊞Commit∖B(C),"?

Yep, Thanks.

Claim: For any Cartesian frame  over  and partition  of , let  send each element of  to its part in . If for all  and  we have , then .

I think this may also need to assume that  is non-empty.

Fixed, Thanks

If 

The  argument is missing in several places like this from 4.2 onwards.

Fixed at least some of them.

 is given by 

There's a prime missing on . I'd also have expected  instead of  as the variable (doesn't affect correctness).

Fixed, thanks.

Claim: For all  and 

Are these the wrong way around?

I believe  is indeed trivial, but the opposite is less obvious.

This is also suspicious in section 2.2 about Assuming. I think it should be the other way around and about Assume rather than Commit, and I don't think that's equivalent to what's written here. (But I'm not confident about this.)

Claim: For all  and .

Oh I see this has also been fixed. Thanks!

Fixed, Thanks.

Similarly, for all  and .

 

We don't need  to be a proper subset here (i.e., I think  is a typo for ). Also in my view all the isomorphisms in this section are actually equalities (but it's also reasonable to never consider equality of frames).

Yeah, the  was a typo, and I just never consider equality of frames.