Spahn effect algebra

Definition

Definition (p.22)

A partial commutative monoid (PCM) consists of a set MM with a zero element 0∈M0 \in M and a partial binary operation ∨:M×M→M\vee : M \times M \to M satisfying the three requirements below. They involve the notation x⊥yx \perp y for: x∨yx \vee y is defined; in that case x,yx, y are called orthogonal.

  1. Commutativity: x⊥yx\perp y implies y⊥xy\perp x and x∨y=y∨xx\vee y=y\vee x.

  2. Associativity: y⊥zy\perp z and x⊥(y∨z)x\perp(y\vee z) implies x⊥yx\perp y and (x∨y)⊥z(x\vee y)\perp z and x∨(y∨z)=(x∨y)∨zx\vee (y\vee z)=(x\vee y)\vee z.

  3. Zero: 0⊥x0\perp x and 0∨x=x0\vee x=x

Definition (p. 23)

An effect algebra is a PCM (E,0,∨)(E,0,\vee) with an orthocomplement. The latter is a unary operation (−) ⊥:E→E(-)^\perp :E\to E satisfying:

  1. x ⊥∈Ex^\perp\in E is the unique element in EE with x∨x ⊥=1x\vee x^\perp=1, where 1=0 ⊥1=0^\perp.

  2. x⊥1⇒x=0x\perp 1\Rightarrow x=0.

For such an effect algebra one defines:

x∧y:=(x ⊥∨y ⊥) ⊥x\wedge y:=(x^\perp\vee y^\perp)^\perp

and

x≤y:⇔∃ z.x∨z=yx\le y:\Leftrightarrow \exists_z.x\vee z=y

and

y⊖x=z:⇔y=x∨zy\ominus x=z:\Leftrightarrow y=x\vee z
Remark (p.25)

If we consider

(−)⊖y:up(y)→down(y ⊥)(-)\ominus y:up(y)\to down(y^\perp)

and

(−)∨y:down(y ⊥)→up(-)\vee y:down(y^\perp)\to up

as functors between posets we have adjunctions

((−∧y)⊣(−⊖y)⊣(−∧y)((-\wedge y)\dashv (-\ominus y)\dashv (-\wedge y)

Hence these functors are a frobenius pair.

Application

In new directions the approach to categorical logic where the substrate carrying the logical notions are Heyting algebras of subobjects in a topos is replaced by a new one where the substrate is effect algebras (of predicates) in extensive categories (extensive category).

Reference