The monus a − b of two elements a and b (also written with a dot above the minus sign, a ∸ b) is defined in certain commutative monoids M such that the relation defined by b ≤ a if and only if there is another element c such that b + c = a is a partial order. Since this relation is a preorder in every monoid, the condition amounts to saying that the relation is antisymmetric, i.e. if a ≤ b and b ≤ a then a = b. If for any b ≤ a there exists a unique least c such that b + c = a, then M is called a commutative monoid with monus.
In a commutative monoid with monus, the monus a − b of any two elements a and b is defined as follows:
- a − b = the least c such that b + c = a, if b ≤ a,
- a − b = 0 otherwise.
For example the natural numbers including 0 form commutative monoid with monus, the order ≤ being the usual order. In this case the monus of a and b can be defined with reference to the ordinary subtraction of integers as max(a − b, 0). The latter definition is commonly encountered in computability theory.