A *Church monoid* is a particular type of algebraic mathematical structure that provides semantics for a flavour of relevance logic, a weak form of substructural logic.

A Church monoid is a partially ordered commutative monoid $(M,\circ, 1,\leq)$ that is has a binary operation, “implication”, written $a\to b$ that as an operation $b\mapsto (a\to b)$ is right adjoint to the functor $-\circ a$. Here $M$ is considered as a thin category associated to the underlying poset. Additionally, for all $a\in M$, $a \leq a\circ a$, resulting in a monoidal category with diagonals, where $\circ$ is the monoidal product.

The operation $\circ$ models intensional conjunction, as $\to$ models implication, analogous to linear implication in linear logic.

- relevance monoidal category
- relevance logic
- Ackermann groupoid (where “groupoid” means magma)
- Heyting algebra

Church monoids were introduced in

- Robert K. Meyer,
*Conservative extension in relevant implication*, Studia Logica volume 31 (1973) pp39–46, doi:10.1007/BF02120525

and named for Alonzo Church.

Last revised on April 30, 2021 at 07:03:38. See the history of this page for a list of all contributions to it.