AI ALIGNMENT FORUM
AF

Cartesian Frames
Embedded AgencySubagentsAI
Frontpage

15

Committing, Assuming, Externalizing, and Internalizing

by Scott Garrabrant
9th Nov 2020
12 min read
25

15

Embedded AgencySubagentsAI
Frontpage
Previous:
Additive and Multiplicative Subagents
7 comments20 karma
Next:
Eight Definitions of Observability
26 comments34 karma
Log in to save where you left off
Committing, Assuming, Externalizing, and Internalizing
5Rohin Shah
6Scott Garrabrant
4Rohin Shah
3Scott Garrabrant
4Rohin Shah
2Ramana Kumar
1Scott Garrabrant
2Ramana Kumar
1Scott Garrabrant
2DanielFilan
2DanielFilan
1Scott Garrabrant
1Ramana Kumar
1Scott Garrabrant
1Ramana Kumar
1Scott Garrabrant
1Ramana Kumar
1Scott Garrabrant
1Ramana Kumar
1Ramana Kumar
1Ramana Kumar
1Scott Garrabrant
1Ramana Kumar
1Scott Garrabrant
1Rob Bensinger
New Comment
25 comments, sorted by
top scoring
Click to highlight new comments since: Today at 5:00 AM
[-]Rohin Shah5y50

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

Claim: V is observable in the frame ExternalV(C).

Proof sketch: Every column of ExternalV(C) is of the form (b,e), and every world involving the same b has the same v by construction of B. Thus, if our agent can condition on subsets of B, then our agent can condition on V as well. We'll denote a subset of B by ^b.

Given two agent options q1,q2 in ExternalV(C), we can implement the conditional policy "if ^b then q1 else q2" by defining q(x)=q1(x) if x∈⋃^b else q2(x). (This can easily be generalized to partitions.) Thus we can implement all conditional policies, and so V is observable.

I think this is correct, though I've done enough handwaving and skipping of proof steps that I'm not confident.

Reply
[-]Scott Garrabrant5y60

This is not correct. It is true, however that V is observable in ExternalV(InternalV(C)).

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

Reply
[-]Rohin Shah5y40

Hmm, I'm not seeing it. Taking your example, let's say that A={u,n}, E={r,s}, and W={ur,us,nr,ns}, all in the obvious way.

Whether or not it rains would be formalized by the partition V={{ur,nr},{us,ns}}.

Plugging this in to the definition from worlds, I get that B={{u},{n}}.

Plugging this in to the definition of a quotient, I get that A/B={id} (the singleton containing the identity function).

Since ExternalB(C)=(A/B,B×E,⋆), we get out a Cartesian frame whose agent has only one option, for which all properties are trivially observable.

Reply
[-]Scott Garrabrant5y30

I think B={{u,n}}.

Reply
[-]Rohin Shah5y40

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

Reply
[-]Ramana Kumar5y20

while h′i:B1−i×E1−i→Bi×Ei is given by h′i(b,e)=(ι1−i,hi(e))

ι1−i should be applied to b above, I think

Reply
[-]Scott Garrabrant5y10

Fixed, thanks.

Reply
[-]Ramana Kumar5y20

Let βi:Ai→Bi, send each element of Ai to its part in Bi, so α(a)={a′∈Ai | ∀e∈Ei, v(a′⋅e)=v(a⋅e)}.

Presuming the α here should be a βi

Reply
[-]Scott Garrabrant5y10

Fixed, thanks.

Reply
[-]DanielFilan5y20

So, the interpretation of Commit∖S(C) 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 S - which makes sense as a commitment to make!

Reply
[-]DanielFilan5y20

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),"?

Reply
[-]Scott Garrabrant5y10

Yep, Thanks.

Reply
[-]Ramana Kumar5y10

Claim: For any Cartesian frame C=(A,E,⋅) over W and partition V of W, let v:W→V send each element of W to its part in V. If for all a0,a1∈A and e∈E, we have v(a0⋅e)=v(a1⋅e), then ExternalV(C)≅C.

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

Reply
[-]Scott Garrabrant5y10

Fixed, Thanks

Reply
[-]Ramana Kumar5y10

If ExternalV=(A′,E′,⋅′)

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

Reply
[-]Scott Garrabrant5y10

Fixed at least some of them.

Reply
[-]Ramana Kumar5y10

h′′i:A1−i/B1−i×E1−i→Ai/Bi×Ei is given by h′i(b,e)=(f1−i(b),hi(e))

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

