Committing, Assuming, Externalizing, and Internalizing

Scott Garrabrant

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 , $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 ${Commit}^{B} (C)$ denote the Cartesian frame $(B, E, ⋆)$ , with $⋆$ given by $b ⋆ e = b \cdot e$ . Let ${Commit}^{∖ B} (C)$ denote the Cartesian frame $(A ∖ B, E, ⋄)$ , with $⋄$ given by $a ⋄ e = a \cdot e$ .

${Commit}^{B} (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 \subseteq A$ , ${Commit}^{B} (C) ◃_{+} C$ and ${Commit}^{∖ B} (C) ◃_{+} C$ . Further, ${Commit}^{∖ B} (C)$ and ${Commit}^{B} (C)$ are brothers in $C$ .

Proof: That ${Commit}^{B} (C) ◃_{+} C$ and ${Commit}^{∖ B} (C) ◃_{+} C$ is trivial from the committing definition of additive subagent.

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

Claim: ${Commit}^{∖ B} (C) ≅ {Commit}^{A ∖ B} (C)$

Proof: Trivial. $□$

1.2. Assuming

Assuming is the dual operation to committing.

Definition: Given a subset $F \subseteq E$ , let ${Assume}^{F} (C)$ denote the Cartesian frame $(A, F, ⋆)$ , with $⋆$ given by $a ⋆ f = a \cdot f$ . Let ${Assume}^{∖ F} (C)$ denote the Cartesian frame $(A, E ∖ F, ⋄)$ , with $⋄$ given by $a ⋄ e = a \cdot e$ .

${Assume}^{F} (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:

$C_{0} = \begin{matrix} \begin{matrix} r & s & m \end{matrix} \begin{matrix} u n u \leftrightarrow r u \leftrightarrow s \end{matrix} & ⎛ ⎜ ⎜ ⎜ ⎝ \begin{matrix} u r & u s & m n r & n s & m u r & n s & m n r & u s & m \end{matrix} ⎞ ⎟ ⎟ ⎟ ⎠ \end{matrix}$ .

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}} (C_{0}) = \begin{matrix} \begin{matrix} r & s \end{matrix} \begin{matrix} u n u \leftrightarrow r u \leftrightarrow s \end{matrix} & ⎛ ⎜ ⎜ ⎜ ⎝ \begin{matrix} u r & u s n r & n s u r & n s n r & u s \end{matrix} ⎞ ⎟ ⎟ ⎟ ⎠ \end{matrix}$ .

Claim: For all $F \subseteq E$ , $({Assume}^{F} (C))^{*} ≅ {Commit}^{F} (C^{*})$ and $({Assume}^{∖ F} (C))^{*} ≅ {Commit}^{∖ F} (C^{*})$ . Similarly, for all $B \subseteq A$ , $({Commit}^{B} (C))^{*} ≅ {Assume}^{B} (C^{*})$ and $({Commit}^{∖ B} (C))^{*} ≅ {Assume}^{∖ B} (C^{*})$ .

Proof: Trivial. $□$

