% Problem: Near-rings and inverse semigroups % Status: Challenge Problem % % Theorem: Let (R,+,*) be a (right) near-ring such that % (R,*) is an inverse semigroup. Then + is commutative. % % There is a high-level proof in % % S. J. Mahmood, J. D. P. Meldrum and L. O'Carroll, % Inverse semigroups and near-rings, % J. London Math. Soc. 23 (1981), 45-60. % % They show that the multiplicative semigroup of a near-ring is an % inverse semigroup if and only if the near-ring is a subdirect product % of near-fields. The addition in a near-field is well-known to be commutative. % % The formulation below is not "minimal". There are some clauses which are % easy consequences of the rest just to move things along. % % Working with right near-fields instead of left near-fields is just a matter % of taste. The problem seems to be hard in either version. % % For using proof sketches, it might be helpful to first find a proof for % near-fields. However, this will make the problem non-Horn. Here are the % additional axioms for a near-field: % x != 0 -> x * x' = 1. % x != 0 -> x' * x = 1. % %%%%%%%%%%%%%%%%%%%%%%% formulas(assumptions). % (R,+,0) is a group 0 + x = x. x + 0 = x. x + -x = 0. -x + x = 0. (x + y) + z = x + (y + z). % (R,*,1) is an inverse (hence, Clifford) monoid 1 * x = x. x * 1 = x. (x * y) * z = x * (y * z). x * (x' * x) = x. x'' = x. x * x' = x' * x. (x * y)' = y' * x'. (x * x') * y = y * (x * x'). % right distributive law (y * x) + (z * x) = (y + z) * x. x * 0 = 0. 0 * x = 0. end_of_list. formulas(goals). x + y = y + x. end_of_list.