Committing, Assuming, Externalizing, and Internalizing

post by Scott Garrabrant · 2020-11-09T16:59:01.525Z · LW · GW · 25 comments

Contents

  1. Definitions from Agents and Environments
    1.1. Committing
    1.2. Assuming
    1.3. Externalizing
    1.4. Internalizing
  2. Definitions from Worlds
    2.1. Committing
    2.2. Assuming
    2.3. Externalizing
    2.4. Internalizing
  3. Basic Properties
    3.1. Biextensional Equivalence
    3.2. Committing and Assuming Can Be Defined Using Lollipop and Tensor
  4. Idempotence
    4.1. Committing and Assuming
    4.2. Externalizing
    4.3. Internalizing
  Footnotes
None
25 comments

This is the tenth post in the Cartesian frames [LW · GW] 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,\cdot )$.

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\subseteq A$, let ${\text{Commit}}^B\left(C\right)$ denote the Cartesian frame $(B,E,\star )$, with $\star$ given by $b\star e=b\cdot e$. Let ${\text{Commit}}^{\setminus B}\left(C\right)$ denote the Cartesian frame $(A\setminus B,E,\diamond )$, with $\diamond$ given by $a\diamond e=a\cdot e$.

${\text{Commit}}^B\left(C\right)$ represents the perspective you get when the agent of $C$ makes a commitment to choose an element of $B$, while ${\text{Commit}}^{\setminus B}\left(C\right)$ represents the perspective you get when the agent of $C$ makes a commitment to choose an element outside of $B$.

Claim: For all $B\subseteq A$, ${\text{Commit}}^B\left(C\right){◃}_{+}C$ and ${\text{Commit}}^{\setminus B}\left(C\right){◃}_{+}C$. Further, ${\text{Commit}}^{\setminus B}\left(C\right)$ and ${\text{Commit}}^B\left(C\right)$ are brothers [LW · GW] in $C$.

Proof: That ${\text{Commit}}^B\left(C\right){◃}_{+}C$ and ${\text{Commit}}^{\setminus B}\left(C\right){◃}_{+}C$ is trivial from the committing definition of additive subagent [LW · GW].

Observe that ${\text{Commit}}^B\left(C\right)\oplus {\text{Commit}}^{\setminus B}\left(C\right)=(A,E\times E,\bullet )$, where $\bullet$ is given by $a\bullet (e,f)=a\cdot e$ if $a\in B$, and $a\bullet (e,f)=a\cdot f$ if $a\notin B$. Let $D\subset E\times E$ be the diagonal, $\left\{\right(e,e)|e\in E\}$. We clearly have that $(A,D,{\bullet }^{\prime })$ is in ${\text{Commit}}^B\left(C\right)⊞{\text{Commit}}^{\setminus B}\left(C\right)$, where ${\bullet }^{\prime }$ is the restriction of $\bullet$ to $A\times D$, and that $(A,D,{\bullet }^{\prime })\cong C$; so ${\text{Commit}}^{\setminus B}\left(C\right){◃}_{+}C$ and ${\text{Commit}}^B\left(C\right){◃}_{+}C$ are brothers in $C$. $\square$

Claim: ${\text{Commit}}^{\setminus B}\left(C\right)\cong {\text{Commit}}^{A\setminus B}\left(C\right)$

Proof: Trivial. $\square$

 

1.2. Assuming

Assuming is the dual operation to committing.

Definition: Given a subset $F\subseteq E$, let ${\text{Assume}}^F\left(C\right)$ denote the Cartesian frame $(A,F,\star )$, with $\star$ given by $a\star f=a\cdot f$. Let ${\text{Assume}}^{\setminus F}\left(C\right)$ denote the Cartesian frame $(A,E\setminus F,\diamond )$, with $\diamond$ given by $a\diamond e=a\cdot e$.

${\text{Assume}}^F\left(C\right)$ represents the perspective you get when you assume the environment is chosen from $F$, while ${\text{Assume}}^{\setminus F}\left(C\right)$ 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 [LW · GW]), I noted the counter-intuitive result that agents have no control in worlds where a meteor (or other event) could have prevented their existence:

$C_0=\begin{array}{cc}& \begin{array}{ccc}r& s& m\end{array}\\ \begin{array}{c}u\\ n\\ u\leftrightarrow r\\ u\leftrightarrow s\end{array}& \left(\begin{array}{ccc}ur& us& m\\ nr& ns& m\\ ur& ns& m\\ nr& us& m\end{array}\right)\end{array}$.

Here, we see that we can use ${\text{Assume}}^{\setminus F}\left(C\right)$ 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:

${\text{Assume}}^{\setminus \left\{m\right\}}\left(C_0\right)=\begin{array}{cc}& \begin{array}{cc}r& s\end{array}\\ \begin{array}{c}u\\ n\\ u\leftrightarrow r\\ u\leftrightarrow s\end{array}& \left(\begin{array}{cc}ur& us\\ nr& ns\\ ur& ns\\ nr& us\end{array}\right)\end{array}$.

Claim: For all $F\subseteq E$, $\left({\text{Assume}}^F\right(C){)}^{\ast }\cong {\text{Commit}}^F(C^{\ast })$ and $\left({\text{Assume}}^{\setminus F}\right(C){)}^{\ast }\cong {\text{Commit}}^{\setminus F}(C^{\ast })$. Similarly, for all $B\subseteq A$, $\left({\text{Commit}}^B\right(C){)}^{\ast }\cong {\text{Assume}}^B(C^{\ast })$ and $\left({\text{Commit}}^{\setminus B}\right(C){)}^{\ast }\cong {\text{Assume}}^{\setminus B}(C^{\ast })$.

Proof: Trivial. $\square$

Claim: For all $F\subseteq E$, $C{◃}_{+}^{\ast }{\text{Assume}}^F\left(C\right)$ and $C{◃}_{+}^{\ast }{\text{Assume}}^{\setminus F}\left(C\right)$. 

Proof: Trivial. $\square$

 

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\in Y$, there exists a unique $x\in X$ such that $y\in 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\left(x\right)\in x$ for all $x\in X$.

Definition: Given a partition $B$ of $A$, let ${\text{External}}^B\left(C\right)$ denote the Cartesian Frame $(A/B,B\times E,\star )$, where $\star$ is given by $q\star (b,e)=q\left(b\right)\cdot e$. Let ${\text{External}}^{/B}\left(C\right)$ denote the Cartesian Frame $(B,A/B\times E,\diamond )$, where $\diamond$ is given by $b\diamond (q,e)=q\left(b\right)\cdot e$.

We say "externalizing $B$" for ${\text{External}}^B$ and "externalizing mod $B$" for ${\text{External}}^{/B}$.

${\text{External}}^B\left(C\right)$ 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, ${\text{External}}^{/B}\left(C\right)$ 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$, ${\text{External}}^B\left(C\right){◃}_{\times }C$ and ${\text{External}}^{/B}\left(C\right){◃}_{\times }C$. Further, ${\text{External}}^B\left(C\right)$ and ${\text{External}}^{/B}\left(C\right)$ are sisters [LW · GW] in $C$.

Proof: Let ${\text{External}}^B\left(C\right)=(A/B,B\times E,\star )$ and ${\text{External}}^{/B}\left(C\right)=(B,A/B\times E,\diamond )$.

First, observe that for every $e\in E$, there exists a morphism $(g_e,h_e):{\text{External}}^B\left(C\right)\to \left({\text{External}}^{/B}\right(C){)}^{\ast }$, with $g_e:\to A/B\times E$ given by $g_e\left(q\right)=(q,e)$, and $h_e:B\to B\times E$ given by $h_e\left(b\right)=(b,e)$. To see that this is a morphism, observe that for all $q\in A/B$ and $b\in B$,

$$\begin{array}{cc}{g}_e\left(q\right)\diamond b& =q\left(b\right)\cdot e\\ & =q\star h_e\left(b\right).\end{array}$$

Let $E^{\prime }\subseteq \text{hom}\left({\text{External}}^B\right(C),({\text{External}}^{/B}\left(C\right){)}^{\ast })$ be given by $E^{\prime }=\left\{\right(g_e,h_e)|e\in E\}$, and let $D=(A/B\times B,E^{\prime },\bullet )$, where

$$\begin{array}{cc}(q,b)\bullet (g_e,h_e)& =g_e\left(q\right)\diamond b\\ & =q\star h_e\left(b\right)\\ & =q\left(b\right)\cdot e.\end{array}$$

Our goal is to show that $D\in {\text{External}}^B\left(C\right)⊠{\text{External}}^{/B}\left(C\right)$, and that $D\simeq C$.

To see $D\simeq C$, we define $(g_0,h_0):D\to C$ and $(g_1,h_1):C\to D$ as follows.

First, $g_0:A/p\times B\to A$ is given by $g_0(q,b)=q\left(b\right)$. We first need to confirm that $g_0$ is surjective. Given any $a\in A$, we can let $b\in B$ be the set with $a\in b$ and construct a function $q\in A/B$ by saying $q\left(b\right)=a$, and for each $b^{\prime }\ne b$, choosing an $a^{\prime }\in b^{\prime }$, and saying $q\left(b^{\prime }\right)=a^{\prime }$. Observing that $g_0(q,b)=a$, we have that $g_0$ is surjective and thus has a right inverse.

We choose $g_1:A\to A/B\times B$ to be any right inverse to $g_0$. Similarly, we define $h_0:E\to E^{\prime }$ by $h_0\left(e\right)=(g_e,h_e)$, which is clearly surjective, and define $h_1:E^{\prime }\to E$ to be any right inverse to $h_0$. (Indeed, $h_0$ is bijective as long as $A$ is nonempty.)

Then, for all $(q,b)\in A/B\times B$ and $e\in E$, we have

$$\begin{array}{cc}{g}_0(q,b)\cdot e& =q\left(b\right)\cdot e\\ & =(q,b)\bullet (g_e,h_e)\\ & =q,b\bullet h_0\left(e\right),\end{array}$$

so $(g_0,h_0)$ is a morphism. This also gives us that for all $a\in A$ and $e^{\prime }\in E^{\prime }$ we have

$$\begin{array}{cc}{g}_1\left(a\right)\bullet e^{\prime }& =g_1\left(a\right)\bullet h_0\left(h_1\right(e^{\prime }\left)\right)\\ & =g_0\left(g_1\right(a\left)\right)\cdot h_1\left(e\right)\\ & =a\cdot h_1\left(e\right),\end{array}$$

so $(g_1,h_1)$ is a morphism. We know $(g_0,h_0)\circ (g_1,h_1)$ is homotopic to the identity on $C$, since $g_0\circ g_1$ is the identity on $A$, and we know that $(g_1,h_1)\circ (g_0,h_0)$ is homotopic to the identity on $D$, since $h_0\circ h_1$ is the identity on $E^{\prime }$. Thus, $D\simeq C$.

To show that $D\in {\text{External}}^B\left(C\right)⊠{\text{External}}^{/B}\left(C\right)$, it suffices to show that

$$\begin{array}{cc}{\text{External}}^B\left(C\right)& =(A/B,B\times E,\star )\\ & \simeq (A/B,B\times E^{\prime },{\star }^{\prime }),\end{array}$$

and

$$\begin{array}{cc}{\text{External}}^{/B}\left(C\right)& =(B,A/B\times E,\diamond )\\ & \simeq (B,A/B\times E^{\prime },{\diamond }^{\prime }),\end{array}$$

where ${\star }^{\prime }$ and ${\diamond }^{\prime }$ are given by

$$\begin{array}{cc}q{\star }^{\prime }(b,(g_e,h_e\left)\right)& =b{\diamond }^{\prime }(q,(g_e,h_e\left)\right)\\ & =q\star h_e\left(b\right)\\ & =b\diamond g_e\left(q\right)\\ & =q\left(b\right)\cdot e.\end{array}$$

Indeed, we show that if $A$ is nonempty, $(A/B,B\times E,\star )\cong (A/B,B\times E^{\prime },{\star }^{\prime })$, and $(B,A/B\times E,\diamond )\cong (B,A/B\times E^{\prime },{\diamond }^{\prime })$.

If $A$ is nonempty, then the function from $E$ to $E^{\prime }$ given by $e\mapsto (g_e,h_e)$ is a bijection, since it is clearly surjective, and is injective because $e$ is uniquely defined by $g_e\left(a\right)=(a,e)$. This gives a bijection between $B\times E$ and $B\times E^{\prime }$, and we have that for all $q\in A/B$, $b\in B$, and $e\in E$,

$$\begin{array}{cc}q{\star }^{\prime }(b,(g_e,h_e\left)\right)& =q\left(b\right)\cdot e\\ & =q\star (b,e).\end{array}$$

Similarly, we have a bijection between $A/B\times E$ and $A/B\times E^{\prime }$, and for all $q\in A/B$, $b\in B$, and $e\in E$,

$$\begin{array}{cc}b{\diamond }^{\prime }(q,(g_e,h_e\left)\right)& =q\left(b\right)\cdot e\\ & =b\diamond (q,e).\end{array}$$

If $A$ is empty, then $B$ is empty, and $A/p$ is a singleton empty function, so $(A/B,B\times E,\star )\simeq (A/B,B\times E^{\prime },{\star }^{\prime })\simeq \top$, and we either have $(B,A/B\times E,\diamond )\simeq (B,A/B\times E^{\prime },{\diamond }^{\prime })\simeq 0$ or $(B,A/B\times E,\diamond )\simeq (B,A/B\times E^{\prime },{\diamond }^{\prime })\simeq \text{null}$, depending on whether or not $E$ is empty.

Thus, $D\in {\text{External}}^B\left(C\right)⊠{\text{External}}^{/B}\left(C\right)$, so ${\text{External}}^B\left(C\right)$ and ${\text{External}}^{/B}\left(C\right)$ are sisters in $C$. $\square$

 

1.4. Internalizing

Definition: Given a partition $F$ of $E$, let ${\text{Internal}}^F\left(C\right)$ denote the Cartesian Frame $(F\times A,E/F,\star )$, where $\star$ is given by $(f,a)\star q=a\cdot q\left(f\right)$. Let  ${\text{Internal}}^{/F}\left(C\right)$ denote the Cartesian Frame $(E/F\times A,F,\diamond )$, where $\diamond$ is given by $(q,a)\diamond f=a\cdot q\left(f\right)$. 

We say "internalizing $p$" for ${\text{Internal}}^p$ and "internalizing mod $p$" for ${\text{Internal}}^{/p}$.

Claim: For all partitions $F$ of $E$, $\left({\text{Internal}}^F\right(C){)}^{\ast }\cong {\text{External}}^F(C^{\ast })$ and $\left({\text{Internal}}^{/F}\right(C){)}^{\ast }\cong {\text{External}}^{/F}(C^{\ast })$. Similarly, for all partitions $B$ of $A$, $\left({\text{External}}^B\right(C){)}^{\ast }\cong {\text{Internal}}^B(C^{\ast })$ and $\left({\text{External}}^{/B}\right(C){)}^{\ast }\cong {\text{Internal}}^{/B}(C^{\ast })$. 

Proof: Trivial. $\square$

Claim: For all partitions $F$ of $E$, $C{◃}_{\times }{\text{Internal}}^F\left(C\right)$ and $C{◃}_{\times }{\text{Internal}}^{/F}\left(C\right)$.

Proof: This follows from the fact that $\left({\text{Internal}}^F\right(C){)}^{\ast }\cong {\text{External}}^F(C^{\ast }){◃}_{\times }{C}^{\ast }$ and $\left({\text{Internal}}^{/F}\right(C){)}^{\ast }\cong {\text{External}}^{/F}(C^{\ast }){◃}_{\times }{C}^{\ast }$, and the fact that multiplicative subagent is equivalent to multiplicative sub-environment. $\square$

 

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\subseteq W$, we define ${\text{Commit}}_S\left(C\right)={\text{Commit}}^B\left(C\right)$ and ${\text{Commit}}_{\setminus S}\left(C\right)={\text{Commit}}^{\setminus B}\left(C\right)$, where $B\subseteq A$ is given by $B=\{a\in A|\forall e\in E,a\cdot e\in S\}$.

Claim: For all $S\subseteq W$, ${\text{Commit}}_S\left(C\right){◃}_{+}C$ and ${\text{Commit}}_{\setminus S}\left(C\right){◃}_{+}C$. Further, ${\text{Commit}}_{\setminus S}\left(C\right)$ and ${\text{Commit}}_S\left(C\right)$ are brothers in $C$.

Proof: Trivial. $\square$

Unlike before, it is not necessarily the case that ${\text{Commit}}_{\setminus S}\left(C\right)\cong {\text{Commit}}_{W\setminus S}\left(C\right)$. This is because there might be rows that contains both elements of $S$ and elements of $W\setminus S$.

 

2.2. Assuming

Definition: Given $S\subseteq W$, we define ${\text{Assume}}_S\left(C\right)={\text{Assume}}^F\left(C\right)$ and ${\text{Assume}}_{\setminus S}\left(C\right)={\text{Assume}}^{\setminus F}\left(C\right)$, where $F\subseteq E$ is given by $F=\{e\in E|\forall a\in A,a\cdot e\in S\}.$

Claim: For all $S\subseteq W$, $\left({\text{Assume}}_S\right(C){)}^{\ast }\cong {\text{Commit}}_S(C^{\ast })$ and $\left({\text{Assume}}_{\setminus S}\right(C){)}^{\ast }\cong {\text{Commit}}_{\setminus S}(C^{\ast })$, $\left({\text{Commit}}_S\right(C){)}^{\ast }\cong {\text{Assume}}_S(C^{\ast })$ and $\left({\text{Commit}}_{\setminus S}\right(C){)}^{\ast }\cong {\text{Assume}}_{\setminus S}(C^{\ast })$.

Proof: Trivial. $\square$

Claim: For all $S\subseteq W$, $C{◃}_{+}^{\ast }{\text{Assume}}_S\left(C\right)$ and $C{◃}_{+}^{\ast }{\text{Assume}}_{\setminus S}\left(C\right)$.

Proof: Trivial. $\square$

 

2.3. Externalizing

Definition: Given a partition $V$ of $W$, let $v:W\to V$ send each element $w\in W$ to the part that contains it. We define ${\text{External}}_V\left(C\right)={\text{External}}^B\left(C\right)$ and ${\text{External}}_{/V}\left(C\right)={\text{External}}^{/B}\left(C\right)$, where $B=\left\{\right\{a^{\prime }\in A|\forall e\in E,v(a^{\prime }\cdot e)=v(a\cdot e)\}|a\in A\}$.

Claim: For all partitions $V$ of $W$, ${\text{External}}_V\left(C\right){◃}_{\times }C$ and ${\text{External}}_{/V}\left(C\right){◃}_{\times }C$. Further, ${\text{External}}_V\left(C\right)$ and ${\text{External}}_{/V}\left(C\right)$ are sisters in $C$.

Proof: Trivial. $\square$

 

2.4. Internalizing

Definition: Given a partition $V$ of $W$, let $v:W\to V$ send each element $w\in W$ to the part that contains it. We define ${\text{Internal}}_V\left(C\right)={\text{Internal}}^F\left(C\right)$ and ${\text{Internal}}_{/V}\left(C\right)={\text{Internal}}^{/F}\left(C\right)$, where $F=\left\{\right\{e^{\prime }\in E|\forall a\in a,v(a\cdot e^{\prime })=v(a\cdot e)\}|e\in E\}$.

Claim: For all partitions $V$ of $W$, $C{◃}_{\times }{\text{Internal}}_V\left(C\right)$ and $C{◃}_{\times }{\text{Internal}}_{/V}\left(C\right)$. 

Proof: Trivial. $\square$

