This is a list of the main definitions from Scott Garrabrant's Cartesian Frames sequence. (I'll update it as more posts come out.)
1. Small Cartesian Frames
Let W={w0,w1} for the matrix visualizations below. Let C be an arbitrary Cartesian frame.
visualization
definition
notes
0
e()
0=({},{e},⋅), where Agent(0) is empty, Env(0)={e} is any singleton set, and Eval(0) is trivial.
⊥{}. Initial. Identity of sum (⊕).
⊤
a()
⊤=({a},{},⋅), where Agent(⊤) is any singleton set, Env(⊤) is empty, and Eval(⊤) is trivial.
1{}. Terminal. ⊤◃C. Identity of product (&).
1
w0w1a(w0w1)
1S=({a},S,⋆), where S⊆W and a⋆s=s for all s∈S. 1 is the frame 1W.
Identity of tensor (⊗).
⊥
ew0w1(w0w1)
⊥S=(S,{e},⋆), where S⊆W and s⋆e=s for all s∈S. ⊥ is the frame ⊥W.
C◃⊥. Identity of par (⅋).
null
()
null=({},{},⋅), with empty agent, environment, and evaluation function.
2. Binary Operations
Sum. For Cartesian frames C=(A,E,⋅) and D=(B,F,⋆) over W, C⊕D is the Cartesian frame (A⊔B,E×F,⋄), where a⋄(e,f)=a⋅e if a∈A, and a⋄(e,f)=a⋆f if a∈B.
Product. For Cartesian frames C=(A,E,⋅) and D=(B,F,⋆) over W, C&D is the Cartesian frame (A×B,E⊔F,⋄), where (a,b)⋄e=a⋅e if e∈E, and (a,b)⋄e=b⋆e if e∈F.
Tensor. Let C=(A,E,⋅) and D=(B,F,⋆) be Cartesian frames over W. The tensor product of C and D, written C⊗D, is given by C⊗D=(A×B,hom(C,D∗),⋄), where hom(C,D∗) is the set of morphisms (g,h):C→D∗ (i.e., the set of all pairs (g:A→F,h:B→E) such that b⋆g(a)=a⋅h(b) for all a∈A, b∈B), and ⋄ is given by (a,b)⋄(g,h)=b⋆g(a)=a⋅h(b).
Par. Let C=(A,E,⋅) and D=(B,F,⋆) be Cartesian frames over W. C⅋D=(hom(C∗,D),E×F,⋄), where (g,h)⋄(e,f)=g(e)⋆f=h(f)⋅e.
Lollipop. Given two Cartesian frames over W, C=(A,E,⋅) and D=(B,F,⋆), we let C⊸D denote the Cartesian frame C⊸D=(hom(C,D),A×F,⋄), where ⋄ is given by (g,h)⋄(a,f)=g(a)⋆f=a⋅h(f).
3. Frames, Morphisms, and Equivalence Relations
Cartesian frame. A Cartesian frame C over a set W is a triple (A,E,⋅), where A and E are sets and ⋅:A×E→W. If C=(A,E,⋅) is a Cartesian frame over W, we say Agent(C)=A, Env(C)=E, World(C)=W, and Eval(C)=⋅.
Environment subset. Given a Cartesian frame C=(A,E,⋅) over W, and a subset S of W, let ES denote the subset {e∈E|∀a∈A,e⋅a∈S}.
Chu category. Chu(W) is the category whose objects are Cartesian frames over W, whose morphisms from C=(A,E,⋅) to D=(B,F,⋆) are pairs of functions (g:A→B,h:F→E), such that a⋅h(f)=g(a)⋆f for all a∈A and f∈F, and whose composition of morphisms is given by (g1,h1)∘(g0,h0)=(g1∘g0,h0∘h1).
Isomorphism. A morphism (g,h):C→D is an isomorphism if both g and h are bijective. If there is an isomorphism between C and D, we say C≅D.
Homotopic. Two morphisms (g0,h0),(g1,h1):C→D with the same source and target are called homotopic if (g0,h1) is also a morphism.
Homotopy equivalence / biextensional equivalence. C is homotopy equivalent (or biextensionally equivalent) to D, written C≃D, if there exists a pair of morphisms ϕ:C→D and ψ:D→C such that ψ∘ϕ is homotopic to the identity on C and ϕ∘ψ is homotopic to the identity on D.
Sub-sum. Let C=(A,E,⋅), and let D=(B,F,⋆). A sub-sum of C and D is a Cartesian frame of the form (A⊔B,X,⋄), where X⊆Env(C⊕D) and ⋄ is Eval(C⊕D) restricted to (A⊔B)×X, such that C≃(A,X,⋄C) and D≃(B,X,⋄D), where ⋄C is ⋄ restricted to A×X and ⋄D is ⋄ restricted to B×X. Let C⊞D denote the set of all sub-sums of C and D.
Sub-tensor. Let C=(A,E,⋅), and let D=(B,F,⋆). A sub-tensor of C and D is a Cartesian frame of the form (A×B,X,∙), where X⊆Env(C⊗D) and ∙ is Eval(C⊗D) restricted to (A×B)×X, such that C≃(A,B×X,∙C) and D≃(B,A×X,∙D), where ∙C and ∙D are given by a∙C(b,x)=(a,b)∙x and b∙D(a,x)=(a,b)∙x. Let C⊠D denote the set of all sub-tensors of C and D.
4. Functors
Functions between worlds. Given a Cartesian frame C=(A,E,⋅) over W, and a function f:W→V, let f∘(C) denote the Cartesian frame over V, f∘(C)=(A,E,⋆), where a⋆e=f(a⋅e).
Dual. Let −∗:Chu(W)→Chu(W)op be the functor given by (A,E,⋅)∗=(E,A,⋆), where e⋆a=a⋅e, and (g,h)∗=(h,g).
Functor (from functions between worlds). Given two sets W and and V, and a function p:W→V, let p∘:Chu(W)→Chu(V) denote the functor that sends the object (A,E,⋅)∈Chu(W) to the object (A,E,⋆)∈Chu(V), where a⋆e=p(a⋅e), and sends the morphism(g,h) to the morphism with the same underlying functions, (g,h).
Functor (from Cartesian frames). Let C=(V,E,⋅) be a Cartesian frame over W, with Agent(C)=V. Then C∘:Chu(V)→Chu(W) is the functor that sends (B,F,⋆) to (B,F×E,⋄), where b⋄(f,e)=(b⋆f)⋅e, and sends the morphism (g,h) to (g,h′), where h′(f,e)=(h(f),e).
5. Subagents
Subagent (categorical definition). Let C and D be Cartesian frames over W. We say that C is a subagent of D, written C◃D, if for every morphism ϕ:C→⊥ there exists a pair of morphisms ϕ0:C→D and ϕ1:D→⊥ such that ϕ=ϕ1∘ϕ0.
Subagent (currying definition). Let C and D be Cartesian frames over W. We say that C◃D if there exists a Cartesian frame Z over Agent(D) such that C≃D∘(Z).
Subagent (covering definition). Let C=(A,E,⋅) and D=(B,F,⋆) be Cartesian frames over W. We say that C◃D if for all e∈E, there exists an f∈F and a (g,h):C→D such that e=h(f).
Sub-environment. We say C is a sub-environment of D, written C◃∗D, if D∗◃C∗.
5.1. Additive and Multiplicative Subagents
Additive subagent (sub-sum definition). C is an additive subagent of D, written C◃+D, if there exists a C′ and a D′≃D with D′∈C⊞C′.
Additive subagent (brother definition). C′ is called a brother to C in D if D≃D′ for some D′∈C⊞C′. We say C◃+D if C has a brother in D.
Additive subagent (committing definition). Given Cartesian frames C and D over W, we say C◃+D if there exist three sets X, Y, and Z, with X⊆Y, and a function f:Y×Z→W such that C≃(X,Z,⋄) and D≃(Y,Z,∙), where ⋄ and ∙ are given by x⋄z=f(x,z) and y∙z=f(y,z).
Additive subagent (currying definition). We say C◃+D if there exists a Cartesian frame M over Agent(D) with |Env(M)|=1, such that C≃D∘(M).
Additive subagent (categorical definition). We say C◃+D if there exists a single morphism ϕ0:C→D such that for every morphism ϕ:C→⊥ there exists a morphism ϕ1:D→⊥ such that ϕ is homotopic to ϕ1∘ϕ0 .
Multiplicative subagent (sub-tensor definition). C is a multiplicative subagent of D, written C◃×D, if there exists a C′ and D′≃D with D′∈C⊠C′.
Multiplicative subagent (sister definition). C′ is called a sister to C in D if D≃D′ for some D′∈C⊠C′. We say C◃×D if C has a sister in D.
Multiplicative subagent (externalizing definition). Given Cartesian frames C and D over W, we say C◃×D if there exist three sets X, Y, and Z, and a function f:X×Y×Z→W such that C≃(X,Y×Z,⋄) and D≃(X×Y,Z,∙), where ⋄ and ∙ are given by x⋄(y,z)=f(x,y,z) and (x,y)∙z=f(x,y,z).
Multiplicative subagent (currying definition). We say C◃×D if there exists a Cartesian frame M over Agent(D) with Image(M)=Agent(D), such that C≃D∘(M).
Multiplicative subagent (categorical definition). We say C◃×D if for every morphism ϕ:C→⊥, there exist morphisms ϕ0:C→D and ϕ1:D→⊥ such that ϕ≅ϕ1∘ϕ0, and for every morphism ψ:1→D, there exist morphisms ψ0:1→C and ψ1:C→D such that ψ≅ψ1∘ψ0.
Multiplicative subagent (sub-environment definition). We say C◃×D if C◃D and C◃∗D. Equivalently, we say C◃×D if C◃D and D∗◃C∗.
Additive sub-environment. We say C is an additive sub-environment of D, written C◃∗+D, if D∗◃+C∗.
Multiplicative sub-environment. We say C is an multiplicative sub-environment of D, written C◃∗×D, if D∗◃×C∗.
5.2. Ways to Construct Subagents, Sub-Environments, etc.
Committing. Given a set S⊆W and a frame C=(A,E,⋅) over 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}.
Assuming. Given a set S⊆W and a frame C=(A,E,⋅) over 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}.
Externalizing. Given a partition V of W, let v:W→V send each element w∈W to the part that contains it. Given a frame C=(A,E,⋅) over W, 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}.
Internalizing. Given a partition V of W, let v:W→V send each element w∈W to the part that contains it. Given a frame C=(A,E,⋅) over W, 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}.
6. Controllables and Observables
Ensurables (categorical definition).Ensure(C) is the set of all S⊆W such that there exists a morphism ϕ:1S→C.
Preventables (categorical definition). Prevent(C)is the set of all S⊆W such that there exists a morphism ϕ1:1W∖S→C.
Controllables (categorical definition). Let 2S denote the Cartesian frame 1S⊕1W∖S. Ctrl(C) is the set of all S⊆W such that there exists a morphism ϕ:2S→C.
Observables (original categorical definition). Obs(C) is the set of all S⊆W such that there exist C0 and C1 with Image(C0)⊆S and Image(C1)⊆W∖S such that C≃C0&C1.
Observables (definition from subsets). We say that a finite partition V of W is observable in a frame C over W if for all parts Si∈V, Si∈Obs(C). We let Obs′(C) denote the set of all finite partitions of W that are observable in C.
Observables (conditional policies definition): We say that a finite partition V of W is observable in a frame C=(A,E,⋅) over W if for all functions f:V→A, there exists an element af∈A such that for all e∈E, f(v(af⋅e))⋅e=af⋅e, where v:W→V is the function that sends each element of W to its part in V.
Observables (non-constructive additive definition): We say that a finite partition V={S1,…,Sn} of W is observable in a frame C over W if there exist frames C1,⋯Cn over W, with Ci◃⊥Si such that C≃C1&…&Cn.
Observables (constructive additive definition): We say that a finite partition V={S1,…,Sn} of W is observable in a frame C over W if C≃AssumeS1(C)&…&AssumeSn(C).
Powerless outside of a subset: Given a frame C=(A,E,⋅) over W and a subset S of W, we say that C's agent is powerless outside S if for all e∈E and all a0,a1∈A, if a0⋅e∉S, then a0⋅e=a1⋅e.
Observables (non-constructive multiplicative definition): We say that a finite partition V={S1,…,Sn} of W is observable in a frame C over W if C≃C1⊗⋯⊗Cn, where each Ci's agent is powerless outside Si.
Observables (constructive multiplicative definition): We say that a finite partition V={S1,…,Sn} of W is observable in a frame C over W if C≃C1⊗⋯⊗Cn, where Ci=AssumeSi(C)&1Ti, where Ti=(W∖Si)∩Image(C).
Observables (non-constructive internalizing-externalizing definition): We say that a finite partition V of W is observable in a frame C=(A,E,⋅) over W if either A={} or C is biextensionally equivalent to something in the image of ExternalV∘InternalV.
Observables (constructive internalizing-externalizing definition): We say that a finite partition V of W is observable in a frame C=(A,E,⋅) over W if either A={} or C≃ExternalV(InternalV(C)).
This is a list of the main definitions from Scott Garrabrant's Cartesian Frames sequence. (I'll update it as more posts come out.)
1. Small Cartesian Frames
Let W={w0,w1} for the matrix visualizations below. Let C be an arbitrary Cartesian frame.
2. Binary Operations
Sum. For Cartesian frames C=(A,E,⋅) and D=(B,F,⋆) over W, C⊕D is the Cartesian frame (A⊔B,E×F,⋄), where a⋄(e,f)=a⋅e if a∈A, and a⋄(e,f)=a⋆f if a∈B.
Product. For Cartesian frames C=(A,E,⋅) and D=(B,F,⋆) over W, C&D is the Cartesian frame (A×B,E⊔F,⋄), where (a,b)⋄e=a⋅e if e∈E, and (a,b)⋄e=b⋆e if e∈F.
Tensor. Let C=(A,E,⋅) and D=(B,F,⋆) be Cartesian frames over W. The tensor product of C and D, written C⊗D, is given by C⊗D=(A×B,hom(C,D∗),⋄), where hom(C,D∗) is the set of morphisms (g,h):C→D∗ (i.e., the set of all pairs (g:A→F,h:B→E) such that b⋆g(a)=a⋅h(b) for all a∈A, b∈B), and ⋄ is given by (a,b)⋄(g,h)=b⋆g(a)=a⋅h(b).
Par. Let C=(A,E,⋅) and D=(B,F,⋆) be Cartesian frames over W. C⅋ D=(hom(C∗,D),E×F,⋄), where (g,h)⋄(e,f)=g(e)⋆f=h(f)⋅e.
Lollipop. Given two Cartesian frames over W, C=(A,E,⋅) and D=(B,F,⋆), we let C⊸D denote the Cartesian frame C⊸D=(hom(C,D),A×F,⋄), where ⋄ is given by (g,h)⋄(a,f)=g(a)⋆f=a⋅h(f).
3. Frames, Morphisms, and Equivalence Relations
Cartesian frame. A Cartesian frame C over a set W is a triple (A,E,⋅), where A and E are sets and ⋅:A×E→W. If C=(A,E,⋅) is a Cartesian frame over W, we say Agent(C)=A, Env(C)=E, World(C)=W, and Eval(C)=⋅.
Environment subset. Given a Cartesian frame C=(A,E,⋅) over W, and a subset S of W, let ES denote the subset {e∈E | ∀a∈A,e⋅a∈S}.
Cartesian frame image. Image(C)={w∈W | ∃a∈A, ∃e∈E s.t. a⋅e=w}.
Chu category. Chu(W) is the category whose objects are Cartesian frames over W, whose morphisms from C=(A,E,⋅) to D=(B,F,⋆) are pairs of functions (g:A→B,h:F→E), such that a⋅h(f)=g(a)⋆f for all a∈A and f∈F, and whose composition of morphisms is given by (g1,h1)∘(g0,h0)=(g1∘g0,h0∘h1).
Isomorphism. A morphism (g,h):C→D is an isomorphism if both g and h are bijective. If there is an isomorphism between C and D, we say C≅D.
Homotopic. Two morphisms (g0,h0),(g1,h1):C→D with the same source and target are called homotopic if (g0,h1) is also a morphism.
Homotopy equivalence / biextensional equivalence. C is homotopy equivalent (or biextensionally equivalent) to D, written C≃D, if there exists a pair of morphisms ϕ:C→D and ψ:D→C such that ψ∘ϕ is homotopic to the identity on C and ϕ∘ψ is homotopic to the identity on D.
Sub-sum. Let C=(A,E,⋅), and let D=(B,F,⋆). A sub-sum of C and D is a Cartesian frame of the form (A⊔B,X,⋄), where X⊆Env(C⊕D) and ⋄ is Eval(C⊕D) restricted to (A⊔B)×X, such that C≃(A,X,⋄C) and D≃(B,X,⋄D), where ⋄C is ⋄ restricted to A×X and ⋄D is ⋄ restricted to B×X. Let C⊞D denote the set of all sub-sums of C and D.
Sub-tensor. Let C=(A,E,⋅), and let D=(B,F,⋆). A sub-tensor of C and D is a Cartesian frame of the form (A×B,X,∙), where X⊆Env(C⊗D) and ∙ is Eval(C⊗D) restricted to (A×B)×X, such that C≃(A,B×X,∙C) and D≃(B,A×X,∙D), where ∙C and ∙D are given by a∙C(b,x)=(a,b)∙x and b∙D(a,x)=(a,b)∙x. Let C⊠D denote the set of all sub-tensors of C and D.
4. Functors
Functions between worlds. Given a Cartesian frame C=(A,E,⋅) over W, and a function f:W→V, let f∘(C) denote the Cartesian frame over V, f∘(C)=(A,E,⋆), where a⋆e=f(a⋅e).
Dual. Let −∗:Chu(W)→Chu(W)op be the functor given by (A,E,⋅)∗=(E,A,⋆), where e⋆a=a⋅e, and (g,h)∗=(h,g).
Functor (from functions between worlds). Given two sets W and and V, and a function p:W→V, let p∘:Chu(W)→Chu(V) denote the functor that sends the object (A,E,⋅)∈Chu(W) to the object (A,E,⋆)∈Chu(V), where a⋆e=p(a⋅e), and sends the morphism (g,h) to the morphism with the same underlying functions, (g,h).
Functor (from Cartesian frames). Let C=(V,E,⋅) be a Cartesian frame over W, with Agent(C)=V. Then C∘:Chu(V)→Chu(W) is the functor that sends (B,F,⋆) to (B,F×E,⋄), where b⋄(f,e)=(b⋆f)⋅e, and sends the morphism (g,h) to (g,h′), where h′(f,e)=(h(f),e).
5. Subagents
Subagent (categorical definition). Let C and D be Cartesian frames over W. We say that C is a subagent of D, written C◃D, if for every morphism ϕ:C→⊥ there exists a pair of morphisms ϕ0:C→D and ϕ1:D→⊥ such that ϕ=ϕ1∘ϕ0.
Subagent (currying definition). Let C and D be Cartesian frames over W. We say that C◃D if there exists a Cartesian frame Z over Agent(D) such that C≃D∘(Z).
Subagent (covering definition). Let C=(A,E,⋅) and D=(B,F,⋆) be Cartesian frames over W. We say that C◃D if for all e∈E, there exists an f∈F and a (g,h):C→D such that e=h(f).
Sub-environment. We say C is a sub-environment of D, written C◃∗D, if D∗◃C∗.
5.1. Additive and Multiplicative Subagents
Additive subagent (sub-sum definition). C is an additive subagent of D, written C◃+D, if there exists a C′ and a D′≃D with D′∈C⊞C′.
Additive subagent (brother definition). C′ is called a brother to C in D if D≃D′ for some D′∈C⊞C′. We say C◃+D if C has a brother in D.
Additive subagent (committing definition). Given Cartesian frames C and D over W, we say C◃+D if there exist three sets X, Y, and Z, with X⊆Y, and a function f:Y×Z→W such that C≃(X,Z,⋄) and D≃(Y,Z,∙), where ⋄ and ∙ are given by x⋄z=f(x,z) and y∙z=f(y,z).
Additive subagent (currying definition). We say C◃+D if there exists a Cartesian frame M over Agent(D) with |Env(M)|=1, such that C≃D∘(M).
Additive subagent (categorical definition). We say C◃+D if there exists a single morphism ϕ0:C→D such that for every morphism ϕ:C→⊥ there exists a morphism ϕ1:D→⊥ such that ϕ is homotopic to ϕ1∘ϕ0 .
Multiplicative subagent (sub-tensor definition). C is a multiplicative subagent of D, written C◃×D, if there exists a C′ and D′≃D with D′∈C⊠C′.
Multiplicative subagent (sister definition). C′ is called a sister to C in D if D≃D′ for some D′∈C⊠C′. We say C◃×D if C has a sister in D.
Multiplicative subagent (externalizing definition). Given Cartesian frames C and D over W, we say C◃×D if there exist three sets X, Y, and Z, and a function f:X×Y×Z→W such that C≃(X,Y×Z,⋄) and D≃(X×Y,Z,∙), where ⋄ and ∙ are given by x⋄(y,z)=f(x,y,z) and (x,y)∙z=f(x,y,z).
Multiplicative subagent (currying definition). We say C◃×D if there exists a Cartesian frame M over Agent(D) with Image(M)=Agent(D), such that C≃D∘(M).
Multiplicative subagent (categorical definition). We say C◃×D if for every morphism ϕ:C→⊥, there exist morphisms ϕ0:C→D and ϕ1:D→⊥ such that ϕ≅ϕ1∘ϕ0, and for every morphism ψ:1→D, there exist morphisms ψ0:1→C and ψ1:C→D such that ψ≅ψ1∘ψ0.
Multiplicative subagent (sub-environment definition). We say C◃×D if C◃D and C◃∗D. Equivalently, we say C◃×D if C◃D and D∗◃C∗.
Additive sub-environment. We say C is an additive sub-environment of D, written C◃∗+D, if D∗◃+C∗.
Multiplicative sub-environment. We say C is an multiplicative sub-environment of D, written C◃∗×D, if D∗◃×C∗.
5.2. Ways to Construct Subagents, Sub-Environments, etc.
Committing. Given a set S⊆W and a frame C=(A,E,⋅) over 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}.
Assuming. Given a set S⊆W and a frame C=(A,E,⋅) over 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}.
Externalizing. Given a partition V of W, let v:W→V send each element w∈W to the part that contains it. Given a frame C=(A,E,⋅) over W, 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}.
Internalizing. Given a partition V of W, let v:W→V send each element w∈W to the part that contains it. Given a frame C=(A,E,⋅) over W, 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}.
6. Controllables and Observables
Ensurables (categorical definition). Ensure(C) is the set of all S⊆W such that there exists a morphism ϕ:1S→C.
Preventables (categorical definition). Prevent(C) is the set of all S⊆W such that there exists a morphism ϕ1:1W∖S→C.
Controllables (categorical definition). Let 2S denote the Cartesian frame 1S⊕1W∖S. Ctrl(C) is the set of all S⊆W such that there exists a morphism ϕ:2S→C.
Observables (original categorical definition). Obs(C) is the set of all S⊆W such that there exist C0 and C1 with Image(C0)⊆S and Image(C1)⊆W∖S such that C≃C0&C1.
Observables (definition from subsets). We say that a finite partition V of W is observable in a frame C over W if for all parts Si∈V, Si∈Obs(C). We let Obs′(C) denote the set of all finite partitions of W that are observable in C.
Observables (conditional policies definition): We say that a finite partition V of W is observable in a frame C=(A,E,⋅) over W if for all functions f:V→A, there exists an element af∈A such that for all e∈E, f(v(af⋅e))⋅e=af⋅e, where v:W→V is the function that sends each element of W to its part in V.
Observables (non-constructive additive definition): We say that a finite partition V={S1,…,Sn} of W is observable in a frame C over W if there exist frames C1,⋯Cn over W, with Ci◃⊥Si such that C≃C1&…&Cn.
Observables (constructive additive definition): We say that a finite partition V={S1,…,Sn} of W is observable in a frame C over W if C≃AssumeS1(C)&…&AssumeSn(C).
Powerless outside of a subset: Given a frame C=(A,E,⋅) over W and a subset S of W, we say that C's agent is powerless outside S if for all e∈E and all a0,a1∈A, if a0⋅e∉S, then a0⋅e=a1⋅e.
Observables (non-constructive multiplicative definition): We say that a finite partition V={S1,…,Sn} of W is observable in a frame C over W if C≃C1⊗⋯⊗Cn, where each Ci's agent is powerless outside Si.
Observables (constructive multiplicative definition): We say that a finite partition V={S1,…,Sn} of W is observable in a frame C over W if C≃C1⊗⋯⊗Cn, where Ci=AssumeSi(C)&1Ti, where Ti=(W∖Si)∩Image(C).
Observables (non-constructive internalizing-externalizing definition): We say that a finite partition V of W is observable in a frame C=(A,E,⋅) over W if either A={} or C is biextensionally equivalent to something in the image of ExternalV∘InternalV.
Observables (constructive internalizing-externalizing definition): We say that a finite partition V of W is observable in a frame C=(A,E,⋅) over W if either A={} or C≃ExternalV(InternalV(C)).