Claim: For all $F \subseteq E$ , $C ◃_{+}^{*} {Assume}^{F} (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 \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 (x) \in x$ for all $x \in X$ .

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

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

${External}^{B} (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$ , ${External}^{B} (C) ◃_{\times} C$ and ${External}^{/ B} (C) ◃_{\times} C$ . Further, ${External}^{B} (C)$ and ${External}^{/ B} (C)$ are sisters in $C$ .

Proof: Let ${External}^{B} (C) = (A / B, B \times E, ⋆)$ and ${External}^{/ B} (C) = (B, A / B \times E, ⋄)$ .

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

\begin{matrix} g_{e} (q) ⋄ b & = q (b) \cdot e = q ⋆ h_{e} (b) . \end{matrix}

Let $E^{'} \subseteq hom ({External}^{B} (C), ({External}^{/ B} (C))^{*})$ be given by $E^{'} = {(g_{e}, h_{e}) | e \in E}$ , and let $D = (A / B \times B, E^{'}, ∙)$ , where

\begin{matrix} (q, b) ∙ (g_{e}, h_{e}) & = g_{e} (q) ⋄ b = q ⋆ h_{e} (b) = q (b) \cdot e . \end{matrix}

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

To see $D ≃ 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 (b)$ . 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 (b) = a$ , and for each $b^{'} \neq b$ , choosing an $a^{'} \in b^{'}$ , and saying $q (b^{'}) = a^{'}$ . 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^{'}$ by $h_{0} (e) = (g_{e}, h_{e})$ , which is clearly surjective, and define $h_{1} : E^{'} \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{matrix} g_{0} (q, b) \cdot e & = q (b) \cdot e = (q, b) ∙ (g_{e}, h_{e}) = q, b ∙ h_{0} (e), \end{matrix}

so $(g_{0}, h_{0})$ is a morphism. This also gives us that for all $a \in A$ and $e^{'} \in E^{'}$ we have

\begin{matrix} g_{1} (a) ∙ e^{'} & = g_{1} (a) ∙ h_{0} (h_{1} (e^{'})) = g_{0} (g_{1} (a)) \cdot h_{1} (e) = a \cdot h_{1} (e), \end{matrix}

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^{'}$ . Thus, $D ≃ C$ .

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

\begin{matrix} {External}^{B} (C) & = (A / B, B \times E, ⋆) ≃ (A / B, B \times E^{'}, ⋆^{'}), \end{matrix}

and

\begin{matrix} {External}^{/ B} (C) & = (B, A / B \times E, ⋄) ≃ (B, A / B \times E^{'}, ⋄^{'}), \end{matrix}

where $⋆^{'}$ and $⋄^{'}$ are given by

\begin{matrix} q ⋆^{'} (b, (g_{e}, h_{e})) & = b ⋄^{'} (q, (g_{e}, h_{e})) = q ⋆ h_{e} (b) = b ⋄ g_{e} (q) = q (b) \cdot e . \end{matrix}

Indeed, we show that if $A$ is nonempty, $(A / B, B \times E, ⋆) ≅ (A / B, B \times E^{'}, ⋆^{'})$ , and $(B, A / B \times E, ⋄) ≅ (B, A / B \times E^{'}, ⋄^{'})$ .

If $A$ is nonempty, then the function from $E$ to $E^{'}$ 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} (a) = (a, e)$ . This gives a bijection between $B \times E$ and $B \times E^{'}$ , and we have that for all $q \in A / B$ , $b \in B$ , and $e \in E$ ,

\begin{matrix} q ⋆^{'} (b, (g_{e}, h_{e})) & = q (b) \cdot e = q ⋆ (b, e) . \end{matrix}

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

\begin{matrix} b ⋄^{'} (q, (g_{e}, h_{e})) & = q (b) \cdot e = b ⋄ (q, e) . \end{matrix}

If $A$ is empty, then $B$ is empty, and $A / p$ is a singleton empty function, so $(A / B, B \times E, ⋆) ≃ (A / B, B \times E^{'}, ⋆^{'}) ≃ ⊤$ , and we either have $(B, A / B \times E, ⋄) ≃ (B, A / B \times E^{'}, ⋄^{'}) ≃ 0$ or $(B, A / B \times E, ⋄) ≃ (B, A / B \times E^{'}, ⋄^{'}) ≃ null$ , depending on whether or not $E$ is empty.

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

1.4. Internalizing

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

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

Claim: For all partitions $F$ of $E$ , $({Internal}^{F} (C))^{*} ≅ {External}^{F} (C^{*})$ and $({Internal}^{/ F} (C))^{*} ≅ {External}^{/ F} (C^{*})$ . Similarly, for all partitions $B$ of $A$ , $({External}^{B} (C))^{*} ≅ {Internal}^{B} (C^{*})$ and $({External}^{/ B} (C))^{*} ≅ {Internal}^{/ B} (C^{*})$ .

Proof: Trivial. $□$

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

Proof: This follows from the fact that $({Internal}^{F} (C))^{*} ≅ {External}^{F} (C^{*}) ◃_{\times} C^{*}$ and $({Internal}^{/ F} (C))^{*} ≅ {External}^{/ F} (C^{*}) ◃_{\times} 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 \subseteq W$ , we define ${Commit}_{S} (C) = {Commit}^{B} (C)$ and ${Commit}_{∖ S} (C) = {Commit}^{∖ B} (C)$ , 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$ , ${Commit}_{S} (C) ◃_{+} C$ and ${Commit}_{∖ S} (C) ◃_{+} C$ . Further, ${Commit}_{∖ S} (C)$ and ${Commit}_{S} (C)$ are brothers in $C$ .

Proof: Trivial. $□$

Unlike before, it is not necessarily the case that ${Commit}_{∖ S} (C) ≅ {Commit}_{W ∖ 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 \subseteq W$ , we define ${Assume}_{S} (C) = {Assume}^{F} (C)$ and ${Assume}_{∖ S} (C) = {Assume}^{∖ F} (C)$ , 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$ , $({Assume}_{S} (C))^{*} ≅ {Commit}_{S} (C^{*})$ and $({Assume}_{∖ S} (C))^{*} ≅ {Commit}_{∖ S} (C^{*})$ , $({Commit}_{S} (C))^{*} ≅ {Assume}_{S} (C^{*})$ and $({Commit}_{∖ S} (C))^{*} ≅ {Assume}_{∖ S} (C^{*})$ .

Proof: Trivial. $□$

Claim: For all $S \subseteq W$ , $C ◃_{+}^{*} {Assume}_{S} (C)$ and $C ◃_{+}^{*} {Assume}_{∖ S} (C)$ .

Proof: Trivial. $□$

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 ${External}_{V} (C) = {External}^{B} (C)$ and ${External}_{/ V} (C) = {External}^{/ B} (C)$ , where $B = {{a^{'} \in A | \forall e \in E, v (a^{'} \cdot e) = v (a \cdot e)} | a \in A}$ .

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

Proof: Trivial. $□$

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 ${Internal}_{V} (C) = {Internal}^{F} (C)$ and ${Internal}_{/ V} (C) = {Internal}^{/ F} (C)$ , where $F = {{e^{'} \in E | \forall a \in a, v (a \cdot e^{'}) = v (a \cdot e)} | e \in E}$ .

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

Proof: Trivial. $□$

Claim: For all partitions $V$ of $W$ , $({Internal}_{V} (C))^{*} ≅ {External}_{V} (C^{*})$ , $({Internal}_{/ V} (C))^{*} ≅ {External}_{/ V} (C^{*})$ , $({External}_{V} (C))^{*} ≅ {Internal}_{V} (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 $C_{0} ≃ C_{1}$ are Cartesian frames over $W$ , then for any subset $S \subseteq W$ , ${Commit}_{S} (C_{0}) ≃ {Commit}_{S} (C_{1})$ , ${Commit}_{∖ S} (C_{0}) ≃ {Commit}_{∖ S} (C_{1})$ , ${Assume}_{S} (C_{0}) ≃ {Assume}_{S} (C_{1})$ , and ${Assume}_{∖ S} (C_{0}) ≃ {Assume}_{∖ S} (C_{1})$ .

Observe that if $b \in B_{0}$ , then for all $e \in E_{1}$ , $g_{0} (b) \cdot_{1} e = b \cdot_{0} h_{0} (e) \in S$ , so $g_{0} (b) \in B_{1}$ . Similarly, if $b \in B_{1}$ , then $g_{1} (b) \in B_{0}$ . Thus, if we let $g_{i}^{'} : B_{i} \to B_{1 - i}$ be given by $g_{i}^{'} (b) = g_{i} (b)$ , we get morphisms $(g_{i}^{'}, h_{i}) : {Commit}_{S} (C_{i}) \to {Commit}_{S} (C_{1 - i})$ , 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, $({id}_{A_{i}}, h_{1 - i} \circ h_{i}) : C_{i} \to C_{i}$ is a morphism, so $({id}_{B_{i}}, h_{1 - i} \circ h_{i}) : {Commit}_{S} (C_{i}) \to {Commit}_{S} (C_{i})$ is a morphism, so $(g_{0}^{'}, h_{0})$ and $(g_{1}^{'}, h_{1})$ compose to something homotopic to the identity in both orders. Thus ${Commit}_{S} (C_{0}) ≃ {Commit}_{S} (C_{1})$ .

Similarly, if $b \in A_{0} ∖ B_{0}$ , then there exists an $e \in E_{0}$ such that $b \cdot_{0} e \notin S$ . But then

\begin{matrix} g_{0} (b) \cdot_{1} h_{1} (e) & = g_{1} (g_{0} (b)) \cdot_{0} e = b \cdot_{0} e \end{matrix}

$\notin S$ , so $g_{0} (b) \in A_{1} ∖ B_{1}$ . Similarly, if $b \in A_{1} ∖ B_{1}$ , then $g_{1} (b) \in A_{0} ∖ B_{0}$ . Thus, if we let $g_{i}^{''} : A_{i} ∖ B_{i} \to A_{1 - i} ∖ B_{1 - i}$ be given by $g_{i}^{''} (b) = g_{i} (b)$ , we get morphisms $(g_{i}^{''}, h_{i}) : {Commit}_{∖ S} (C_{i}) \to {Commit}_{∖ S} (C_{1 - i})$ , which (similarly to above) compose to something homotopic to the identity in both orders. Thus, ${Commit}_{∖ S} (C_{0}) ≃ {Commit}_{∖ S} (C_{1})$ .

We know that ${Assume}_{S} (C_{0}) ≃ {Assume}_{S} (C_{1})$ and ${Assume}_{∖ S} (C_{0}) ≃ {Assume}_{∖ S} (C_{1})$ , because

\begin{matrix} ({Assume}_{S} (C_{0}))^{*} & ≅ {Commit}_{S} (C_{0}^{*}) ≃ {Commit}_{S} (C_{1}^{*}) ≅ {Assume}_{S} (C_{1}) \end{matrix}

and

\begin{matrix} ({Assume}_{∖ S} (C_{0}))^{*} & ≅ {Commit}_{∖ S} (C_{0}^{*}) ≃ {Commit}_{∖ S} (C_{1}^{*}) ≅ {Assume}_{∖ S} (C_{1}) . \end{matrix}

$□$

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

Claim: If $C_{0} ≃ C_{1}$ are Cartesian frames over $W$ , then for all partitions $V$ of $W$ , ${External}_{V} (C_{0}) ≃ {External}_{V} (C_{1})$ , ${External}_{/ V} (C_{0}) ≃ {External}_{/ V} (C_{1})$ , ${Internal}_{V} (C_{0}) ≃ {Internal}_{V} (C_{1})$ , and ${Internal}_{/ V} (C_{0}) ≃ {Internal}_{/ V} (C_{1})$ .

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} = {{a^{'} \in A_{i} | \forall e \in E_{i}, v (a^{'} \cdot e) = v (a \cdot e)} | a \in A_{i}}$ .

Let $β_{i} : A_{i} \to B_{i}$ , send each element of $A_{i}$ to its part in $B_{i}$ , so $β_{i} (a) = {a^{'} \in A_{i} | \forall e \in E_{i}, v (a^{'} \cdot e) = v (a \cdot e)}$ . Since $β_{i}$ is surjective, it has a right inverse. Let $α_{i} : B_{i} \to A_{i}$ be any choice of right inverse to $β_{i}$ . This gives a pair of functions $ι_{i} : B_{i} \to B_{1 - i}$ given by $ι_{i} = β_{1 - i} \circ g_{i} \circ α_{i}$ .

We start by showing that $ι_{0}$ and $ι_{1}$ are inverses, and thus bijections between $B_{0}$ and $B_{1}$ . We do this by showing that $β_{i} \circ g_{1 - i} \circ g_{i} = β_{i}$ , and that $ι_{i} \circ β_{i} = β_{1 - i} \circ g_{i}$ , and thus we will have

\begin{matrix} ι_{1 - i} \circ ι_{i} & = ι_{1 - i} \circ β_{1 - i} \circ g_{i} \circ α_{i} = β_{i} \circ g_{1 - i} \circ g_{i} \circ α_{i} = β_{i} \circ α_{i}, \end{matrix}

which is the identity on $B_{i}$ .

To see that $β_{i} \circ g_{1 - i} \circ g_{i} = β_{i}$ , observe that for all $a \in A_{i}$ , we have that for all $e \in E_{i}$ , $v (a \cdot_{i} e) = v (g_{1 - i} (g_{i} (a)) \cdot_{i} e)$ , so, $β_{i} (a) = β_{i} (g_{1 - i} (g_{i} (a)))$ . Thus, $β_{i} = β_{i} \circ g_{1 - i} \circ g_{i}$ .

To see that $ι_{i} \circ β_{i} = β_{1 - i} \circ g_{i}$ , first observe that for all $a \in A_{i}$ , we have that $β_{i} (α_{i} (β_{i} (a))) = β_{i} (a)$ , and thus, for all $e \in E_{1 - i}$ ,

\begin{matrix} v (g_{i} (a) \cdot_{1 - i} e) & = v (a \cdot_{i} h_{i} (e)) = v (α_{i} (β_{i} (a)) \cdot_{i} h_{i} (e)) = v (g_{i} (α_{i} (β_{i} (a))) \cdot_{1 - i} e) . \end{matrix}

Thus, $β_{1 - i} (g_{i} (a)) = β_{1 - i} (g_{i} (α_{i} (β_{i} (a))))$ . Thus, we have

\begin{matrix} β_{1 - i} \circ g_{i} & = β_{1 - i} \circ g_{i} \circ α_{i} \circ β_{i} = ι_{i} \circ β_{i} . \end{matrix}

This also gives us functions $f_{i} : A_{i} / B_{i} \to A_{1 - i} / B_{1 - i}$ , by $f_{i} (q) = g_{i} \circ q \circ ι_{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} (q)$ is in fact in $A_{1 - i} / B_{1 - i}$ , by showing that for all $b \in B_{1 - i}$ , $g_{i} (q (ι_{1 - i} (b))) \in b$ , or equivalently that $β_{1 - i} \circ g_{i} \circ q \circ ι_{1 - i}$ is the identity on $B_{1 - i}$ . Since $q \in A_{i} / B_{i}$ , we already have that $β_{i} \circ q$ is the identity of $B_{i}$ . Thus, we have that

\begin{matrix} β_{1 - i} \circ g_{i} \circ q \circ ι_{1 - i} & = ι_{i} \circ β_{i} \circ q \circ ι_{1 - i} = ι_{i} \circ ι_{1 - i} \end{matrix}

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

We are now ready to demonstrate that ${External}_{V} (C_{0}) ≃ {External}_{V} (C_{1})$ .

Let ${External}_{V} (C_{i}) = (A_{i} / B_{i}, B_{i} \times E_{i}, ⋆_{i})$ , and define

(g_{i}^{'}, h_{i}^{'}) : (A_{i} / B_{i}, B_{i} \times E_{i}, ⋆_{i}) \to (A_{1 - i} / B_{1 - i}, B_{1 - i} \times E_{1 - i}, ⋆_{1 - i})

by $g_{i}^{'} = f_{i}$ , while $h_{i}^{'} : B_{1 - i} \times E_{1 - i} \to B_{i} \times E_{i}$ is given by $h_{i}^{'} (b, e) = (ι_{1 - i} (b), h_{i} (e))$ .

To see that $(g_{i}^{'}, h_{i}^{'})$ is a morphism, observe that for all $q \in A_{i} / B_{i}$ , and $(b, e) \in B_{1 - i} \times E_{1 - i},$ we have

\begin{matrix} g_{i}^{'} (q) ⋆_{1 - i} (b, e) & = f_{i} (q) ⋆_{1 - i} (b, e) = f_{i} (q) (b) \cdot_{1 - i} e = g_{i} (q (ι_{1 - i} (b))) \cdot_{1 - i} e = q (ι_{1 - i} (b)) \cdot_{i} h_{i} (e) = q ⋆_{i} (ι_{1 - i} (b), h_{i} (e)) = q ⋆_{i} h_{i}^{'} (b, e) . \end{matrix}

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

({id}_{A_{i} / B_{i}}, h_{i}^{'} \circ h_{1 - i}^{'}) : (A_{i} / B_{i}, B_{i} \times E_{i}, ⋆_{i}) \to (A_{i} / B_{i}, B_{i} \times E_{i}, ⋆_{i})

is a morphism. Indeed, for all $q \in A_{i} / B_{i}$ and $(b, e) \in B_{i} \times E_{i}$ ,

\begin{matrix} q ⋆_{i} h_{i}^{'} (h_{1 - i}^{'} (b, e)) & = q ⋆_{i} (b, h_{i} (h_{1 - i} (e))) = q (b) \cdot_{i} h_{i} (h_{1 - i} (e)) = q (b) \cdot_{i} e = q ⋆_{i} (b, e) . \end{matrix}

Thus, ${External}_{V} (C_{0}) ≃ {External}_{V} (C_{1})$

Similarly, let ${External}_{/ V} (C_{i}) = (B_{i}, A_{i} / B_{i} \times E_{i}, ⋄_{i})$ , and define

(g_{i}^{''}, h_{i}^{''}) : (B_{i}, A_{i} / B_{i} \times E_{i}, ⋄_{i}) \to (B_{1 - i}, A_{1 - i} / B_{1 - i} \times E_{1 - i}, ⋄_{1 - i})

by $g_{i}^{''} = ι_{i}$ , and $h_{i}^{''} : A_{1 - i} / B_{1 - i} \times E_{1 - i} \to A_{i} / B_{i} \times E_{i}$ is given by $h_{i}^{''} (q, e) = (f_{1 - i} (q), h_{i} (e))$ .

To see that $(g_{i}^{''}, h_{i}^{''})$ 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{matrix} g_{i}^{''} (b) ⋄_{1 - i} (q, e) & = ι_{i} (b) ⋄_{1 - i} (q, e) = q (ι_{i} (b)) \cdot_{1 - i} e = q (ι_{i} (b)) \cdot_{1 - i} h_{1 - i} (h_{i} (e)) = g_{1 - i} (q (ι_{i} (b))) \cdot_{i} h_{i} (e) = f_{1 - i} (q) (b) \cdot_{i} h_{i} (e) = b ⋄_{i} (f_{1 - i} (q), h_{i} (e)) = b ⋄_{i} h_{i}^{''} (q, e) . \end{matrix}

Clearly, $(g_{1 - i}^{''}, h_{1 - i}^{''}) \circ (g_{i}^{''}, h_{i}^{''})$ is homotopic to the identity, since $g_{1 - i}^{''} \circ g_{i}^{''}$ is the identity on $B_{i}$ . Thus, ${External}_{/ V} (C_{0}) ≃ {External}_{/ V} (C_{1})$ .

We know that ${Internal}_{V} (C_{0}) ≃ {Internal}_{V} (C_{1})$ and ${Internal}_{/ V} (C_{0}) ≃ {Internal}_{/ V} (C_{1})$ , because

\begin{matrix} ({Internal}_{V} (C_{0}))^{*} & ≅ {External}_{V} (C_{0}^{*}) ≃ {External}_{V} (C_{1}^{*}) ≅ {Internal}_{V} (C_{1}) \end{matrix}

and

\begin{matrix} ({Internal}_{/ V} (C_{0}))^{*} & ≅ {External}_{/ V} (C_{0}^{*}) ≃ {External}_{/ V} (C_{1}^{*}) ≅ {Internal}_{/ V} (C_{1}) . \end{matrix}

$□$

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

Claim: ${Commit}_{S} (C) ≅ 1_{S} ⊸ C$ and ${Assume}_{S} (C) ≅ 1_{S} \otimes C$ .

Proof: Let $C = (A, E, \cdot)$ , and let $1_{S} = ({a}, S, ⋄)$ .

Let ${Commit}_{S} (C) = (B, E, ⋆)$ , where $B = {b \in A | \forall e \in e, b \cdot e \in S}$ , and $b ⋆ e = b \cdot e$ .

Let $1_{S} ⊸ C = (hom (1_{S}, C), {a} \times E, ∙)$ , where

\begin{matrix} (g, h) ∙ (a, e) & = g (a) \cdot e = a ⋄ h (e) = h (e) . \end{matrix}

We construct an isomorphism $(g_{0}, h_{0}) : (1_{S} ⊸ C) \to {Commit}_{S} (C)$ , by defining $g_{0} : hom (1_{S}, C) \to B$ by $g_{0} (g, h) = g (a)$ , and by defining $h_{0} : E \to {a} \times E$ by $h_{0} (e) = (a, e)$ .

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

\begin{matrix} g_{0} (g, h) \cdot e & = g (a) \cdot e = h (e) \end{matrix}

$\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 hom (1_{S}, C)$ and $e \in E$ ,

\begin{matrix} g_{0} (g, h) ⋆ e & = g (a) ⋆ e = g (a) \cdot e = a ⋄ h (e) = (g, h) ∙ (a, e) = (g, h) ∙ h_{0} (e) . \end{matrix}

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^{'}, h^{'})$ , then $g (a) = g^{'} (a)$ , so $g = g^{'}$ . Further, for all $e \in E$ ,

\begin{matrix} h (e) & = a ⋄ h (e) = g (a) \cdot e = g^{'} (a) \cdot e = a ⋄ h^{'} (e) = h^{'} (e), \end{matrix}

so $h = h^{'}$ . 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} (a) = b$ , and $h_{b} (e) = b ⋆ e$ . This is a morphism because, for all $a \in {a}$ and $e \in E$ ,

\begin{matrix} g_{b} (a) ⋆ e & = b ⋆ e = h_{b} (e) = a ⋄ h_{b} (e) . \end{matrix}

Since

\begin{matrix} g_{0} (g_{b}, h_{b}) & = g_{b} (a) = b, \end{matrix}

we have that $g_{0}$ is surjective, and thus $(g_{0}, h_{0})$ is an isomorphism between $1_{S} ⊸ C$ and ${Commit}_{S} (C)$ .

To see that ${Assume}_{S} (C) ≅ 1_{S} \otimes C$ , observe that

\begin{matrix} {Assume}_{S} (C) & ≅ {Commit}_{S} (C^{*})^{*} ≅ (1_{S} \to C^{*})^{*} ≅ (1_{S}^{*} ⅋ C^{*})^{*} ≅ 1_{S} \otimes C . \end{matrix}

$□$

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 $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 (1_{S})$ is powerless, the resultant team is exactly $Agent (C)$ joined with the promise, i.e., ${Assume}_{S} (C)$ .

${Commit}_{S} (C) ≅ 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.¹

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$ , ${Commit}_{S} (C) ◃ ⊥_{S}$ and ${Assume}_{S} (C) ◃ ⊥_{S}$ .

Proof: Trivial. $□$

Claim: For any Cartesian frame $C = (A, E, \cdot)$ over $W$ and subset $S$ of $W$ , with $C ◃ ⊥_{S}$ , ${Commit}_{S} (C) ≅ {Assume}_{S} (C) ≅ C$ .

Proof: Trivial. $□$

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

Proof: Trivial. $□$

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

Proof: Trivial. $□$

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 ${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, \cdot)$ over $W$ and subset $S$ of $W$ , if ${Assume}_{∖ S} (C) = (A^{'}, E^{'}, \cdot^{'})$ , then for all $e^{'} \in E^{'}$ , there exists an $a^{'} \in A^{'}$ such that $a^{'} \cdot^{'} e^{'} \notin S$ .

Proof: Trivial. $□$

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 ${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, \cdot)$ over $W$ and partition $V$ of $W$ , let $v : W \to V$ send each element of $W$ to its part in $V$ . If ${External}_{V} (C) = (A^{'}, E^{'}, \cdot^{'})$ , then $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^{'})$ .

Proof: Let $B$ be defined, as in the definition of ${External}_{V}$ , as $B = {{a^{'} \in A | \forall e \in E, v (a^{'} \cdot e) = v (a \cdot e)} | a \in 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 \times E$ . $A^{'}$ is clearly nonempty. Consider an arbitrary $a_{0}^{'}, a_{1}^{'} \in A^{'}$ and $(e, b) \in E^{'}$ . Since $a_{0}^{'} (b), a_{0}^{'} (b) \in b$ are in the same part, we have that $a_{0}^{'} (b) \cdot e = a_{0}^{'} (b) \cdot e$ , and thus $v (a_{0}^{'} \cdot^{'} (b, e)) = v (a_{1}^{'} \cdot^{'} (b, e))$ . $□$

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,$ we have $v (a_{0} \cdot e) = v (a_{1} \cdot e)$ , then ${External}_{V} (C) ≅ C$ .

Proof: Let $B$ be defined, as in the definition of ${External}_{V}$ , as $B = {{a^{'} \in A | \forall e \in E, v (a^{'} \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 = {A}$ . Thus, ${External}_{V} (C) = (A / {A}, {A} \times E, ⋆)$ , where $⋆$ is given by $q ⋆ (A, e) = q (A) \cdot e$ .

Let $(g, h) : {External}_{V} (C) \to 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 ${External}_{V} (C) ≅ C$ . $□$

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

Proof: Trivial. $□$

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 ${External}_{/ V} = (A^{'}, E^{'}, \cdot^{'})$ , then for all $a_{0}^{'} \neq a_{1}^{'} \in A^{'}$ there exists an $e^{'} \in E^{'}$ , such that $v (a_{0}^{'} \cdot^{'} e^{'}) \neq v (a_{1}^{'} \cdot^{'} e^{'})$ .

Proof: Let $B$ be defined once again as $B = {{a^{'} \in A | \forall e \in E, v (a^{'} \cdot e) = v (a \cdot e)} | a \in A}$ . $A^{'} = B$ and $E^{'} = A / B \times E$ . Since $A / B$ is clearly nonempty, fix any $q \in A / B$ . Observe that if $a_{0}^{'} \neq a_{1}^{'}$ , then $q (a_{0}^{'})$ and $q (a_{1}^{'})$ are in different parts in B, so there exists an $e \in E$ such that $v (q (a_{0}^{'}) \cdot e) \neq v (q (a_{1}^{'}) \cdot e)$ . Thus $v (a_{0}^{'} \cdot^{'} (q, e)) \neq v (a_{1}^{'} \cdot^{'} (q, e))$ . $□$

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} \neq a_{1} \in A$ there exists an $e \in E$ , such that $v (a_{0} \cdot e) \neq v (a_{1} \cdot e)$ , then ${External}_{V} (C) ≅ C$ .

Proof: Again, let $B$ be defined again as $B = {{a^{'} \in A | \forall e \in E, v (a^{'} \cdot e) = v (a \cdot e)} | a \in A}$ . If for all $a_{0} \neq a_{1} \in A$ there exists an $e \in E$ such that $v (a_{0} \cdot e) \neq v (a_{1} \cdot 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} \times E, ⋆)$ , where $⋆$ is given by $b ⋆ (q, e) = q (b) \cdot e$ . Let $(g, h) : {External}_{/ V} (C) \to 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, \cdot)$ over $W$ and partition $V$ of $W$ , let $v : W \to V$ send each element of $W$ to its part in $V$ . If ${Internal}_{V} (C) = (A^{'}, E^{'}, \cdot^{'})$ , then $E^{'}$ is nonempty and for all $e_{0}^{'}, e_{1}^{'} \in E^{'}$ and $a^{'} \in A^{'}$ , we have $v (a^{'} \cdot^{'} e_{0}^{'}) = v (a^{'} \cdot^{'} e_{1}^{'})$ .

Proof: Trivial. $□$

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 ${Internal}_{V} (C) ≅ C$ .

Proof: Trivial. $□$

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

Proof: Trivial. $□$

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 ${Internal}_{/ V} (C) = (A^{'}, E^{'}, \cdot^{'})$ , then for all $e_{0}^{'} \neq e_{1}^{'} \in E^{'}$ there exists an $a^{'} \in A^{'}$ , such that $v (a^{'} \cdot^{'} e_{0}^{'}) \neq v (a^{'} \cdot^{'} e_{0}^{'})$ .

Proof: Trivial. $□$

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} \neq e_{1} \in A$ there exists an $a \in A$ , such that $v (a \cdot e_{0}) \neq v (a \cdot e_{1})$ , then ${Internal}_{V} (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 $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" that $1_{S}$ is "a powerless, all-knowing agent... plus a promise from the environment that the world will be in $S$ ." ↩

[-]Rohin Shah4yΩ580

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

Claim: is observable in the frame ${External}_{V} (C)$ .

Proof sketch: Every column of ${External}_{V} (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 $q_{1}, q_{2}$ in ${External}_{V} (C)$ , we can implement the conditional policy "if $^b$ then $q_{1}$ else $q_{2}$ " by defining $q (x) = q_{1} (x) if x \in ⋃^b else q_{2} (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.

[-]Scott Garrabrant4yΩ6100

This is not correct. It is true, however that is observable in ${External}_{V} ({Internal}_{V} (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.

[-]Rohin Shah4yΩ460

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

Whether or not it rains would be formalized by the partition $V = {{u r, n r}, {u s, n s}}$ .

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 ${External}^{B} (C) = (A / B, B \times E, ⋆)$ , we get out a Cartesian frame whose agent has only one option, for which all properties are trivially observable.

[-]Scott Garrabrant4yΩ360

I think .

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

[-]DanielFilan4yΩ240

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

[-]Scott Garrabrant4yΩ120

Yep, Thanks.

[-]Ramana Kumar4yΩ230

Let , send each element of $A_{i}$ to its part in $B_{i}$ , so $α (a) = {a^{'} \in A_{i} | \forall e \in E_{i}, v (a^{'} \cdot e) = v (a \cdot e)}$ .

Presuming the $α$ here should be a $β_{i}$

Fixed, thanks.

[-]Ramana Kumar4yΩ110

Claim: For any Cartesian frame 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}, a_{1} \in A$ and $e \in E,$ we have $v (a_{0} \cdot e) = v (a_{1} \cdot e)$ , then ${External}_{V} (C) ≅ C$ .

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

Fixed, Thanks

is given by $h_{i}^{'} (b, e) = (f_{1 - i} (b), h_{i} (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).

Claim: For all , ${Assume}^{F} (C) ◃_{+}^{*} C$ and ${Assume}^{∖ F} (C) ◃_{+}^{*} C$ .

Are these the wrong way around?

I believe $C ◃_{+}^{*} {A s s u m e}^{F} (C)$ is indeed trivial, but the opposite is less obvious.

Fixed, Thanks.

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 , ${Commit}_{S} (C) ◃_{+}^{*} C$ and ${Commit}_{∖ S} (C) ◃_{+}^{*} C$ .

Oh I see this has also been fixed. Thanks!

Similarly, for all , $({Commit}^{B} (C))^{*} ≅ {Assume}^{B} (C^{*})$ and $({Commit}^{∖ B} (C))^{*} ≅ {Assume}^{∖ B} (C^{*})$ .

We don't need $B$ to be a proper subset here (i.e., I think $\subset$ is a typo for $\subseteq$ ). 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.

LESSWRONG
LW

31

Committing, Assuming, Externalizing, and Internalizing

31

Ω 15

1. Definitions from Agents and Environments

2. Definitions from Worlds

3. Basic Properties

4. Idempotence

Footnotes

31

Ω 15