Claim: For all partitions $V$ of $W$, $\left({\text{Internal}}_V\right(C){)}^{\ast }\cong {\text{External}}_V(C^{\ast })$, $\left({\text{Internal}}_{/V}\right(C){)}^{\ast }\cong {\text{External}}_{/V}(C^{\ast })$, $\left({\text{External}}_V\right(C){)}^{\ast }\cong {\text{Internal}}_V(C^{\ast })$, and $\left({\text{External}}_{/V}\right(C){)}^{\ast }\cong {\text{Internal}}_{/V}(C^{\ast })$. 

Proof: Trivial. $\square$

 

3. Basic Properties

3.1. Biextensional Equivalence

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

Claim: If $C_0\simeq C_1$ are Cartesian frames over $W$, then for any subset $S\subseteq W$, ${\text{Commit}}_S\left(C_0\right)\simeq {\text{Commit}}_S\left(C_1\right)$, ${\text{Commit}}_{\setminus S}\left(C_0\right)\simeq {\text{Commit}}_{\setminus S}\left(C_1\right)$,${\text{Assume}}_S\left(C_0\right)\simeq {\text{Assume}}_S\left(C_1\right)$, and ${\text{Assume}}_{\setminus S}\left(C_0\right)\simeq {\text{Assume}}_{\setminus S}\left(C_1\right)$.

Proof: Let $C_i=(A_i,E_i,{\cdot }_i)$, and let $(g_0,h_0):C_0\to C_1$ and $(g_1,h_1):C_1\to C_0$ compose to something homotopic to the identity in both orders. Let $B_i\subset A_i$ be defined by $B_i=\{a\in A_i|\forall e\in E_i,a{\cdot }_{i}e\in S\}$.

Observe that if $b\in B_0$, then for all $e\in E_1$, $g_0\left(b\right){\cdot }_{1}e=b{\cdot }_0{h}_0\left(e\right)\in S$, so $g_0\left(b\right)\in B_1$. Similarly, if $b\in B_1$, then $g_1\left(b\right)\in B_0$. Thus, if we let $g_i^{\prime }:B_i\to B_{1-i}$ be given by $g_i^{\prime }\left(b\right)=g_i\left(b\right)$, we get morphisms $(g_i^{\prime },h_i):{\text{Commit}}_S\left(C_i\right)\to {\text{Commit}}_S\left(C_{1-i}\right)$, which are clearly morphisms, since they are restrictions of our original morphisms $(g_i,h_i)$.

Since $(g_0,h_0)$ and $(g_1,h_1)$ compose to something homotopic to the identity in both orders, $({\text{id}}_{A_i},h_{1-i}\circ h_i):C_i\to C_i$ is a morphism, so $({\text{id}}_{B_i},h_{1-i}\circ h_i):{\text{Commit}}_S\left(C_i\right)\to {\text{Commit}}_S\left(C_i\right)$ is a morphism, so $(g_0^{\prime },h_0)$ and $(g_1^{\prime },h_1)$ compose to something homotopic to the identity in both orders. Thus ${\text{Commit}}_S\left(C_0\right)\simeq {\text{Commit}}_S\left(C_1\right)$.

Similarly, if $b\in A_0\setminus B_0$, then there exists an $e\in E_0$ such that $b{\cdot }_{0}e\notin S$. But then

$$\begin{array}{cc}{g}_0\left(b\right){\cdot }_1{h}_1\left(e\right)& =g_1\left(g_0\right(b\left)\right){\cdot }_{0}e\\ & =b{\cdot }_{0}e\end{array}$$

$\notin S$, so $g_0\left(b\right)\in A_1\setminus B_1$. Similarly, if $b\in A_1\setminus B_1$, then $g_1\left(b\right)\in A_0\setminus B_0$. Thus, if we let $g_i^{\prime \prime }:A_i\setminus B_i\to A_{1-i}\setminus B_{1-i}$ be given by $g_i^{\prime \prime }\left(b\right)=g_i\left(b\right)$, we get morphisms $(g_i^{\prime \prime },h_i):{\text{Commit}}_{\setminus S}\left(C_i\right)\to {\text{Commit}}_{\setminus S}\left(C_{1-i}\right)$, which (similarly to above) compose to something homotopic to the identity in both orders. Thus, ${\text{Commit}}_{\setminus S}\left(C_0\right)\simeq {\text{Commit}}_{\setminus S}\left(C_1\right)$.

We know that ${\text{Assume}}_S\left(C_0\right)\simeq {\text{Assume}}_S\left(C_1\right)$ and ${\text{Assume}}_{\setminus S}\left(C_0\right)\simeq {\text{Assume}}_{\setminus S}\left(C_1\right)$, because

$$\begin{array}{cc}\left({\text{Assume}}_S\right(C_0){)}^{\ast }& \cong {\text{Commit}}_S\left(C_0^{\ast }\right)\\ & \simeq {\text{Commit}}_S\left(C_1^{\ast }\right)\\ & \cong {\text{Assume}}_S\left(C_1\right)\end{array}$$

and

$$\begin{array}{cc}\left({\text{Assume}}_{\setminus S}\right(C_0){)}^{\ast }& \cong {\text{Commit}}_{\setminus S}\left(C_0^{\ast }\right)\\ & \simeq {\text{Commit}}_{\setminus S}\left(C_1^{\ast }\right)\\ & \cong {\text{Assume}}_{\setminus S}\left(C_1\right).\end{array}$$

$\square$

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

Claim: If $C_0\simeq C_1$ are Cartesian frames over $W$, then for all partitions $V$ of $W$, ${\text{External}}_V\left(C_0\right)\simeq {\text{External}}_V\left(C_1\right)$, ${\text{External}}_{/V}\left(C_0\right)\simeq {\text{External}}_{/V}\left(C_1\right)$, ${\text{Internal}}_V\left(C_0\right)\simeq {\text{Internal}}_V\left(C_1\right)$, and ${\text{Internal}}_{/V}\left(C_0\right)\simeq {\text{Internal}}_{/V}\left(C_1\right)$.

Proof: Let $C_i=(A_i,E_i,{\cdot }_i)$, and let $(g_0,h_0):C_0\to C_1$ and $(g_1,h_1):C_1\to C_0$ compose to something homotopic to the identity in both orders. Let $V$ be a partition of W, and let $v:W\to V$ send each element $w\in W$ to the part that contains it. Let $B_i$ be the partition of $A_i$ defined by $B_i=\left\{\right\{a^{\prime }\in A_i|\forall e\in E_i,v(a^{\prime }\cdot e)=v(a\cdot e)\}|a\in A_i\}$. 

Let ${\beta }_i:A_i\to B_i$, send each element of $A_i$ to its part in $B_i$, so ${\beta }_i\left(a\right)=\{a^{\prime }\in A_i|\forall e\in E_i,v(a^{\prime }\cdot e)=v(a\cdot e\left)\right\}$. Since ${\beta }_i$ is surjective, it has a right inverse. Let ${\alpha }_i:B_i\to A_i$ be any choice of right inverse to ${\beta }_i$. This gives a pair of functions ${\iota }_i:B_i\to B_{1-i}$ given by ${\iota }_i={\beta }_{1-i}\circ g_i\circ {\alpha }_i$.

We start by showing that ${\iota }_0$ and ${\iota }_1$ are inverses, and thus bijections between $B_0$ and $B_1$. We do this by showing that ${\beta }_i\circ g_{1-i}\circ g_i={\beta }_i$, and that ${\iota }_i\circ {\beta }_i={\beta }_{1-i}\circ g_i$ , and thus we will have

$$\begin{array}{cc}{\iota }_{1-i}\circ {\iota }_i& ={\iota }_{1-i}\circ {\beta }_{1-i}\circ g_i\circ {\alpha }_i\\ & ={\beta }_i\circ g_{1-i}\circ g_i\circ {\alpha }_i\\ & ={\beta }_i\circ {\alpha }_i,\end{array}$$

which is the identity on $B_i$.

To see that ${\beta }_i\circ g_{1-i}\circ g_i={\beta }_i$, observe that for all $a\in A_i$, we have that for all $e\in E_i$, $v\left(a{\cdot }_{i}e\right)=v\left(g_{1-i}\right(g_i\left(a\right)\left){\cdot }_{i}e\right)$, so, ${\beta }_i\left(a\right)={\beta }_i\left(g_{1-i}\right(g_i\left(a\right)\left)\right)$. Thus, ${\beta }_i={\beta }_i\circ g_{1-i}\circ g_i$.

To see that ${\iota }_i\circ {\beta }_i={\beta }_{1-i}\circ g_i$, first observe that for all $a\in A_i$, we have that ${\beta }_i\left({\alpha }_i\right({\beta }_i\left(a\right)\left)\right)={\beta }_i\left(a\right)$, and thus, for all $e\in E_{1-i}$,

$$\begin{array}{cc}v\left(g_i\right(a\left){\cdot }_{1-i}e\right)& =v\left(a{\cdot }_i{h}_i\right(e\left)\right)\\ & =v\left({\alpha }_i\right({\beta }_i\left(a\right)\left){\cdot }_i{h}_i\right(e\left)\right)\\ & =v\left(g_i\right({\alpha }_i\left({\beta }_i\right(a\left)\right)\left){\cdot }_{1-i}e\right).\end{array}$$

Thus, ${\beta }_{1-i}\left(g_i\right(a\left)\right)={\beta }_{1-i}\left(g_i\right({\alpha }_i\left({\beta }_i\right(a\left)\right)\left)\right)$. Thus, we have

$$\begin{array}{cc}{\beta }_{1-i}\circ g_i& ={\beta }_{1-i}\circ g_i\circ {\alpha }_i\circ {\beta }_i\\ & ={\iota }_i\circ {\beta }_i.\end{array}$$

This also gives us functions $f_i:A_i/B_i\to A_{1-i}/B_{1-i}$, by $f_i\left(q\right)=g_i\circ q\circ {\iota }_{1-i}$. To ehow that these functions are well-defined, we need to show that for all $q\in A_i/B_i$,  $f_i\left(q\right)$ is in fact in $A_{1-i}/B_{1-i}$, by showing that for all $b\in B_{1-i}$,  $g_i\left(q\right({\iota }_{1-i}\left(b\right)\left)\right)\in b$, or equivalently that ${\beta }_{1-i}\circ g_i\circ q\circ {\iota }_{1-i}$ is the identity on $B_{1-i}$. Since $q\in A_i/B_i$, we already have that ${\beta }_i\circ q$ is the identity of $B_i$. Thus, we have that

$$\begin{array}{cc}{\beta }_{1-i}\circ g_i\circ q\circ {\iota }_{1-i}& ={\iota }_i\circ {\beta }_i\circ q\circ {\iota }_{1-i}\\ & ={\iota }_i\circ {\iota }_{1-i}\end{array}$$

is the identity on $B_{1-i}$.

We are now ready to demonstrate that ${\text{External}}_V\left(C_0\right)\simeq {\text{External}}_V\left(C_1\right)$.

Let ${\text{External}}_V\left(C_i\right)=(A_i/B_i,B_i\times E_i,{\star }_i)$, and define

$$(g_i^{\prime },h_i^{\prime }):(A_i/B_i,B_i\times E_i,{\star }_i)\to (A_{1-i}/B_{1-i},B_{1-i}\times E_{1-i},{\star }_{1-i})$$

by $g_i^{\prime }=f_i$, while $h_i^{\prime }:B_{1-i}\times E_{1-i}\to B_i\times E_i$ is given by $h_i^{\prime }(b,e)=\left({\iota }_{1-i}\right(b),h_i(e\left)\right)$.

To see that $(g_i^{\prime },h_i^{\prime })$ is a morphism, observe that for all $q\in A_i/B_i$, and $(b,e)\in B_{1-i}\times E_{1-i}\text{,}$ we have

$$\begin{array}{cc}{g}_i^{\prime }\left(q\right){\star }_{1-i}(b,e)& =f_i\left(q\right){\star }_{1-i}(b,e)\\ & =f_i\left(q\right)\left(b\right){\cdot }_{1-i}e\\ & =g_i\left(q\right({\iota }_{1-i}\left(b\right)\left)\right){\cdot }_{1-i}e\\ & =q\left({\iota }_{1-i}\right(b\left)\right){\cdot }_i{h}_i\left(e\right)\\ & =q{\star }_i\left({\iota }_{1-i}\right(b),h_i(e\left)\right)\\ & =q{\star }_i{h}_i^{\prime }(b,e).\end{array}$$

To see that $(g_{1-i}^{\prime },h_{1-i}^{\prime })\circ (g_i^{\prime },h_i^{\prime })$ is homotopic to the identity, we show that

$$({\text{id}}_{A_i/B_i},h_i^{\prime }\circ h_{1-i}^{\prime }):(A_i/B_i,B_i\times E_i,{\star }_i)\to (A_i/B_i,B_i\times E_i,{\star }_i)$$

is a morphism. Indeed, for all $q\in A_i/B_i$ and $(b,e)\in B_i\times E_i$,

$$\begin{array}{cc}q{\star }_i{h}_i^{\prime }\left(h_{1-i}^{\prime }\right(b,e\left)\right)& =q{\star }_i(b,h_i(h_{1-i}\left(e\right)\left)\right)\\ & =q\left(b\right){\cdot }_i{h}_i\left(h_{1-i}\right(e\left)\right)\\ & =q\left(b\right){\cdot }_{i}e=q{\star }_i(b,e).\end{array}$$

Thus, ${\text{External}}_V\left(C_0\right)\simeq {\text{External}}_V\left(C_1\right)$

Similarly, let ${\text{External}}_{/V}\left(C_i\right)=(B_i,A_i/B_i\times E_i,{\diamond }_i)$, and define

$$(g_i^{\prime \prime },h_i^{\prime \prime }):(B_i,A_i/B_i\times E_i,{\diamond }_i)\to (B_{1-i},A_{1-i}/B_{1-i}\times E_{1-i},{\diamond }_{1-i})$$

by $g_i^{\prime \prime }={\iota }_i$, and $h_i^{\prime \prime }:A_{1-i}/B_{1-i}\times E_{1-i}\to A_i/B_i\times E_i$ is given by $h_i^{\prime \prime }(q,e)=\left(f_{1-i}\right(q),h_i(e\left)\right)$.

To see that $(g_i^{\prime \prime },h_i^{\prime \prime })$ is a morphism, observe that for all $q\in B_i$, and $(q,e)\in A_{1-i}/B_{1-i}\times E_{1-i}$, we have 

$$\begin{array}{cc}{g}_i^{\prime \prime }\left(b\right){\diamond }_{1-i}(q,e)& ={\iota }_i\left(b\right){\diamond }_{1-i}(q,e)\\ & =q\left({\iota }_i\right(b\left)\right){\cdot }_{1-i}e\\ & =q\left({\iota }_i\right(b\left)\right){\cdot }_{1-i}{h}_{1-i}\left(h_i\right(e\left)\right)\\ & =g_{1-i}\left(q\right({\iota }_i\left(b\right)\left)\right){\cdot }_i{h}_i\left(e\right)\\ & =f_{1-i}\left(q\right)\left(b\right){\cdot }_i{h}_i\left(e\right)\\ & =b{\diamond }_i\left(f_{1-i}\right(q),h_i(e\left)\right)\\ & =b{\diamond }_i{h}_i^{\prime \prime }(q,e).\end{array}$$

Clearly, $(g_{1-i}^{\prime \prime },h_{1-i}^{\prime \prime })\circ (g_i^{\prime \prime },h_i^{\prime \prime })$ is homotopic to the identity, since $g_{1-i}^{\prime \prime }\circ g_i^{\prime \prime }$ is the identity on $B_i$. Thus, ${\text{External}}_{/V}\left(C_0\right)\simeq {\text{External}}_{/V}\left(C_1\right)$.

We know that ${\text{Internal}}_V\left(C_0\right)\simeq {\text{Internal}}_V\left(C_1\right)$ and ${\text{Internal}}_{/V}\left(C_0\right)\simeq {\text{Internal}}_{/V}\left(C_1\right)$, because

$$\begin{array}{cc}\left({\text{Internal}}_V\right(C_0){)}^{\ast }& \cong {\text{External}}_V\left(C_0^{\ast }\right)\\ & \simeq {\text{External}}_V\left(C_1^{\ast }\right)\\ & \cong {\text{Internal}}_V\left(C_1\right)\end{array}$$

and

$$\begin{array}{cc}\left({\text{Internal}}_{/V}\right(C_0){)}^{\ast }& \cong {\text{External}}_{/V}\left(C_0^{\ast }\right)\\ & \simeq {\text{External}}_{/V}\left(C_1^{\ast }\right)\\ & \cong {\text{Internal}}_{/V}\left(C_1\right).\end{array}$$

$\square$

 

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

Claim: ${\text{Commit}}_S\left(C\right)\cong 1_S⊸C$ and ${\text{Assume}}_S\left(C\right)\cong 1_S\otimes C$.

Proof: Let $C=(A,E,\cdot )$, and let $1_S=\left(\right\{a\},S,\diamond )$. 

Let ${\text{Commit}}_S\left(C\right)=(B,E,\star )$, where $B=\{b\in A|\forall e\in e,b\cdot e\in S\}$, and $b\star e=b\cdot e$. 

Let $1_S⊸C=\left(\text{hom}\right(1_S,C),\{a\}\times E,\bullet )$, where

$$\begin{array}{cc}(g,h)\bullet (a,e)& =g\left(a\right)\cdot e\\ & =a\diamond h\left(e\right)\\ & =h\left(e\right).\end{array}$$

We construct an isomorphism $(g_0,h_0):(1_S⊸C)\to {\text{Commit}}_S\left(C\right)$, by defining $g_0:\text{hom}(1_S,C)\to B$ by $g_0(g,h)=g\left(a\right)$, and by defining $h_0:E\to \left\{a\right\}\times E$ by $h_0\left(e\right)=(a,e)$.

First, we need to show that $g_0$ is a well-defined function into $B$. Observe that for all $(g,h)\in \text{hom}(1_S,C)$, and for all $e\in E$,

$$\begin{array}{cc}{g}_0(g,h)\cdot e& =g\left(a\right)\cdot e\\ & =h\left(e\right)\end{array}$$

$\in S$, and so $g_0(g,h)\in B$.

Next, we show that $(g_0,h_0)$ is a morphism, by showing that for all $(g,h)\in \text{hom}(1_S,C)$ and $e\in E$,

$$\begin{array}{cc}{g}_0(g,h)\star e& =g\left(a\right)\star e\\ & =g\left(a\right)\cdot e\\ & =a\diamond h\left(e\right)\\ & =(g,h)\bullet (a,e)\\ & =(g,h)\bullet h_0\left(e\right).\end{array}$$

Finally, to show that $(g_0,h_0)$, we need to show that $g_0$ and $h_0$ are bijections. Clearly, $h_0$ is a bijection. To see that $g_0$ is injective, observe that if $g_0(g,h)=g_0(g^{\prime },h^{\prime })$, then $g\left(a\right)=g^{\prime }\left(a\right)$, so $g=g^{\prime }$. Further, for all $e\in E$, 

$$\begin{array}{cc}h\left(e\right)& =a\diamond h\left(e\right)\\ & =g\left(a\right)\cdot e\\ & =g^{\prime }\left(a\right)\cdot e\\ & =a\diamond h^{\prime }\left(e\right)\\ & =h^{\prime }\left(e\right),\end{array}$$

so $h=h^{\prime }$. Thus $g_0$ is injective. To see that $g_0$ is surjective, observe that for all $b\in B$, there exists a morphism $(g_b,h_b):1_S\to C$, given by $g_b\left(a\right)=b$, and $h_b\left(e\right)=b\star e$. This is a morphism because, for all $a\in \left\{a\right\}$ and $e\in E$,

$$\begin{array}{cc}{g}_b\left(a\right)\star e& =b\star e\\ & =h_b\left(e\right)\\ & =a\diamond h_b\left(e\right).\end{array}$$

Since

$$\begin{array}{cc}{g}_0(g_b,h_b)& =g_b\left(a\right)\\ & =b,\end{array}$$

we have that $g_0$ is surjective, and thus $(g_0,h_0)$ is an isomorphism between $1_S⊸C$ and ${\text{Commit}}_S\left(C\right)$.

To see that ${\text{Assume}}_S\left(C\right)\cong 1_S\otimes C$, observe that

$$\begin{array}{cc}{\text{Assume}}_S\left(C\right)& \cong {\text{Commit}}_S(C^{\ast }{)}^{\ast }\\ & \cong (1_S\to C^{\ast }{)}^{\ast }\\ & \cong (1_S^{\ast }⅋C^{\ast }{)}^{\ast }\\ & \cong 1_S\otimes C.\end{array}$$

$\square$

Recall that we can think of $1_S$ as a powerless agent that has been promised $S$. $1_S\otimes C$, then, is a team consisting of $\text{Agent}\left(C\right)$ 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 $\text{Agent}\left(1_S\right)$ is powerless, the resultant team is exactly $\text{Agent}\left(C\right)$ joined with the promise, i.e., ${\text{Assume}}_S\left(C\right)$.

${\text{Commit}}_S\left(C\right)\cong 1_S⊸C$ is less intuitive. $1_S⊸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 $1_S$, as this highlights the close relationship between these operations and the other objects and operations we've been working with.¹ [LW(p) · GW(p)]

 

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,\cdot )$ over $W$ and subset $S$ of $W$, ${\text{Commit}}_S\left(C\right)◃{\perp }_S$ and ${\text{Assume}}_S\left(C\right)◃{\perp }_S$.

Proof: Trivial. $\square$

Claim: For any Cartesian frame $C=(A,E,\cdot )$ over $W$ and subset $S$ of $W$, with $C◃{\perp }_S$, ${\text{Commit}}_S\left(C\right)\cong {\text{Assume}}_S\left(C\right)\cong C$.

Proof: Trivial. $\square$

Corollary: For any subset $S$ of $W$, ${\text{Commit}}_S$ and ${\text{Assume}}_S$ are idempotent.

Proof: Trivial. $\square$

Claim: For any Cartesian frame $C=(A,E,\cdot )$ over $W$ and subset $S$ of $W$, if ${\text{Commit}}_{\setminus S}=(A^{\prime },E^{\prime },{\cdot }^{\prime })$, then for all $a^{\prime }\in A^{\prime }$, there exists an $e^{\prime }\in E^{\prime }$ such that $a^{\prime }{\cdot }^{\prime }{e}^{\prime }\notin S$.

Proof: Trivial. $\square$

Claim: For any Cartesian frame $C=(A,E,\cdot )$ over $W$ and subset $S$ of $W$, if for all $a\in A$, there exists an $e\in E$ such that $a\cdot e\notin S$, then ${\text{Commit}}_{\setminus S}\left(C\right)\cong C$.

Proof: Trivial. $\square$

Corollary: For any subset $S$ of $W$, ${\text{Commit}}_{\setminus S}$ is idempotent.

Proof: Trivial. $\square$

Claim: For any Cartesian frame $C=(A,E,\cdot )$ over $W$ and subset $S$ of $W$, if ${\text{Assume}}_{\setminus S}\left(C\right)=(A^{\prime },E^{\prime },{\cdot }^{\prime })$, then for all $e^{\prime }\in E^{\prime }$, there exists an $a^{\prime }\in A^{\prime }$ such that $a^{\prime }{\cdot }^{\prime }{e}^{\prime }\notin S$.

Proof: Trivial. $\square$

Claim: For any Cartesian frame $C=(A,E,\cdot )$ over $W$ and subset $S$ of $W$, if for all $e\in E$, there exists an $a\in A$ such that $a\cdot e\notin S$, then ${\text{Assume}}_{\setminus S}\left(C\right)\cong C$.

Proof: Trivial. $\square$

Corollary: For any subset $S$ of $W$, ${\text{Assume}}_{\setminus S}\left(C\right)$ is idempotent.

Proof: Trivial. $\square$

 

4.2. Externalizing

Claim: For any Cartesian frame $C=(A,E,\cdot )$ over $W$ and partition $V$ of $W$, let $v:W\to V$ send each element of $W$ to its part in $V$. If ${\text{External}}_V\left(C\right)=(A^{\prime },E^{\prime },{\cdot }^{\prime })$, then $A^{\prime }$ is nonempty and for all $a_0^{\prime },a_1^{\prime }\in A^{\prime }$ and $e^{\prime }\in E^{\prime }$, we have $v\left(a_0^{\prime }{\cdot }^{\prime }{e}^{\prime }\right)=v\left(a_1^{\prime }{\cdot }^{\prime }{e}^{\prime }\right)$.

Proof: Let $B$ be defined, as in the definition of ${\text{External}}_V$, as $B=\left\{\right\{a^{\prime }\in A|\forall e\in E,v(a^{\prime }\cdot e)=v(a\cdot e)\}|a\in A\}$. $A^{\prime }$ 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^{\prime }=B\times E$. $A^{\prime }$ is clearly nonempty. Consider an arbitrary $a_0^{\prime },a_1^{\prime }\in A^{\prime }$ and $(e,b)\in E^{\prime }$. Since $a_0^{\prime }\left(b\right),a_0^{\prime }\left(b\right)\in b$ are in the same part, we have that $a_0^{\prime }\left(b\right)\cdot e=a_0^{\prime }\left(b\right)\cdot e$, and thus $v\left(a_0^{\prime }{\cdot }^{\prime }\right(b,e\left)\right)=v\left(a_1^{\prime }{\cdot }^{\prime }\right(b,e\left)\right)$. $\square$

Claim: For any Cartesian frame $C=(A,E,\cdot )$ over $W$ and partition $V$ of $W$, let $v:W\to V$ send each element of $W$ to its part in $V$. If $A$ is nonempty and for all $a_0,a_1\in A$ and $e\in E\text{,}$ we have $v(a_0\cdot e)=v(a_1\cdot e)$, then ${\text{External}}_V\left(C\right)\cong C$.

Proof: Let $B$ be defined, as in the definition of ${\text{External}}_V$, as $B=\left\{\right\{a^{\prime }\in A|\forall e\in E,v(a^{\prime }\cdot e)=v(a\cdot e)\}|a\in A\}$. If $A$ is nonempty and for all $a_0,a_1\in A$ and $e\in E$, we have $v(a_0\cdot e)=v(a_1\cdot e)$, then $B$ has only one part, $B=\left\{A\right\}$. Thus, ${\text{External}}_V\left(C\right)=\left(A/\right\{A\},\{A\}\times E,\star )$, where $\star$ is given by $q\star (A,e)=q\left(A\right)\cdot e$.

