Committing, Assuming, Externalizing, and Internalizing

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 .”