Spahn effect algebra (Rev #1, changes)

Definition

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

1. Commutativity: $x\perp y$ implies $y\perp x$ and $x\vee y=y\vee x$.

2. Associativity: $y\perp z$ and $x\perp(y\vee z)$ implies $x\perp y$ and $(x\vee y)\perp z$ and $x\vee (y\vee z)=(x\vee y)\vee z$.

3. Zero: $0\perp x$ and $0\vee x=x$

Definition

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

1. $x^\perp\in E$ is the unique element in $E$ with $x\vee x^\perp=1$, where $1=0^\perp$.

2. $x\perp 1\Rightarrow x=0$.

For such an effect algebra one defines:

and

and