Let $(g,h):{\text{External}}_V\left(C\right)\to C$ be given by $g\left(q\right)=q\left(A\right)$, and $h\left(e\right)=(A,e)$. This is trivially a morphism, and both $g$ and $h$ are trivially bijections, so ${\text{External}}_V\left(C\right)\cong C$.$\square$

Corollary: For any partition $V$ of $W$, ${\text{External}}_V$ is idempotent.

Proof: Trivial. $\square$

Claim: For any Cartesian frame $C=(A,E,\cdot )$ over $W$ and partition $V$ of $W$, let $v:W\to V$ send each element of $W$ to its part in $V$. If ${\text{External}}_{/V}=(A^{\prime },E^{\prime },{\cdot }^{\prime })$, then for all $a_0^{\prime }\ne a_1^{\prime }\in A^{\prime }$ there exists an $e^{\prime }\in E^{\prime }$, such that $v\left(a_0^{\prime }{\cdot }^{\prime }{e}^{\prime }\right)\ne v\left(a_1^{\prime }{\cdot }^{\prime }{e}^{\prime }\right)$.

Proof: Let $B$ be defined once again as $B=\left\{\right\{a^{\prime }\in A|\forall e\in E,v(a^{\prime }\cdot e)=v(a\cdot e)\}|a\in A\}$. $A^{\prime }=B$ and $E^{\prime }=A/B\times E$. Since $A/B$ is clearly nonempty, fix any $q\in A/B$. Observe that if $a_0^{\prime }\ne a_1^{\prime }$, then $q\left(a_0^{\prime }\right)$ and $q\left(a_1^{\prime }\right)$ are in different parts in B, so there exists an $e\in E$ such that $v\left(q\right(a_0^{\prime })\cdot e)\ne v\left(q\right(a_1^{\prime })\cdot e)$. Thus $v\left(a_0^{\prime }{\cdot }^{\prime }\right(q,e\left)\right)\ne v\left(a_1^{\prime }{\cdot }^{\prime }\right(q,e\left)\right)$. $\square$

Claim: For any Cartesian frame $C=(A,E,\cdot )$ over $W$ and partition $V$ of $W$, let $v:W\to V$ send each element of $W$ to its part in $V$. If for all $a_0\ne a_1\in A$ there exists an $e\in E$, such that $v(a_0\cdot e)\ne v(a_1\cdot e)$, then ${\text{External}}_V\left(C\right)\cong C$.

Proof: Again, let $B$ be defined again as $B=\left\{\right\{a^{\prime }\in A|\forall e\in E,v(a^{\prime }\cdot e)=v(a\cdot e)\}|a\in A\}$. If for all $a_0\ne a_1\in A$ there exists an $e\in E$ such that $v(a_0\cdot e)\ne v(a_1\cdot e)$, then every element of $B$ is a singleton. Thus $A/B=\left\{q\right\}$ is a singleton, and $q$ is a bijection.

${\text{External}}_{/V}\left(C\right)=(B,\{q\}\times E,\star )$, where $\star$ is given by $b\star (q,e)=q\left(b\right)\cdot e$. Let $(g,h):{\text{External}}_{/V}\left(C\right)\to C$ be given by $g\left(b\right)=q\left(b\right)$, and $h\left(e\right)=(q,e)$. This is trivially a morphism and both $g$ and $h$ are trivially bijections, so ${\text{External}}_{/V}\left(C\right)\cong C$. $\square$

Corollary: For any partition $V$ of $W$, ${\text{External}}_{/V}\left(C\right)$ is idempotent.

Proof: Trivial. $\square$

 

4.3. Internalizing

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

Claim: For any Cartesian frame $C=(A,E,\cdot )$ over $W$ and partition $V$ of $W$, let $v:W\to V$ send each element of $W$ to its part in $V$. If ${\text{Internal}}_V\left(C\right)=(A^{\prime },E^{\prime },{\cdot }^{\prime })$, then $E^{\prime }$ is nonempty and for all $e_0^{\prime },e_1^{\prime }\in E^{\prime }$ and $a^{\prime }\in A^{\prime }$, we have $v\left(a^{\prime }{\cdot }^{\prime }{e}_0^{\prime }\right)=v\left(a^{\prime }{\cdot }^{\prime }{e}_1^{\prime }\right)$.

Proof: Trivial. $\square$

Claim: For any Cartesian frame $C=(A,E,\cdot )$ over $W$ and partition $V$ of $W$, let $v:W\to V$ send each element of $W$ to its part in $V$. If for all $e_0,e_1\in E$ and $a\in A$ we have $v(a\cdot e_0)=v(a\cdot e_1)$, then ${\text{Internal}}_V\left(C\right)\cong C$.

Proof: Trivial. $\square$

Corollary: For any partition $V$ of $W$, ${\text{Internal}}_V\left(C\right)$ is idempotent.

Proof: Trivial. $\square$

Claim: For any Cartesian frame $C=(A,E,\cdot )$ over $W$ and partition $V$ of $W$, let $v:W\to V$ send each element of $W$ to its part in $V$. If ${\text{Internal}}_{/V}\left(C\right)=(A^{\prime },E^{\prime },{\cdot }^{\prime })$, then for all $e_0^{\prime }\ne e_1^{\prime }\in E^{\prime }$ there exists an $a^{\prime }\in A^{\prime }$, such that $v\left(a^{\prime }{\cdot }^{\prime }{e}_0^{\prime }\right)\ne v\left(a^{\prime }{\cdot }^{\prime }{e}_0^{\prime }\right)$.

Proof: Trivial. $\square$

Claim: For any Cartesian frame $C=(A,E,\cdot )$ over $W$ and partition $V$ of $W$, let $v:W\to V$ send each element of $W$ to its part in $V$. If for all $e_0\ne e_1\in A$ there exists an $a\in A$, such that $v(a\cdot e_0)\ne v(a\cdot e_1)$, then ${\text{Internal}}_V\left(C\right)\cong C$.

Proof: Trivial. $\square$

Corollary: For any partition $V$ of $W$, ${\text{Internal}}_{/V}\left(C\right)$ is idempotent.

Proof: Trivial. $\square$

 

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 $1_S$ as it relates to multiplicative operations. The additive role of $1_S$ is quite different from this, and quite varied. There isn't a single interpretation for $1_S$ in additive contexts, beyond the basic interpretation we provided in "Biextensional Equivalence [LW · GW]" that $1_S$ is "a powerless, all-knowing agent... plus a promise from the environment that the world will be in $S$." ↩ [LW · GW]

25 comments

Comments sorted by top scores.