Reply
[-]Scott Garrabrant5y10

Fixed, thanks.

Reply
[-]Ramana Kumar5y10

Claim: For all F⊆E, AssumeF(C)◃∗+C and Assume∖F(C)◃∗+C. 

Are these the wrong way around?

I believe C◃∗+AssumeF(C) is indeed trivial, but the opposite is less obvious.

Reply
[-]Ramana Kumar5y10

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 S⊆W, CommitS(C)◃∗+C and Commit∖S(C)◃∗+C.

Reply
[-]Ramana Kumar5y10

Oh I see this has also been fixed. Thanks!

Reply
[-]Scott Garrabrant5y10

Fixed, Thanks.

Reply
[-]Ramana Kumar5y10

Similarly, for all B⊂A, (CommitB(C))∗≅AssumeB(C∗) and (Commit∖B(C))∗≅Assume∖B(C∗).

 

We don't need B 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).

Reply
[-]Scott Garrabrant5y10

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

Reply
[-]Rob Bensinger5y10

I've added the section-2 definitions above to https://www.lesswrong.com/posts/kLLu387fiwbis3otQ/cartesian-frames-definitions.

Reply
Moderation Log
More from Scott Garrabrant
View more
Curated and popular this week
25Comments

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 W, C=(A,E,⋅).

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

 

1. Definitions from Agents and Environments

1.1. Committing

Definition: Given a subset B⊆A, let CommitB(C) denote the Cartesian frame (B,E,⋆), with ⋆ given by b⋆e=b⋅e. Let Commit∖B(C) denote the Cartesian frame (A∖B,E,⋄), with ⋄ given by a⋄e=a⋅e.

CommitB(C) represents the perspective you get when the agent of C makes a commitment to choose an element of B, while Commit∖B(C) represents the perspective you get when the agent of C makes a commitment to choose an element outside of B.

Claim: For all B⊆A, CommitB(C)◃+C and Commit∖B(C)◃+C. Further, Commit∖B(C) and CommitB(C) are brothers in C.

Proof: That CommitB(C)◃+C and Commit∖B(C)◃+C is trivial from the committing definition of additive subagent.

Observe that CommitB(C)⊕Commit∖B(C)=(A,E×E,∙), where ∙ is given by a∙(e,f)=a⋅e if a∈B, and a∙(e,f)=a⋅f if a∉B. Let D⊂E×E be the diagonal, {(e,e) | e∈E}. We clearly have that (A,D,∙′) is in CommitB(C)⊞Commit∖B(C), where ∙′ is the restriction of ∙ to A×D, and that (A,D,∙′)≅C; so Commit∖B(C)◃+C and CommitB(C)◃+C are brothers in C. □

Claim: Commit∖B(C)≅CommitA∖B(C)

Proof: Trivial. □

 

1.2. Assuming

Assuming is the dual operation to committing.

Definition: Given a subset F⊆E, let AssumeF(C) denote the Cartesian frame (A,F,⋆), with ⋆ given by a⋆f=a⋅f. Let Assume∖F(C) denote the Cartesian frame (A,E∖F,⋄), with ⋄ given by a⋄e=a⋅e.

AssumeF(C) represents the perspective you get when you assume the environment is chosen from F, while Assume∖F(C) represents the perspective you get when you assume the environment is chosen from outside of F.

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:

C0=     rsmunu↔ru↔s⎛⎜ ⎜ ⎜⎝urusmnrnsmurnsmnrusm⎞⎟ ⎟ ⎟⎠.

Here, we see that we can use Assume∖F(C) 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:

Assume∖{m}(C0)=     rsunu↔ru↔s⎛⎜ ⎜ ⎜⎝urusnrnsurnsnrus⎞⎟ ⎟ ⎟⎠.

Claim: For all F⊆E, (AssumeF(C))∗≅CommitF(C∗) and (Assume∖F(C))∗≅Commit∖F(C∗). Similarly, for all B⊆A, (CommitB(C))∗≅AssumeB(C∗) and (Commit∖B(C))∗≅Assume∖B(C∗).

Proof: Trivial. □

Claim: For all F⊆E, C◃∗+AssumeF(C) and C◃∗+Assume∖F(C). 

Proof: Trivial. □

 

1.3. Externalizing

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

Definition: Given a partition X of Y, let Y/X denote the set of all functions q from X to Y such that q(x)∈x for all x∈X.

