The idea of a closed midpoint algebra comes from Peter Freyd.

Definition

A closed midpoint algebra is a cancellative midpoint algebra$(M,\vert)$ equipped with two chosen elements $\bot:M$ and $\top:M$.

Examples

The unit interval with $a \vert b \coloneqq \frac{a + b}{2}$, $\bot = 0$, and $\top = 1$ is an example of a closed midpoint algebra.

The set of truth values in Girard’s linear logic is a closed midpoint algebra.

Properties

Every closed midpoint algebra with $\bot = \top$ is trivial.

Partial order

Every closed midpoint algebra has a natural partial order defined as $a \leq b$ for elements $a$ and $b$ in $M$ if there exists $c$ in $M$ such that $a \vert \top = b \vert c$. Dually, $a \leq b$ for elements $a$ and $b$ in $M$ if there exists $c$ in $M$ such that $c \vert a = \bot \vert b$.

For any set $S$ and any closed midpoint algebra $M$, the set of functions from $S$ to $M$ is a closed midpoint algebra $(S\to M,\vert_{S\to M},\bot_{S\to M},\top_{S\to M})$, defined by

$(f\vert_{S\to M} g)(x) = f(x)\vert_M g(x)$ for all $f,g:S\to M$ and $x:M$

$(\bot_{S\to M})(x) = \bot_M$ for all $x:M$

$(\top_{S\to M})(x) = \top_M$ for all $x:M$

Definite integration

Let $M$ and $N$ be continuous closed midpoint algebras and let $M\to_C N$ be the space of continuous functions from $M$ to $N$. Then there exists an operator$\int (-)(x) \mathrm{d}x: (M\to_C N)\to (M\to_C N)$ called definite integration such that

When $M$ is the unit interval on the real numbers$[0,1]$, and $N$ is an interval $[a,b]$ on the real numbers, written in conventional notation the axioms become: