nLab Church monoid

Contents

Contents

Idea

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.

Definition

A Church monoid is a partially ordered commutative monoid (M,,1,)(M,\circ, 1,\leq) that is has a binary operation, “implication”, written aba\to b that as an operation b(ab)b\mapsto (a\to b) is right adjoint to the functor a-\circ a. Here MM is considered as a thin category associated to the underlying poset. Additionally, for all aMa\in M, aaaa \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.

References

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.