Definition: Given a partition B of A, let ExternalB(C) denote the Cartesian Frame (A/B,B×E,⋆), where ⋆ is given by q⋆(b,e)=q(b)⋅e. Let External/B(C) denote the Cartesian Frame (B,A/B×E,⋄), where ⋄ is given by b⋄(q,e)=q(b)⋅e.

We say "externalizing B" for ExternalB and "externalizing mod B" for External/B.

ExternalB(C) can be thought of the result of the agent of C first factoring its choice into choosing an equivalence class in B, 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, External/B(C) can be thought of the result of the agent of C factoring as above, then externalizing the part of itself that chooses an element of each equivalence class.

Claim: For all partitions B of A, ExternalB(C)◃×C and External/B(C)◃×C. Further, ExternalB(C) and External/B(C) are sisters in C.

Proof: Let ExternalB(C)=(A/B,B×E,⋆) and External/B(C)=(B,A/B×E,⋄).

First, observe that for every e∈E, there exists a morphism (ge,he):ExternalB(C)→(External/B(C))∗, with ge:→A/B×E given by ge(q)=(q,e), and he:B→B×E given by he(b)=(b,e). To see that this is a morphism, observe that for all q∈A/B and b∈B,

ge(q)⋄b=q(b)⋅e=q⋆he(b).

Let E′⊆hom(ExternalB(C),(External/B(C))∗) be given by E′={(ge,he) | e∈E}, and let D=(A/B×B,E′,∙), where

(q,b)∙(ge,he)=ge(q)⋄b=q⋆he(b)=q(b)⋅e.

Our goal is to show that D∈ExternalB(C)⊠External/B(C), and that D≃C.

To see D≃C, we define (g0,h0):D→C and (g1,h1):C→D as follows.

First, g0:A/p×B→A is given by g0(q,b)=q(b). We first need to confirm that g0 is surjective. Given any a∈A, we can let b∈B be the set with a∈b and construct a function q∈A/B by saying q(b)=a, and for each b′≠b, choosing an a′∈b′, and saying q(b′)=a′. Observing that g0(q,b)=a, we have that g0 is surjective and thus has a right inverse.

We choose g1:A→A/B×B to be any right inverse to g0. Similarly, we define h0:E→E′ by h0(e)=(ge,he), which is clearly surjective, and define h1:E′→E to be any right inverse to h0. (Indeed, h0 is bijective as long as A is nonempty.)

Then, for all (q,b)∈A/B×B and e∈E, we have

g0(q,b)⋅e=q(b)⋅e=(q,b)∙(ge,he)=q,b∙h0(e),

so (g0,h0) is a morphism. This also gives us that for all a∈A and e′∈E′ we have

g1(a)∙e′=g1(a)∙h0(h1(e′))=g0(g1(a))⋅h1(e)=a⋅h1(e),

so (g1,h1) is a morphism. We know (g0,h0)∘(g1,h1) is homotopic to the identity on C, since g0∘g1 is the identity on A, and we know that (g1,h1)∘(g0,h0) is homotopic to the identity on D, since h0∘h1 is the identity on E′. Thus, D≃C.

To show that D∈ExternalB(C)⊠External/B(C), it suffices to show that

ExternalB(C)=(A/B,B×E,⋆)≃(A/B,B×E′,⋆′),

and

External/B(C)=(B,A/B×E,⋄)≃(B,A/B×E′,⋄′),

where ⋆′ and ⋄′ are given by

q⋆′(b,(ge,he))=b⋄′(q,(ge,he))=q⋆he(b)=b⋄ge(q)=q(b)⋅e.

Indeed, we show that if A is nonempty, (A/B,B×E,⋆)≅(A/B,B×E′,⋆′), and (B,A/B×E,⋄)≅(B,A/B×E′,⋄′).

If A is nonempty, then the function from E to E′ given by e↦(ge,he) is a bijection, since it is clearly surjective, and is injective because e is uniquely defined by ge(a)=(a,e). This gives a bijection between B×E and B×E′, and we have that for all q∈A/B, b∈B, and e∈E,

q⋆′(b,(ge,he))=q(b)⋅e=q⋆(b,e).

Similarly, we have a bijection between A/B×E and A/B×E′, and for all q∈A/B, b∈B, and e∈E,

b⋄′(q,(ge,he))=q(b)⋅e=b⋄(q,e).

If A is empty, then B is empty, and A/p is a singleton empty function, so (A/B,B×E,⋆)≃(A/B,B×E′,⋆′)≃⊤, and we either have (B,A/B×E,⋄)≃(B,A/B×E′,⋄′)≃0 or (B,A/B×E,⋄)≃(B,A/B×E′,⋄′)≃null, depending on whether or not E is empty.

