nLab closed midpoint algebra




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


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


The unit interval with a|ba+b2a \vert b \coloneqq \frac{a + b}{2}, =0\bot = 0, and =1\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.


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

Partial order

Every closed midpoint algebra has a natural partial order defined as aba \leq b for elements aa and bb in MM if there exists cc in MM such that a|=b|ca \vert \top = b \vert c. Dually, aba \leq b for elements aa and bb in MM if there exists cc in MM such that c|a=|bc \vert a = \bot \vert b.

Every closed midpoint algebra homomorphism is a monotone.

Function algebras

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

  • (f| SMg)(x)=f(x)| Mg(x)(f\vert_{S\to M} g)(x) = f(x)\vert_M g(x) for all f,g:SMf,g:S\to M and x:Mx:M

  • ( SM)(x)= M(\bot_{S\to M})(x) = \bot_M for all x:Mx:M

  • ( SM)(x)= M(\top_{S\to M})(x) = \top_M for all x:Mx:M

Definite integration

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

MN(x)dx= N\int \top_{M\to N}(x) \mathrm{d}x = \top_N
MN(x)dx= N\int \bot_{M\to N}(x) \mathrm{d}x = \bot_N
f(x)| Ng(x)dx=f(x)dx| Ng(x)dx\int f(x) \vert_N g(x) \mathrm{d}x = \int f(x) \mathrm{d}x \vert_N \int g(x) \mathrm{d}x
f(x)dx=f( M| Mx)dx| Nf(x| M M)dx\int f(x) \mathrm{d}x = \int f(\bot_M \vert_M x) \mathrm{d}x \vert_N \int f(x \vert_M \top_M) \mathrm{d}x

for all xx in MM.

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

0 1a(x)dx=a\int_{0}^{1} a(x) \mathrm{d}x = a
0 1b(x)dx=b\int_{0}^{1} b(x) \mathrm{d}x = b
0 1f(x)+g(x)2dx= 0 1f(x)dx+ 0 1g(x)dx2\int_{0}^{1} \frac{f(x) + g(x)}{2} \mathrm{d}x = \frac{\int_{0}^{1} f(x) \mathrm{d}x + \int_{0}^{1} g(x) \mathrm{d}x}{2}
0 1f(x)dx= 0 1f(0+x2)dx+ 0 1f(x+12)dx2\int_{0}^{1} f(x) \mathrm{d}x = \frac{\int_{0}^{1} f(\frac{0 + x}{2}) \mathrm{d}x + \int_{0}^{1} f(\frac{x + 1}{2}) \mathrm{d}x}{2}


  • Peter Freyd, Algebraic real analysis, Theory and Applications of Categories, Vol. 20, 2008, No. 10, pp 215-306 (tac:20-10)

Last revised on June 16, 2021 at 02:03:37. See the history of this page for a list of all contributions to it.