Thus, D∈ExternalB(C)⊠External/B(C), so ExternalB(C) and External/B(C) are sisters in C. □

 

1.4. Internalizing

Definition: Given a partition F of E, let InternalF(C) denote the Cartesian Frame (F×A,E/F,⋆), where ⋆ is given by (f,a)⋆q=a⋅q(f). Let  Internal/F(C) denote the Cartesian Frame (E/F×A,F,⋄), where ⋄ is given by (q,a)⋄f=a⋅q(f). 

We say "internalizing p" for Internalp and "internalizing mod p" for Internal/p.

Claim: For all partitions F of E, (InternalF(C))∗≅ExternalF(C∗) and (Internal/F(C))∗≅External/F(C∗). Similarly, for all partitions B of A, (ExternalB(C))∗≅InternalB(C∗) and (External/B(C))∗≅Internal/B(C∗). 

Proof: Trivial. □

Claim: For all partitions F of E, C◃×InternalF(C) and C◃×Internal/F(C).

Proof: This follows from the fact that (InternalF(C))∗≅ExternalF(C∗)◃×C∗ and (Internal/F(C))∗≅External/F(C∗)◃×C∗, 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 A and E, and thus do not represent a single operation that can be applied to an arbitrary Cartesian frame over W. We will now use the above eight definitions to define another eight operations that instead use subsets and partitions of W.

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 S⊆W, we define CommitS(C)=CommitB(C) and Commit∖S(C)=Commit∖B(C), where B⊆A is given by B={a∈A | ∀e∈E,a⋅e∈S}.

Claim: For all S⊆W, CommitS(C)◃+C and Commit∖S(C)◃+C. Further, Commit∖S(C) and CommitS(C) are brothers in C.

Proof: Trivial. □

Unlike before, it is not necessarily the case that Commit∖S(C)≅CommitW∖S(C). This is because there might be rows that contains both elements of S and elements of W∖S.

 

2.2. Assuming

Definition: Given S⊆W, we define AssumeS(C)=AssumeF(C) and Assume∖S(C)=Assume∖F(C), where F⊆E is given by F={e∈E | ∀a∈A,a⋅e∈S}.

Claim: For all S⊆W, (AssumeS(C))∗≅CommitS(C∗) and (Assume∖S(C))∗≅Commit∖S(C∗), (CommitS(C))∗≅AssumeS(C∗) and (Commit∖S(C))∗≅Assume∖S(C∗).

Proof: Trivial. □

Claim: For all S⊆W, C◃∗+AssumeS(C) and C◃∗+Assume∖S(C).

Proof: Trivial. □

 

2.3. Externalizing

Definition: Given a partition V of W, let v:W→V send each element w∈W to the part that contains it. We define ExternalV(C)=ExternalB(C) and External/V(C)=External/B(C), where B={{a′∈A | ∀e∈E, v(a′⋅e)=v(a⋅e)} | a∈A}.

Claim: For all partitions V of W, ExternalV(C)◃×C and External/V(C)◃×C. Further, ExternalV(C) and External/V(C) are sisters in C.

Proof: Trivial. □

 

2.4. Internalizing

Definition: Given a partition V of W, let v:W→V send each element w∈W to the part that contains it. We define InternalV(C)=InternalF(C) and Internal/V(C)=Internal/F(C), where F={{e′∈E | ∀a∈a, v(a⋅e′)=v(a⋅e)} | e∈E}.

Claim: For all partitions V of W, C◃×InternalV(C) and C◃×Internal/V(C). 

Proof: Trivial. □

Claim: For all partitions V of W, (InternalV(C))∗≅ExternalV(C∗), (Internal/V(C))∗≅External/V(C∗), (ExternalV(C))∗≅InternalV(C∗), and (External/V(C))∗≅Internal/V(C∗). 

Proof: Trivial. □

 

3. Basic Properties

3.1. Biextensional Equivalence

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

Claim: If C0≃C1 are Cartesian frames over W, then for any subset S⊆W, CommitS(C0)≃CommitS(C1), Commit∖S(C0)≃Commit∖S(C1),AssumeS(C0)≃AssumeS(C1), and Assume∖S(C0)≃Assume∖S(C1).

Proof: Let Ci=(Ai,Ei,⋅i), and let (g0,h0):C0→C1 and (g1,h1):C1→C0 compose to something homotopic to the identity in both orders. Let Bi⊂Ai be defined by Bi={a∈Ai | ∀e∈Ei, a⋅ie∈S}.

Observe that if b∈B0, then for all e∈E1, g0(b)⋅1e=b⋅0h0(e)∈S, so g0(b)∈B1. Similarly, if b∈B1, then g1(b)∈B0. Thus, if we let g′i:Bi→B1−i be given by g′i(b)=gi(b), we get morphisms (g′i,hi):CommitS(Ci)→CommitS(C1−i), which are clearly morphisms, since they are restrictions of our original morphisms (gi,hi).

Since (g0,h0) and (g1,h1) compose to something homotopic to the identity in both orders, (idAi,h1−i∘hi):Ci→Ci is a morphism, so (idBi,h1−i∘hi):CommitS(Ci)→CommitS(Ci) is a morphism, so (g′0,h0) and (g′1,h1) compose to something homotopic to the identity in both orders. Thus CommitS(C0)≃CommitS(C1).

Similarly, if b∈A0∖B0, then there exists an e∈E0 such that b⋅0e∉S. But then

g0(b)⋅1h1(e)=g1(g0(b))⋅0e=b⋅0e

∉S, so g0(b)∈A1∖B1. Similarly, if b∈A1∖B1, then g1(b)∈A0∖B0. Thus, if we let g′′i:Ai∖Bi→A1−i∖B1−i be given by g′′i(b)=gi(b), we get morphisms (g′′i,hi):Commit∖S(Ci)→Commit∖S(C1−i), which (similarly to above) compose to something homotopic to the identity in both orders. Thus, Commit∖S(C0)≃Commit∖S(C1).

We know that AssumeS(C0)≃AssumeS(C1) and Assume∖S(C0)≃Assume∖S(C1), because

(AssumeS(C0))∗≅CommitS(C∗0)≃CommitS(C∗1)≅AssumeS(C1)

and

(Assume∖S(C0))∗≅Commit∖S(C∗0)≃Commit∖S(C∗1)≅Assume∖S(C1).

□

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

Claim: If C0≃C1 are Cartesian frames over W, then for all partitions V of W, ExternalV(C0)≃ExternalV(C1), External/V(C0)≃External/V(C1), InternalV(C0)≃InternalV(C1), and Internal/V(C0)≃Internal/V(C1).

Proof: Let Ci=(Ai,Ei,⋅i), and let (g0,h0):C0→C1 and (g1,h1):C1→C0 compose to something homotopic to the identity in both orders. Let V be a partition of W, and let v:W→V send each element w∈W to the part that contains it. Let Bi be the partition of Ai defined by Bi={{a′∈Ai | ∀e∈Ei, v(a′⋅e)=v(a⋅e)} | a∈Ai}. 

Let βi:Ai→Bi, send each element of Ai to its part in Bi, so βi(a)={a′∈Ai | ∀e∈Ei, v(a′⋅e)=v(a⋅e)}. Since βi is surjective, it has a right inverse. Let αi:Bi→Ai be any choice of right inverse to βi. This gives a pair of functions ιi:Bi→B1−i given by ιi=β1−i∘gi∘αi.

We start by showing that ι0 and ι1 are inverses, and thus bijections between B0 and B1. We do this by showing that βi∘g1−i∘gi=βi, and that ιi∘βi=β1−i∘gi , and thus we will have

ι1−i∘ιi=ι1−i∘β1−i∘gi∘αi=βi∘g1−i∘gi∘αi=βi∘αi,

which is the identity on Bi.

To see that βi∘g1−i∘gi=βi, observe that for all a∈Ai, we have that for all e∈Ei, v(a⋅ie)=v(g1−i(gi(a))⋅ie), so, βi(a)=βi(g1−i(gi(a))). Thus, βi=βi∘g1−i∘gi.

To see that ιi∘βi=β1−i∘gi, first observe that for all a∈Ai, we have that βi(αi(βi(a)))=βi(a), and thus, for all e∈E1−i,

v(gi(a)⋅1−ie)=v(a⋅ihi(e))=v(αi(βi(a))⋅ihi(e))=v(gi(αi(βi(a)))⋅1−ie).

Thus, β1−i(gi(a))=β1−i(gi(αi(βi(a)))). Thus, we have

β1−i∘gi=β1−i∘gi∘αi∘βi=ιi∘βi.

This also gives us functions fi:Ai/Bi→A1−i/B1−i, by fi(q)=gi∘q∘ι1−i. To ehow that these functions are well-defined, we need to show that for all q∈Ai/Bi,  fi(q) is in fact in A1−i/B1−i, by showing that for all b∈B1−i,  gi(q(ι1−i(b)))∈b, or equivalently that β1−i∘gi∘q∘ι1−i is the identity on B1−i. Since q∈Ai/Bi, we already have that βi∘q is the identity of Bi. Thus, we have that

β1−i∘gi∘q∘ι1−i=ιi∘βi∘q∘ι1−i=ιi∘ι1−i

is the identity on B1−i.

We are now ready to demonstrate that ExternalV(C0)≃ExternalV(C1).

Let ExternalV(Ci)=(Ai/Bi,Bi×Ei,⋆i), and define

(g′i,h′i):(Ai/Bi,Bi×Ei,⋆i)→(A1−i/B1−i,B1−i×E1−i,⋆1−i)

by g′i=fi, while h′i:B1−i×E1−i→Bi×Ei is given by h′i(b,e)=(ι1−i(b),hi(e)).

To see that (g′i,h′i) is a morphism, observe that for all q∈Ai/Bi, and (b,e)∈B1−i×E1−i, we have

g′i(q)⋆1−i(b,e)=fi(q)⋆1−i(b,e)=fi(q)(b)⋅1−ie=gi(q(ι1−i(b)))⋅1−ie=q(ι1−i(b))⋅ihi(e)=q⋆i(ι1−i(b),hi(e))=q⋆ih′i(b,e).

To see that (g′1−i,h′1−i)∘(g′i,h′i) is homotopic to the identity, we show that

(idAi/Bi,h′i∘h′1−i):(Ai/Bi,Bi×Ei,⋆i)→(Ai/Bi,Bi×Ei,⋆i)

is a morphism. Indeed, for all q∈Ai/Bi and (b,e)∈Bi×Ei,

q⋆ih′i(h′1−i(b,e))=q⋆i(b,hi(h1−i(e)))=q(b)⋅ihi(h1−i(e))=q(b)⋅ie=q⋆i(b,e).

Thus, ExternalV(C0)≃ExternalV(C1)

Similarly, let External/V(Ci)=(Bi,Ai/Bi×Ei,⋄i), and define

(g′′i,h′′i):(Bi,Ai/Bi×Ei,⋄i)→(B1−i,A1−i/B1−i×E1−i,⋄1−i)

by g′′i=ιi, and h′′i:A1−i/B1−i×E1−i→Ai/Bi×Ei is given by h′′i(q,e)=(f1−i(q),hi(e)).

To see that (g′′i,h′′i) is a morphism, observe that for all q∈Bi, and (q,e)∈A1−i/B1−i×E1−i, we have 

g′′i(b)⋄1−i(q,e)=ιi(b)⋄1−i(q,e)=q(ιi(b))⋅1−ie=q(ιi(b))⋅1−ih1−i(hi(e))=g1−i(q(ιi(b)))⋅ihi(e)=f1−i(q)(b)⋅ihi(e)=b⋄i(f1−i(q),hi(e))=b⋄ih′′i(q,e).

Clearly, (g′′1−i,h′′1−i)∘(g′′i,h′′i) is homotopic to the identity, since g′′1−i∘g′′i is the identity on Bi. Thus, External/V(C0)≃External/V(C1).

We know that InternalV(C0)≃InternalV(C1) and Internal/V(C0)≃Internal/V(C1), because

(InternalV(C0))∗≅ExternalV(C∗0)≃ExternalV(C∗1)≅InternalV(C1)

and

(Internal/V(C0))∗≅External/V(C∗0)≃External/V(C∗1)≅Internal/V(C1).

□

 

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

Claim: CommitS(C)≅1S⊸C and AssumeS(C)≅1S⊗C.

Proof: Let C=(A,E,⋅), and let 1S=({a},S,⋄). 

Let CommitS(C)=(B,E,⋆), where B={b∈A | ∀e∈e, b⋅e∈S}, and b⋆e=b⋅e. 

Let 1S⊸C=(hom(1S,C),{a}×E,∙), where

(g,h)∙(a,e)=g(a)⋅e=a⋄h(e)=h(e).

We construct an isomorphism (g0,h0):(1S⊸C)→CommitS(C), by defining g0:hom(1S,C)→B by g0(g,h)=g(a), and by defining h0:E→{a}×E by h0(e)=(a,e).

First, we need to show that g0 is a well-defined function into B. Observe that for all (g,h)∈hom(1S,C), and for all e∈E,

g0(g,h)⋅e=g(a)⋅e=h(e)

∈S, and so g0(g,h)∈B.

Next, we show that (g0,h0) is a morphism, by showing that for all (g,h)∈hom(1S,C) and e∈E,

g0(g,h)⋆e=g(a)⋆e=g(a)⋅e=a⋄h(e)=(g,h)∙(a,e)=(g,h)∙h0(e).

Finally, to show that (g0,h0), we need to show that g0 and h0 are bijections. Clearly, h0 is a bijection. To see that g0 is injective, observe that if g0(g,h)=g0(g′,h′), then g(a)=g′(a), so g=g′. Further, for all e∈E, 

h(e)=a⋄h(e)=g(a)⋅e=g′(a)⋅e=a⋄h′(e)=h′(e),

so h=h′. Thus g0 is injective. To see that g0 is surjective, observe that for all b∈B, there exists a morphism (gb,hb):1S→C, given by gb(a)=b, and hb(e)=b⋆e. This is a morphism because, for all a∈{a} and e∈E,

gb(a)⋆e=b⋆e=hb(e)=a⋄hb(e).

Since

g0(gb,hb)=gb(a)=b,

we have that g0 is surjective, and thus (g0,h0) is an isomorphism between 1S⊸C and CommitS(C).

To see that AssumeS(C)≅1S⊗C, observe that

AssumeS(C)≅CommitS(C∗)∗≅(1S→C∗)∗≅(1∗S⅋ C∗)∗≅1S⊗C.

□

Recall that we can think of 1S as a powerless agent that has been promised S. 1S⊗C, then, is a team consisting of Agent(C) alongside an agent that has been promised S.

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

CommitS(C)≅1S⊸C is less intuitive. 1S⊸C is "C with a hole in it shaped like a promise that S 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 S will happen.

It will sometimes be helpful to think about assuming and committing in terms of 1S, 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 W 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 C=(A,E,⋅) over W and subset S of W, CommitS(C)◃⊥S and AssumeS(C)◃⊥S.

Proof: Trivial. □

Claim: For any Cartesian frame C=(A,E,⋅) over W and subset S of W, with C◃⊥S, CommitS(C)≅AssumeS(C)≅C.

Proof: Trivial. □

Corollary: For any subset S of W, CommitS and AssumeS are idempotent.

Proof: Trivial. □

Claim: For any Cartesian frame C=(A,E,⋅) over W and subset S of W, if Commit∖S=(A′,E′,⋅′), then for all a′∈A′, there exists an e′∈E′ such that a′⋅′e′∉S.

Proof: Trivial. □

Claim: For any Cartesian frame C=(A,E,⋅) over W and subset S of W, if for all a∈A, there exists an e∈E such that a⋅e∉S, then Commit∖S(C)≅C.

Proof: Trivial. □

Corollary: For any subset S of W, Commit∖S is idempotent.

Proof: Trivial. □

Claim: For any Cartesian frame C=(A,E,⋅) over W and subset S of W, if Assume∖S(C)=(A′,E′,⋅′), then for all e′∈E′, there exists an a′∈A′ such that a′⋅′e′∉S.

Proof: Trivial. □

Claim: For any Cartesian frame C=(A,E,⋅) over W and subset S of W, if for all e∈E, there exists an a∈A such that a⋅e∉S, then Assume∖S(C)≅C.

Proof: Trivial. □

Corollary: For any subset S of W, Assume∖S(C) is idempotent.

Proof: Trivial. □

 

4.2. Externalizing

Claim: For any Cartesian frame C=(A,E,⋅) over W and partition V of W, let v:W→V send each element of W to its part in V. If ExternalV(C)=(A′,E′,⋅′), then A′ is nonempty and for all a′0,a′1∈A′ and e′∈E′, we have v(a′0⋅′e′)=v(a′1⋅′e′).

Proof: Let B be defined, as in the definition of ExternalV, as B={{a′∈A | ∀e∈E, v(a′⋅e)=v(a⋅e)} | a∈A}. A′ is A/B, the set of functions from B to A that sends each part in B to an element of that part, and E′=B×E. A′ is clearly nonempty. Consider an arbitrary a′0,a′1∈A′ and (e,b)∈E′. Since a′0(b),a′0(b)∈b are in the same part, we have that a′0(b)⋅e=a′0(b)⋅e, and thus v(a′0⋅′(b,e))=v(a′1⋅′(b,e)). □

Claim: For any Cartesian frame C=(A,E,⋅) over W and partition V of W, let v:W→V send each element of W to its part in V. If A is nonempty and for all a0,a1∈A and e∈E, we have v(a0⋅e)=v(a1⋅e), then ExternalV(C)≅C.

Proof: Let B be defined, as in the definition of ExternalV, as B={{a′∈A | ∀e∈E, v(a′⋅e)=v(a⋅e)} | a∈A}. If A is nonempty and for all a0,a1∈A and e∈E, we have v(a0⋅e)=v(a1⋅e), then B has only one part, B={A}. Thus, ExternalV(C)=(A/{A},{A}×E,⋆), where ⋆ is given by q⋆(A,e)=q(A)⋅e.

Let (g,h):ExternalV(C)→C be given by g(q)=q(A), and h(e)=(A,e). This is trivially a morphism, and both g and h are trivially bijections, so ExternalV(C)≅C.□

Corollary: For any partition V of W, ExternalV is idempotent.

Proof: Trivial. □

Claim: For any Cartesian frame C=(A,E,⋅) over W and partition V of W, let v:W→V send each element of W to its part in V. If External/V=(A′,E′,⋅′), then for all a′0≠a′1∈A′ there exists an e′∈E′, such that v(a′0⋅′e′)≠v(a′1⋅′e′).

Proof: Let B be defined once again as B={{a′∈A | ∀e∈E, v(a′⋅e)=v(a⋅e)} | a∈A}. A′=B and E′=A/B×E. Since A/B is clearly nonempty, fix any q∈A/B. Observe that if a′0≠a′1, then q(a′0) and q(a′1) are in different parts in B, so there exists an e∈E such that v(q(a′0)⋅e)≠v(q(a′1)⋅e). Thus v(a′0⋅′(q,e))≠v(a′1⋅′(q,e)). □

Claim: For any Cartesian frame C=(A,E,⋅) over W and partition V of W, let v:W→V send each element of W to its part in V. If for all a0≠a1∈A there exists an e∈E, such that v(a0⋅e)≠v(a1⋅e), then ExternalV(C)≅C.

Proof: Again, let B be defined again as B={{a′∈A | ∀e∈E, v(a′⋅e)=v(a⋅e)} | a∈A}. If for all a0≠a1∈A there exists an e∈E such that v(a0⋅e)≠v(a1⋅e), then every element of B is a singleton. Thus A/B={q} is a singleton, and q is a bijection.

External/V(C)=(B,{q}×E,⋆), where ⋆ is given by b⋆(q,e)=q(b)⋅e. Let (g,h):External/V(C)→C be given by g(b)=q(b), and h(e)=(q,e). This is trivially a morphism and both g and h are trivially bijections, so External/V(C)≅C. □

Corollary: For any partition V of W, External/V(C) 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 C=(A,E,⋅) over W and partition V of W, let v:W→V send each element of W to its part in V. If InternalV(C)=(A′,E′,⋅′), then E′ is nonempty and for all e′0,e′1∈E′ and a′∈A′, we have v(a′⋅′e′0)=v(a′⋅′e′1).

Proof: Trivial. □

Claim: For any Cartesian frame C=(A,E,⋅) over W and partition V of W, let v:W→V send each element of W to its part in V. If for all e0,e1∈E and a∈A we have v(a⋅e0)=v(a⋅e1), then InternalV(C)≅C.

Proof: Trivial. □

Corollary: For any partition V of W, InternalV(C) is idempotent.

Proof: Trivial. □

Claim: For any Cartesian frame C=(A,E,⋅) over W and partition V of W, let v:W→V send each element of W to its part in V. If Internal/V(C)=(A′,E′,⋅′), then for all e′0≠e′1∈E′ there exists an a′∈A′, such that v(a′⋅′e′0)≠v(a′⋅′e′0).

Proof: Trivial. □

Claim: For any Cartesian frame C=(A,E,⋅) over W and partition V of W, let v:W→V send each element of W to its part in V. If for all e0≠e1∈A there exists an a∈A, such that v(a⋅e0)≠v(a⋅e1), then InternalV(C)≅C.

Proof: Trivial. □

Corollary: For any partition V of W, Internal/V(C) 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 1S as it relates to multiplicative operations. The additive role of 1S is quite different from this, and quite varied. There isn't a single interpretation for 1S in additive contexts, beyond the basic interpretation we provided in "Biextensional Equivalence" that 1S is "a powerless, all-knowing agent... plus a promise from the environment that the world will be in S." ↩