=Paper=
{{Paper
|id=Vol-3754/paper11
|storemode=property
|title=First-order theorem proving with power maps in semigroups
|pdfUrl=https://ceur-ws.org/Vol-3754/paper11.pdf
|volume=Vol-3754
|authors=Yi Lin,Ranganathan Padmanabhan,Yang Zhang
|dblpUrl=https://dblp.org/rec/conf/sycss/LinPZ24
}}
==First-order theorem proving with power maps in semigroups==
https://ceur-ws.org/Vol-3754/paper11.pdf
First-Order Theorem Proving with Power Maps in
Semigroups⋆
Yi Lin1,† , Ranganathan Padmanabhan2,† and Yang Zhang3,∗,†
1
Department of Mathematics, The Ohio State University, Ohio, USA
2
Department of Mathematics, University of Manitoba, Winnipeg, MB, Canada
3
Department of Mathematics, University of Manitoba, Winnipeg, MB, Canada
Abstract
This paper deals with automated deduction techniques to prove and generalize some well-known theorems in
group theory that involve power maps, i.e., functions of the form 𝑓 (𝑥) = 𝑥 𝑛 . Here, the main obstacle is that if
𝑛 is interpreted as an integer variable, then these results are not expressible in first-order logic with equality.
The strategy followed here is to look at the classical proofs, involving the integer variable 𝑛, and see what
specific first-order properties of power maps that are needed in the proofs. Then we implement these first-order
properties of power maps in a theorem prover Prover9 and demonstrate that a well-designed reformulation makes
specific mathematical theories accessible to the modern first-order theorem-proving software, allowing even for
generalizations of the classical results.
Keywords
Semigroup, Prover9, Power maps
1. Introduction
The theory of groups and that of semigroups are very closely related. In fact, every group is a cancellation
semigroup and, by a classical theorem of O. Ore [14], every cancellation semigroup satisfying some
nontrivial identity, say 𝑓 (𝑥, 𝑦) = 𝑔(𝑥, 𝑦), is embeddable in a group. Also, there are several examples of
identities 𝑓 = 𝑔 which are preserved during this process of expansion. The most well-known example
of a semigroup law that is transferable to groups is, of course, the commutative law. A.I. Mal’cev [8]
and B.H. Neumann [12] have shown independently that nilpotent semigroup laws are transferable.
However, it is also known that not all semigroup laws are preserved under the Ore extension. This
raises the important question of finding more (and possibly all) transferable semigroup laws. This
problem was raised by G.M. Bergman ([1, 2]).
There are several transferability theorems in semigroups that involve power maps 𝑓 (𝑥) = 𝑥 𝑛 . For
example, it is known that every cancellation semigroup satisfying 𝑥 𝑛 ⋅ 𝑦 𝑛 = 𝑦 𝑛 ⋅ 𝑥 𝑛 can be embedded
in a group satisfying the same identity. Such statements belong to first-order logic with equality and
hence provable, in principle, by any first-order theorem prover. However, because of the presence of an
arbitrary integer parameter 𝑛 in the exponent, they are outside the scope of any first-order theorem
prover. In particular, one cannot use such an automated reasoning system to prove theorems involving
power maps. Here we focus just on the needed properties of power map 𝑓 (𝑥) = 𝑥 𝑛 and show how
one can easily avoid having to reason explicitly with integer exponents. Implementing these new
equational rules of power maps, we show how a theorem prover can be a handy tool for quickly proving
or confirming the truth of such theorems involving power maps without explicitly mentioning the
integer variable 𝑛.
Following Macedonska [7], a positive semigroup law is said to be transferable if being satisfied in a
cancellative semigroup 𝑆 it must be satisfied in 𝑆𝑆 −1 , the group of right quotients of 𝑆. The most well-
SCSS 2024: The 10th International Symposium on Symbolic Computation in Software Science, August 28–30, Tokyo, Japan
∗
Corresponding author.
†
These authors contributed equally.
Envelope-Open yilinmaths@gmail.com (Y. Lin); Ranganathan.Padmanabhan@umanitoba.ca (R. Padmanabhan);
Yang.Zhang@umanitoba.ca (Y. Zhang)
© 2024 Copyright for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0).
CEUR
ceur-ws.org
Workshop ISSN 1613-0073
Proceedings
63
known example of a transferable law is, of course, the commutative law. A. I. Malcev, B. H. Neumann
and others ([8, 12]) have shown that nilpotent identities are transferable. Macedonska [7] has proved
the transferablity of several two-variable semigroup laws. These identities are defined by using power
maps 𝑓 (𝑥) = 𝑥 𝑛 in semigroups.
Here we will replace the power map by power-like functions and prove their transferability. The
transferability of identities is first order problem but first-order theorem provers cannot handle
power-maps because of the presence of an integer variable “𝑛”. Here we demonstrate that computers
can prove these semigroup implications, thus generalizing what is known classically.
A motivating example: It is well-known that in groups, the commutators [𝑥, 𝑦] can be expressed in a
product of three squares, that is,
[𝑥, 𝑦] = 𝑥 −1 𝑦 −1 𝑥𝑦 = (𝑥 −1 )2 ⋅ (𝑥𝑦 −1 )2 ⋅ 𝑦 2 ,
and hence 𝑥 2 𝑦 = 𝑦𝑥 2 implies [𝑥, 𝑦] is central, which is equivalent to the semigroup implication
𝑥 2 𝑦 = 𝑦𝑥 2 ⟹ 𝑥𝑦𝑧𝑦𝑥 = 𝑦𝑥𝑧𝑥𝑦.
Definition 1.1. A cancellation semigroup (𝐺, ⋅) is a semigroup with the two-sided cancellative proper-
ties, i.e., for all 𝑥, 𝑦, 𝑧 ∈ 𝐺, the following are true:
(i) 𝑥 ⋅ 𝑦 = 𝑥 ⋅ 𝑧 implies 𝑦 = 𝑧,
(ii) 𝑥 ⋅ 𝑦 = 𝑧 ⋅ 𝑦 implies 𝑥 = 𝑧.
Some properties of cancellation semigroup can be found in, for example, [4, 5, 13, 7, 16, 17]. Here we
show that the above implication is valid in cancellation semigroups:
𝑦 ⋅ 𝑦𝑥𝑧𝑥𝑦 ⋅ 𝑥 = 𝑦 2 𝑥𝑧𝑥𝑦𝑥
= 𝑥𝑧𝑦 2 𝑥𝑦𝑥
= 𝑥𝑧𝑦 ⋅ (𝑦𝑥)2
= (𝑦𝑥)2 𝑥𝑧𝑦
= 𝑦𝑥𝑦𝑥 2 𝑧𝑦
= 𝑦𝑥𝑦𝑧𝑦𝑥 2
= 𝑦 ⋅ 𝑥𝑦𝑧𝑦𝑥 ⋅ 𝑥.
Canceling 𝑦 and 𝑥, we have 𝑥𝑦𝑧𝑦𝑥 = 𝑦𝑥𝑧𝑥𝑦.
Next we present the proof by using Prover9 [9].
%% INPUT file
%% In groups, squares are central ==> commutators are also central
(x * y) * z = x * (y * z).
x * e = x.
x * x' = e.
x * y = (y * x) * [x, y]. %% commutators defined
x * (y * y) = (y * y) * x. %% squares are central
%% goal to prove that commutators are central
x * [y, z] = [y, z] * x.
=============== PROOF =================================
1 x * [y,z] = [y,z] * x # label(non_clause) # label(goal).
2 (x * y) * z = x * (y * z). [].
3 x * e = x. [].
4 x * x' = e. [].
5 x * y = (y * x) * [x,y]. [].
64
6 x * (y * [y,x]) = y * x. [5,2].
7 x * (y * y) = (y * y) * x. [].
8 x * (y * y) = y * (y * x). [7,2].
9 [c2,c3] * c1 != c1 * [c2,c3]. [1].
10 x * (e * y) = x * y. [3,2].
11 x * (x' * y) = e * y. [4,2].
12 x * (y * (x * y)') = e. [4,2].
13 x * (y * ([y,x] * z)) = y * (x * z). [6,2,2,2].
14 x * (y * (z * [z,x * y])) = z * (x * y). [6,2].
15 x * (y * (z * [y * z,x])) = y * (z * x). [2,6,2].
16 x * (y * (y * z)) = y * (y * (x * z)). [8,2,2,2,2].
20 e * x = x. [3,8,3,10].
21 x * (x' * y) = y. [11,20].
29 x'' = x. [4,21,3].
31 x * [x,y'] = y * (x * y'). [6,21].
33 x * (y * (x' * x')) = x' * y. [8,21].
35 x' * x = e. [29,4].
36 x' * (x * y) = y. [29,21].
40 x * (y * [x,y]') = y * x. [4,13,3].
41 x * (y * (z * [z,[x,y]])) = y * (x * (z * [x,y])).[6,13].
43 x * (y * (z * (z * [y,x]))) = y * (x * (z * z)). [8,13].
55 x' * (y * x) = y * [y,x]. [6,36].
58 x * (y * x)' = y'. [12,36,3].
66 x * (y * [y,z' * x]) = z * (y * (z' * x)). [14,21].
80 x*(y *(z*(u*[y*(z*u),x])))=y*(z*(u*x)).[2,15,2,2].
98 (x * y)' = y' * x'. [58,36].
112 x * (y * (z * (z * u))) = z * (z * (x * (y * u))).[16,2,2].
115 x * (x * (y * x')) = y * x. [4,16,3].
127 x * (y * (x' * (x' * z))) = x' * (y * z). [16,21].
128 x * (x * (y * (x' * z))) = y * (x * z). [21,16].
189 x * (x * (y * (z * x'))) = y * (z * x). [2,115,2].
190 x' * (y * x) = x * (y * x'). [115,21,29].
206 x * [x,y] = y * (x * y'). [55,190].
326 x' * (y * (x * z)) = x * (y * (x' * z)). [190,2,2,2,2].
467 x * (y' * [y,x]) = y' * x. [33,13,33].
481 x * [y,x]' = y * (x * y'). [40,36,190].
512 x * (y * (x' * y')) = [x',y']. [31,21].
516 [x',y'] = [x,y']. [31,36,326,512].
543 x * (y * (x' * y')) = [x,y']. [512,516].
547 [x',y] = [x,y']. [206,21,543].
551 [x,y'] = [x,y]. [206,36,326,543].
552 x' * (y * [y,x]) = y * x'. [206,36].
569 x * [y,x] = y * (x * y').
[206,190,98,29,2,36,98,29,2,36].
584 [x',y] = [x,y]. [547,551].
585 x * (y * (x' * y')) = [x,y]. [543,551].
592 x' * (y * ([y,x] * z)) = y * (x' * z). [551,13].
605 x * (y * [x,y]) = y * x. [569,8,8,115].
606 [x,y] = [y,x]. [569,21,585,551].
754 x * (y' * [x,y]) = y' * x. [551,605].
1004 [x,y]' = [y,x]. [481,21,585,551].
1049 x * [y,[x,y]] = x. [21,41,584,754,21].
65
1095 [x,[y,x]] = e. [1049,21,4,584].
1157 [x,y' * (y' * x')] = e.
[35,43,98,98,2,98,98,2,606,2,2,326,36,36,21].
1383 [x,x * (y * y)] = e. [1157,551,98,98,29,29,29,2].
1387 [x,y * (y * x)] = e. [8,1383].
1400 [x * y,x' * y] = e. [21,1387,606].
1534 [x * (y * z),x * (y' * z)] = e. [13,1400,592].
1861 x * (y * (x' * (y' * z))) = [x,y] * z. [585,2,2,2].
1863 x * (y * (z * (x' * (z' * y')))) = [x,y * z].[2,585,98].
1874 x * ([y,z] * (x' * [z,y])) = [x,[y,z]]. [1004,585].
1903 [x,y' * x] = [y,x]. [66,21,190,585,584].
2118 [x,y * x] = [y,x]. [29,1903,584].
2121 [x,x * y] = [x,y]. [36,1903,606,2118].
2148 [x' * y,[x,y]] = e. [1903,1095].
2195 [x * y,[x,y]] = e. [2118,1095].
2365 [x * y,y * x] = e. [2195,2121,2,605].
2384 [x * y,x' * y'] = e. [2365,551,98].
2592 [x,y] * (y' * x) = x * y'.
[2148,467,98,29,3,98,29,2,552].
2674 x' * (y' * (z * (x * (z' * y)))) = [x,z * y].
[2384,80,98,3,2,2,326,98,1863].
3912 x*(y*(z*(x'*(x'*u))))=x'*(y*(z*u)).[112,21].
4517 [x,[y,z]] * ([z,y] * x) = x * [z,y]. [1004,2592,1004].
8121 x*(y*(x'*(z*(x'*z'))))=x'*(y*[x,z]). [206,127,584].
8175 x'*(y*(z*(x*u)))=x*(y*(z*(x'*u))). [128,127,29].
8179 x'*(y*(z*(u*x)))=x*(y*(z*(u*x'))). [189,127,29].
8223 [x,y * z] = [x,z * y]. [2674,8179,8175,1863].
8383 [x * (y * z),y' * (z * x)] = e. [8223,1534,2].
13972 [x,[y,z]] = e. [8383,585,98,98,2,98,98,29,2,2,2,8179,
2,2,3912,8121,2,2,1861,1874].
14283 [x,y] * z = z * [x,y]. [4517,13972,20].
14284 $F. [14283,9].
====================== end of proof ==========================
Coda: In the human proof above, we already ”knew” that commutators are expressible as a product of
squares in the group and hence the human proof was almost trivial. But in the above machine proof of
the same fact, the Prover9 is not even ”aware” of the fact that commutators are products of squares. Still,
the software did prove the centrality of commutators as explicitly shown in line #14283 above (proved
with the Knuth-Bendix option). Dr. William McCune, the author of Prover9, has done a great job.
In this paper, we first consider the implication (𝑥𝑦)𝑛 = (𝑦𝑥)𝑛 in cancellation semigroups. In Section 2,
we prove that this implication is equivalent to the identity 𝑥𝑦 𝑛 = 𝑦 𝑛 𝑥 in all cancellation semigroups by
replacing the power-map 𝑥 𝑛 by a weaker power-like function 𝑓 (𝑥). Furthermore, we discuss a general
extension. In Section 3, we prove that 𝑥𝑦 𝑛 = 𝑦 𝑛 𝑥 is transferable.
2. Power map properties
We first list some properties of power maps. We refer the readers to [11, 15] for more details.
Lemma 2.1. Let (𝑆; ⋅) be a cancellation semigroup and let 𝑓 ∶ 𝑆 → 𝑆 be the usual power map 𝑓 (𝑥) = 𝑥 𝑛 ,
for some 𝑛 > 1. Assume that 𝑓 (𝑥 ⋅ 𝑦) = 𝑓 (𝑦 ⋅ 𝑥). Then the function 𝑓 (𝑥) satisfies the following:
(1) 𝑥 ⋅ 𝑓 (𝑥) = 𝑓 (𝑥) ⋅ 𝑥.
(2) 𝑥 ⋅ 𝑓 (𝑦 ⋅ 𝑥) = 𝑓 (𝑥 ⋅ 𝑦) ⋅ 𝑥.
66
(3) 𝑥 and 𝑓 (𝑓 (𝑥)) commute.
(4) If 𝑥 and 𝑦 commute then 𝑓 (𝑥 ⋅ 𝑦) = 𝑓 (𝑥) ⋅ 𝑓 (𝑦).
(5) 𝑥 and 𝑓 (𝑦 ⋅ 𝑥) commute.
(6) 𝑥 and 𝑓 (𝑓 (𝑥) ⋅ 𝑦) commute.
Proof. (1) is obvious since both sides are equal to 𝑥 𝑛+1 .
(2) 𝑥 ⋅ 𝑓 (𝑦 ⋅ 𝑥) = 𝑥 ⋅ (𝑦 ⋅ 𝑥)𝑛 = (𝑥 ⋅ 𝑦)𝑛 ⋅ 𝑥 = 𝑓 (𝑥 ⋅ 𝑦) ⋅ 𝑥.
(3) follows that 𝑓 (𝑓 (𝑥)) is just a power of 𝑥 and hence commutes with 𝑥.
(4) is obvious thanks to associativity and commutativity.
(5) 𝑥 ⋅ 𝑓 (𝑦 ⋅ 𝑥) = 𝑓 (𝑥 ⋅ 𝑦) ⋅ 𝑥 = 𝑓 (𝑦 ⋅ 𝑥) ⋅ 𝑥 since 𝑓 (𝑥 ⋅ 𝑦) = 𝑓 (𝑦 ⋅ 𝑥).
(6)
𝑓 (𝑓 (𝑥) ⋅ 𝑦) ⋅ 𝑥 = 𝑓 (𝑔(𝑥) ⋅ 𝑥 ⋅ 𝑦) ⋅ 𝑥 where 𝑔(𝑥) = 𝑥 𝑛−1
= 𝑓 (𝑥 ⋅ 𝑦 ⋅ 𝑔(𝑥)) ⋅ 𝑥 since 𝑓 (𝑥 ⋅ 𝑦) = 𝑓 (𝑦 ⋅ 𝑥)
= 𝑥 ⋅ 𝑓 (𝑦 ⋅ 𝑔(𝑥) ⋅ 𝑥) by (2) above
= 𝑥 ⋅ 𝑓 (𝑦 ⋅ 𝑓 (𝑥)) since 𝑓 (𝑥) = 𝑔(𝑥) ⋅ 𝑥
= 𝑥 ⋅ 𝑓 (𝑓 (𝑥) ⋅ 𝑦) since 𝑓 (𝑥 ⋅ 𝑦) = 𝑓 (𝑦 ⋅ 𝑥)
Hence the two elements 𝑥 and 𝑓 (𝑓 (𝑥) ⋅ 𝑦) commute. In particular, the two terms 𝑦 ⋅ 𝑥 and 𝑓 (𝑓 (𝑦 ⋅ 𝑥) ⋅ 𝑥)
commute.
Following the terminology of [11, 15], we call the unary functions 𝑓 (𝑥) satisfying first-order properties
(1) to (4) of Lemma 2.1 as power-like functions.
Theorem 2.2. Let 𝑆 be a cancellation semigroup and let 𝑓 ∶ 𝑆 → 𝑆 be a power-like function and assume
that 𝑓 (𝑥 ⋅ 𝑦) = 𝑓 (𝑦 ⋅ 𝑥). Then 𝑓 (𝑥) is a central element in 𝑆.
We can prove this theorem by using our method and Prover9. Here we list the a few lines of output
of Prover9 which include the conditions and the final result.
========================== prooftrans ===========================
Prover9 (32) version Dec-2007, Dec 2007.
Process 916 was started by yangzhang
on yangzhangsimac2.ad.umanitoba.ca,
Tue Mar 19 12:26:28 2024
The command was "/Users/yangzhang/Desktop/Prover9-Mace4-v05B.app/
Contents/Resources/bin-mac-intel/prover9".
=========================== end of head =========================
========================== end of input =========================
========================= PROOF =================================
% -------- Comments from original proof --------
% Proof 1 at 0.84 (+ 0.02) seconds.
% Length of proof is 24.
% Level of proof is 6.
% Maximum clause weight is 29.
% Given clauses 117.
1 f(x) * y = y * f(x) # label(non_clause) # label(goal). [goal].
2 (x * y) * z = x * (y * z). [assumption].
3 x * y != x * z | y = z. [assumption].
4 x * y != z * y | x = z. [assumption].
5 f(x * y) = f(y * x). [assumption].
6 f(x * y) * x = x * f(y * x). [assumption].
7 f(x) * x = x * f(x). [assumption].
67
8 f(f(x) * y) * x = x * f(f(x) * y). [assumption].
9 x * y != y * x | f(x * y) = f(x) * f(y). [assumption].
10 f(c1) * c2 != c2 * f(c1). [deny(1)].
...........
...........
3645 f(f(x)) * x = x * f(f(x)). [hyper(351,a,139,a),flip(a)].
3699 f(x)*(f(x)*(y*f(f(f(x)*y))))=f(x)*(y*(f(x)*f(f(f(x)*y)))).
[back_rewrite(395),rewrite([3645(8),2(8)])].
3700 $F. [resolve(3699,a,67,a)].
======================== end of proof ==========================
Next, we give the human proof as follows:
𝑓 (𝑥) ⋅ 𝑦 ⋅ 𝑥 ⋅ 𝑓 (𝑓 (𝑦 ⋅ 𝑥))
= 𝑓 (𝑥) ⋅ 𝑓 (𝑓 (𝑦 ⋅ 𝑥)) ⋅ 𝑦 ⋅ 𝑥 since 𝑢 and 𝑓 (𝑓 (𝑢)) commute
= 𝑓 (𝑥 ⋅ 𝑓 (𝑦 ⋅ 𝑥)) ⋅ 𝑦 ⋅ 𝑥 since 𝑥 and 𝑓 (𝑦 ⋅ 𝑥) commute
= 𝑓 (𝑓 (⋅𝑥) ⋅ 𝑥) ⋅ (𝑦 ⋅ 𝑥) since 𝑓 (𝑥 ⋅ 𝑦) = 𝑓 (𝑦 ⋅ 𝑥)
= (𝑦 ⋅ 𝑥) ⋅ 𝑓 (𝑓 (𝑦 ⋅ 𝑥) ⋅ 𝑥) since 𝑦 ⋅ 𝑥 and 𝑓 (𝑓 (𝑦 ⋅ 𝑥) ⋅ 𝑥) commute.
= 𝑦 ⋅ 𝑥 ⋅ 𝑓 (𝑥 ⋅ 𝑓 (𝑦 ⋅ 𝑥)) since 𝑓 (𝑥 ⋅ 𝑦) = 𝑓 (𝑦 ⋅ 𝑥)
= 𝑦 ⋅ 𝑥 ⋅ 𝑓 (𝑥) ⋅ 𝑓 (𝑓 (𝑦 ⋅ 𝑥)) since 𝑥 and 𝑓 (𝑦 ⋅ 𝑥) commute
= 𝑦 ⋅ 𝑓 (𝑥) ⋅ 𝑥 ⋅ 𝑓 (𝑓 (𝑦 ⋅ 𝑥)) since 𝑥 and 𝑓 (𝑥) commute
Hence, we have
𝑓 (𝑥) ⋅ 𝑦 ⋅ 𝑥 ⋅ 𝑓 (𝑓 (𝑦 ⋅ 𝑥)) = 𝑦 ⋅ 𝑓 (𝑥) ⋅ 𝑥 ⋅ 𝑓 (𝑓 (𝑦 ⋅ 𝑥)).
Finally, cancelling the common term 𝑥 ⋅ 𝑓 (𝑓 (𝑦 ⋅ 𝑥)) from the right sides, we get 𝑓 (𝑥) ⋅ 𝑦 = 𝑦 ⋅ 𝑓 (𝑥).
Corollary 2.3. In a cancellation semigroup (𝑆, ⋅), for 𝑥, 𝑦 ∈ 𝑆 and 𝑛 ∈ ℤ+ , (𝑥 ⋅ 𝑦)𝑛 = (𝑦 ⋅ 𝑥)𝑛 implies
𝑥 𝑛 ⋅ 𝑦 = 𝑦 ⋅ 𝑥 𝑛.
Proof. Simply take 𝑓 (𝑥) = 𝑥 𝑛 . The power map 𝑓 (𝑥) = 𝑥 𝑛 satisfies all the six properties mentioned in
Lemma 2.1 and hence the proof of Theorem 2.2 applies. Therefore, the n-th powers are central in the
semigroup, i.e., 𝑥 𝑛 ⋅ 𝑦 = 𝑦 ⋅ 𝑥 𝑛 .
Next we consider the following more general case.
Theorem 2.4. In a cancellation semigroup 𝑆, if there exist 𝑘 ≥ 2, 𝑛 ∈ ℤ+ such that (𝑎1 𝑎2 ⋯ 𝑎𝑘 )𝑛 =
(𝑎𝑘 ⋯ 𝑎2 𝑎1 )𝑛 for any 𝑎𝑖 ∈ 𝑆 holds, then 𝑥 𝑛 is central in 𝑆 for any 𝑥 ∈ 𝑆.
Proof. When 𝑛 = 1, all the situations can be reduced to 𝑘 = 2 or 𝑘 = 3.
In case of 𝑛 = 1 and 𝑘 = 2, we have 𝑎1 𝑎2 = 𝑎2 𝑎1 , and then 𝑆 is commutative.
In case of 𝑛 = 1 and 𝑘 = 3, we have 𝑎1 𝑎2 𝑎3 = 𝑎3 𝑎2 𝑎1 . Then, for any 𝑥, 𝑦, 𝑧, 𝑢 ∈ 𝑆,
𝑥𝑦𝑧𝑢 = 𝑢𝑧𝑥𝑦 = 𝑦𝑧𝑥𝑢.
Cancelling 𝑢 from the right sides, we obtain 𝑥𝑦𝑧 = 𝑦𝑧𝑥. By the condition, 𝑦𝑧𝑥 = 𝑥𝑧𝑦. Then 𝑥𝑦𝑧 = 𝑥𝑧𝑦,
and thus 𝑦𝑧 = 𝑧𝑦. Hence 𝑆 is commutative.
Next, we consider 𝑛 ≥ 2. Note that
𝑥 ⋅ (𝑥𝑦 𝑘−1 )𝑛 = 𝑥 ⋅ (𝑥 ⋅ 𝑦 ⋯ 𝑦)𝑛
= 𝑥 ⋅ (𝑦 ⋯ 𝑦 ⋅ 𝑥)𝑛
= 𝑥 ⋅ (𝑦 𝑘−1 ⋅ 𝑥)𝑛
= (𝑥𝑦 𝑘−1 )𝑛 𝑥,
68
that is, 𝑥 and (𝑥𝑦 𝑘−1 )𝑛 commute, and thus (𝑥𝑦 𝑘−1 )𝑛 = (𝑦 𝑘−1 𝑥)𝑛 .
Pick up 𝑚 ∈ ℤ+ such that 𝑚𝑛 ≥ 𝑘 − 1. Now we claim the following identity holds
𝑥 𝑛 𝑦[(𝑥𝑦 𝑘−1 )𝑚𝑛 ]𝑛 = 𝑦𝑥 𝑛 [(𝑥𝑦 𝑘−1 )𝑚𝑛 ]𝑛 .
We will combine suitable 𝑥’s and 𝑦’s together and apply above commutative properties:
𝑥 𝑛 𝑦[(𝑥𝑦 𝑘−1 )𝑚𝑛 ]𝑛 = 𝑥 𝑛 𝑦[(𝑥𝑦 𝑘−1 )𝑚𝑛−1 (𝑥𝑦 𝑘−2 )𝑦]𝑛
= 𝑥 𝑛 [𝑦(𝑥𝑦 𝑘−1 )𝑚𝑛−1 (𝑥𝑦 𝑘−2 )]𝑛 𝑦
= 𝑥 𝑛 [𝑦(𝑥𝑦 𝑘−1 )𝑚𝑛−1 𝑥 𝑦⏟
⋯ 𝑦]𝑛 𝑦
𝑘−2
= 𝑥 [𝑦 ⋯ 𝑦 ⋅𝑥 ⋅ 𝑦(𝑥𝑦 )𝑚𝑛−1 ]𝑛 𝑦
𝑛
⏟
𝑘−1
𝑘−2
= 𝑥 𝑛 (𝑦 𝑘−2 𝑥𝑦(𝑥𝑦 𝑘−1 )𝑚𝑛−1 )𝑛 𝑦
= 𝑥 𝑛 [𝑦 𝑘−2 𝑥𝑦 (𝑥𝑦 𝑘−1 ) ⋅ (𝑥𝑦 𝑘−1 ) ⋯ (𝑥𝑦 𝑘−1 )𝑚𝑛+2−𝑘 ]𝑛 𝑦
⏟⏟⏟⏟⏟⏟⏟⏟⏟⏟⏟⏟⏟⏟⏟⏟⏟⏟⏟⏟⏟⏟⏟⏟⏟⏟⏟⏟⏟⏟⏟⏟⏟⏟⏟⏟⏟⏟⏟⏟⏟
𝑘−2
( since 𝑚𝑛 ≥ 𝑘 − 1, 𝑚𝑛 + 2 − 𝑘 ≥ 1)
= 𝑥 𝑛 [(𝑥𝑦 𝑘−1 )𝑚𝑛+2−𝑘 (𝑥𝑦 𝑘−1 ) ⋯ (𝑥𝑦 𝑘−1 ) ⋅𝑥𝑦 ⋅ 𝑦 𝑘−2 ]𝑛 𝑦
⏟⏟⏟⏟⏟⏟⏟⏟⏟⏟⏟⏟⏟⏟⏟⏟⏟⏟⏟⏟⏟⏟⏟⏟⏟⏟⏟⏟⏟⏟⏟⏟⏟⏟⏟⏟⏟⏟⏟
𝑘−2
= 𝑥 𝑛 [(𝑥𝑦 𝑘−1 )𝑚𝑛 ]𝑛 𝑦
= [𝑥 ⋅ (𝑥𝑦 𝑘−1 )𝑚𝑛 ]𝑛 𝑦
(since 𝑥 commutes with (𝑥𝑦 𝑘−1 )𝑛 and (𝑥𝑦 𝑘−1 )𝑚𝑛 ).
On the other hand, we have
𝑦𝑥 𝑛 [(𝑥𝑦 𝑘−1 )𝑚𝑐 ]𝑛 = 𝑦[𝑥 ⋅ (𝑥𝑦 𝑘−1 )𝑚𝑛 ]𝑛 ( since 𝑥 and (𝑥𝑦 𝑘−1 )𝑚𝑛 commute)
= 𝑦 ⋅ [𝑥(𝑥𝑦 𝑘−1 )𝑚𝑛−1 ⋅ 𝑥𝑦 𝑘−2 ⋅ 𝑦]𝑛
= [𝑦 ⋅ 𝑥(𝑥𝑦 𝑘−1 )𝑚𝑛−1 ⋅ 𝑥𝑦 𝑘−2 ]𝑛 𝑦
= [𝑦𝑥(𝑥𝑦 𝑘−1 )𝑚𝑛−1 ⋅ 𝑥 𝑦⏟
⋯ 𝑦 ]𝑛 𝑦
𝑘−2
⋯ 𝑦 ⋅𝑥 ⋅ 𝑦𝑥(𝑥𝑦 𝑘−1 )𝑚𝑛−1 ]𝑛 𝑦
= 𝑦⏟
𝑘−2
⋯ 𝑦 ⋅(𝑥𝑦) ⋅ 𝑥(𝑥𝑦 𝑘−1 )𝑚𝑛−1 ]𝑛 𝑦
= 𝑦⏟
𝑘−2
= [𝑥(𝑥𝑦 𝑘−1 )𝑚𝑛−1 ⋅ (𝑥𝑦) ⋅ 𝑦⏟
⋯ 𝑦]𝑛 𝑦
𝑘−2
= [𝑥(𝑥𝑦 𝑘−1 )𝑚𝑛 ]𝑛 𝑦
Therefore, cancelling [(𝑥𝑦 𝑘−1 )𝑚𝑐 ]𝑛 from the right sides of 𝑥 𝑛 𝑦[(𝑥𝑦 𝑘−1 )𝑚𝑛 ]𝑛 = 𝑦𝑥 𝑛 [(𝑥𝑦 𝑘−1 )𝑚𝑐 ]𝑛 , we have
𝑥 𝑛 𝑦 = 𝑦𝑥 𝑛 .
69
3. Transferability of (𝑥𝑦)𝑛 = (𝑦𝑥)𝑛
Let (𝑆, ⋅) be a cancellation semigroup satisfying the law (𝑥𝑦)𝑛 = (𝑦𝑥)𝑛 . Then, by Corollary 2.3, we know
that all the powers of 𝑛 are central in 𝑆, i.e., 𝑆 satisfies the identity 𝑥 𝑛 ⋅ 𝑦 = 𝑦 ⋅ 𝑥 𝑛 . We now use the Ore
principle resulting from this identity to construct the actual group of quotients. Thus we will have
an explicit formula for the group multiplication. We show that this group multiplication satisfies the
semigroup law 𝑥 𝑛 ⋅ 𝑦 = 𝑦 ⋅ 𝑥 𝑛 . This will prove the transferability of 𝑥 𝑛 ⋅ 𝑦 = 𝑦 ⋅ 𝑥 𝑛 from 𝑆 to its Ore
group of right quotients 𝑆𝑆 −1 . Since (𝑥𝑦)𝑛 = (𝑦𝑥)𝑛 and 𝑥 𝑛 ⋅ 𝑦 = 𝑦 ⋅ 𝑥 𝑛 are equivalent in cancellation
semigroups, we get that the semigroup law (𝑥𝑦)𝑛 = (𝑦𝑥)𝑛 is also transferable.
Since the semigroup satisfies a non-trivial identity, it obviously satisfies the Ore left multiple principle
(the property Mv in Ore [14]), the group of right quotients 𝑆𝑆 −1 exists. What is not obvious is that the
group also satisfies the identity.
Theorem 3.1. The semigroup law (𝑥𝑦)𝑛 = (𝑦𝑥)𝑛 is transferable in a semigroup (𝑆, ⋅).
Proof. We first define the multiplication and the equality of quotients. Let 𝑎𝑏 and 𝑑𝑐 be two right quotients
in the group 𝑆𝑆 −1 . Thus the elements 𝑎, 𝑏, 𝑐, 𝑑 are in 𝑆. We follow the idea of Ore and define the product
and equality of two right quotients. Note that
𝑎 𝑐 𝑎𝑏 𝑛−1 𝑐𝑑 𝑛−1
⋅ = 𝑎𝑏 −1 𝑐𝑑 −1 = 𝑎𝑏 𝑛−1−𝑛 𝑐𝑑 𝑛−1−𝑛 = 𝑎𝑏 𝑛−1 𝑐𝑑 𝑛−1 𝑏 −𝑛 𝑑 −𝑛 = .
𝑏 𝑑 𝑏𝑛𝑑 𝑛
Thus we can define the product
𝑎 𝑐 𝑎𝑏 𝑛−1 𝑐𝑑 𝑛−1
⋅ = .
𝑏 𝑑 𝑏𝑛𝑑 𝑛
Also, here
𝑎
𝑏
∼ 𝑑𝑐 if and only if 𝑎𝑏 𝑛−1 𝑑 = 𝑏 𝑛 𝑐.
𝑎 𝑎 −1 𝑏𝑛
Hence, the identity is 𝑎0 and the inverse ( 𝑏 ) = 𝑎𝑏𝑛−1 .
0
Next we define the embedding map as following: for any 𝑎 ∈ 𝑆,
𝑎𝑎
𝜙 ∶ 𝑆 → 𝑆𝑆 −1 , 𝜙(𝑎) = 𝑎 0 . for some 𝑎0 ∈ 𝑆.
0
For any 𝑎, 𝑏 ∈ 𝑆, we have
𝑎𝑏𝑎0 𝑎𝑏𝑎0𝑛 𝑏0𝑛 𝑎𝑎0 𝑏𝑏0
𝜙(𝑎𝑏) = = 𝑛 𝑛 = = 𝜙(𝑎)𝜙(𝑏).
𝑎0 𝑎0 𝑏0 𝑎0 𝑏0
Hence 𝜙 is an isomorphism.
Now we prove that 𝑎𝑏 = 𝜙(𝑎)𝜙(𝑏)−1 for any 𝑎, 𝑏 ∈ 𝑆.
𝑎𝑎0 𝑏𝑏0 −1 𝑎𝑎0 𝑏0𝑛 𝑎𝑎0𝑛 𝑏0𝑛 (𝑏𝑏0𝑛 )𝑛−1
𝜙(𝑎)𝜙(𝑏)−1 = ( ) = = .
𝑎0 𝑏0 𝑎0 𝑏𝑏0𝑛 𝑎0𝑛 (𝑏𝑏0𝑛 )𝑛
Thus
𝑎 𝑎𝑎0𝑛 𝑏0𝑛 (𝑏𝑏0𝑛 )𝑛−1
𝑏
= 𝑎0𝑛 (𝑏𝑏0𝑛 )𝑛
⟺ 𝑎𝑎0𝑛 𝑏0𝑛 (𝑏𝑏0𝑛 )𝑛−1 𝑏 𝑛 = 𝑎𝑏 𝑛−1 𝑎0𝑛 (𝑏𝑏0𝑛 )𝑛
⟺ 𝑎𝑎0𝑛 𝑏0𝑛 (𝑏𝑏0𝑛 )𝑛−1 𝑏 𝑛 = 𝑎𝑎0𝑛 𝑏 𝑛−1 (𝑏𝑏0𝑛 )(𝑏𝑏0𝑛 )𝑛−1
⟺ 𝑎𝑎0𝑛 𝑏0𝑛 𝑏 𝑛 (𝑏𝑏0𝑛 )𝑛−1 = 𝑎𝑎0𝑛 𝑏0𝑛 𝑏 𝑛 (𝑏𝑏0𝑛 )𝑛−1 ( since 𝑎0𝑛 , 𝑏 𝑛 , 𝑏0𝑛 are central).
70
Hence 𝑎𝑏 = 𝜙(𝑎)𝜙(𝑏)−1 . Therefore, we have the following two formats for the group of quotients:
𝑎
𝑆𝑆 −1 = { | 𝑎, 𝑏 ∈ 𝑆} = {𝜙(𝑎)𝜙(𝑏)−1 | 𝑎, 𝑏 ∈ 𝑆}.
𝑏
For any 𝑎, 𝑏 ∈ 𝑆, we can verify the following four identities:
𝜙(𝑎)𝑛 𝜙(𝑏) = 𝜙(𝑎𝑛 𝑏) = 𝜙(𝑏𝑎𝑛 ) = 𝜙(𝑏)𝜙(𝑎)𝑛 .
𝜙(𝑎)𝑛 𝜙(𝑏)−1 = 𝜙(𝑏)−1 𝜙(𝑏)𝜙(𝑎)𝑛 𝜙(𝑏)−1 = 𝜙(𝑏)−1 𝜙(𝑎)𝑛 𝜙(𝑏)𝜙(𝑏)−1 = 𝜙(𝑏)−1 𝜙(𝑎)𝑛 .
(𝜙(𝑎)−1 )𝑛 𝜙(𝑏) = (𝜙(𝑎)−1 )𝑛 𝜙(𝑏)𝜙(𝑎)𝑛 (𝜙(𝑎)−1 )𝑛
= (𝜙(𝑎)−1 )𝑛 𝜙(𝑎)𝑛 𝜙(𝑏)(𝜙(𝑎)−1 )𝑛
= 𝜙(𝑏)(𝜙(𝑎)−1 )𝑛 .
(𝜙(𝑎)−1 )𝑛 𝜙(𝑏)−1 = 𝜙(𝑏)−1 𝜙(𝑏)(𝜙(𝑎)−1 )𝑛 𝜙(𝑏)−1
= 𝜙(𝑏)−1 (𝜙(𝑎)−1 )𝑛 𝜙(𝑏)𝜙(𝑏)−1
= 𝜙(𝑏)−1 (𝜙(𝑎)−1 )𝑛 .
Since every element in 𝑆𝑆 −1 has the form 𝜙(𝑎)𝜙(𝑏)−1 , we can conclude that both 𝜙(𝑎)𝑛 and (𝜙(𝑎)−1 )𝑛
are central in 𝑆𝑆 −1 for all 𝑎 ∈ 𝑆.
𝑛
Next, we prove that for any 𝑎, 𝑏 ∈ 𝑆, ( 𝑎𝑏 ) = [𝜙(𝑎)𝜙(𝑏)−1 ]𝑛 is central in 𝑆𝑆 −1 . For any 𝑔 ∈ 𝑆𝑆 −1 , we
have
[𝜙(𝑎)𝜙(𝑏)−1 ]𝑛 𝑔 = [𝜙(𝑎)𝜙(𝑏)−1 ][𝜙(𝑎)𝜙(𝑏)−1 ]𝑛−1 𝑔
= 𝜙(𝑎)𝑛 [𝜙(𝑎)−1 ]𝑛−1 𝜙(𝑏)−1 [𝜙(𝑎)𝜙(𝑏)−1 ]𝑛−1 𝑔
= 𝜙(𝑏𝑎𝑛−1 )−1 [𝜙(𝑎)𝜙(𝑏)−1 ]𝑛−1 𝑔 ⋅ 𝜙(𝑎)𝑛
= [𝜙(𝑏𝑎𝑛−1 )−1 ]𝑛 𝜙(𝑏𝑎𝑛−1 )𝑛−1 ⋅ [𝜙(𝑎)𝜙(𝑏)−1 ]𝑛−1 𝑔 ⋅ 𝜙(𝑎)𝑛
= [𝜙(𝑏𝑎𝑛−1 )𝑛−1 ] ⋅ [𝜙(𝑎)𝜙(𝑏)−1 ]𝑛−1 𝑔 ⋅ 𝜙(𝑎)𝑛 [𝜙(𝑏𝑎𝑛−1 )−1 ]𝑛
= (𝜙[(𝑏𝑎𝑛−1 )𝑛−1 ⋅ 𝑎]𝜙(𝑏)−1 ) ⋅ [𝜙(𝑎)𝜙(𝑏)−1 ]𝑛−2 𝑔[𝜙(𝑎)𝜙(𝑏)−1 ]
⋅[𝜙(𝑏𝑎𝑛−1 )𝑛−1 ]−1
= (𝜙[(𝑏𝑎𝑛−1 )𝑛−1 𝑎]𝜙(𝑏)−1 ) ⋅ [𝜙(𝑎)𝜙(𝑏)−1 ]𝑛−2 𝑔[𝜙(𝑎)𝜙(𝑏)−1 ]
⋅[𝜙(𝑏𝑎𝑛−1 )𝑛−1 ]−1
(Let 𝑎′ = (𝑏𝑎𝑛−1 )𝑛−1 𝑎)
= [𝜙(𝑎′ )𝜙(𝑏)−1 ] ⋅ [𝜙(𝑎)𝜙(𝑏)−1 ]𝑛−2 𝑔[𝜙(𝑎)𝜙(𝑏)−1 ][𝜙(𝑎′ )𝜙(𝑎)−1 ]−1 .
Using the deduction above again, we have
(𝜙[(𝑏(𝑎′ )𝑛−1 )𝑛−1 𝑎]𝜙(𝑏)−1 ⋅ [𝜙(𝑎)𝜙(𝑏)−1 ]𝑛−3 𝑔[𝜙(𝑎)𝜙(𝑏)−1 ][𝜙(𝑎′ )𝜙(𝑎)−1 ]−1
⋅[𝜙(𝑎′ )𝜙(𝑏)−1 ] ⋅ [𝜙(𝑏(𝑎′ ))𝑛−1 )𝑛−1 ]−1
= (𝜙[(𝑏(𝑎′ )𝑛−1 )𝑛−1 𝑎]𝜙(𝑏)−1 ⋅ [𝜙(𝑎)𝜙(𝑏)−1 ]𝑛−3 𝑔[𝜙(𝑎)𝜙(𝑏)−1 ]2
⋅[𝜙(𝑏(𝑎′ ))𝑛−1 )𝑛−1 ]−1 .
Define
𝑎1 = 𝑎, 𝑎2 = 𝑎′ = (𝑏𝑎𝑛−1 )𝑛−1 𝑎, … , 𝑎𝑘+1 = (𝑏𝑎𝑘𝑛−1 )𝑛−1 𝑎.
71
Then
[𝜙(𝑎)𝜙(𝑏)−1 ]𝑛 𝑔
= [𝜙(𝑎1 )𝜙(𝑏)−1 ] ⋅ [𝜙(𝑎)𝜙(𝑏)−1 ]𝑛−1 𝑔
= [𝜙(𝑎2 )𝜙(𝑏)−1 ] ⋅ [𝜙(𝑎)𝜙(𝑏)−1 ]𝑛−2 𝑔[𝜙(𝑎)𝜙(𝑏)−1 ] ⋅ [𝜙(𝑎2 )𝜙(𝑎)−1 ]−1
=⋯
= [𝜙(𝑎𝑘 )𝜙(𝑏)−1 ] ⋅ [𝜙(𝑎)𝜙(𝑏)−1 ]𝑛−𝑘 𝑔[𝜙(𝑎)𝜙(𝑏)−1 ]𝑘−1 ⋅ [𝜙(𝑎2 )𝜙(𝑎)−1 ]−1
=⋯
= [𝜙(𝑎𝑛 )𝜙(𝑏)−1 ] ⋅ 𝑔[𝜙(𝑎)𝜙(𝑏)−1 ]𝑛−1 ⋅ [𝜙(𝑎𝑛 )𝜙(𝑎)−1 ]−1
If 𝜙(𝑎𝑛 )𝜙(𝑏)−1 is central, then we have
𝑔[𝜙(𝑎)𝜙(𝑏)−1 ]𝑛−1 ⋅ [𝜙(𝑎𝑛 )𝜙(𝑎)−1 ]−1 [𝜙(𝑎𝑛 )𝜙(𝑏)−1 ]
= 𝑔[𝜙(𝑎)𝜙(𝑏)−1 ]𝑛−1 ⋅ [𝜙(𝑎)𝜙(𝑏)−1 ]
= 𝑔[𝜙(𝑎)𝜙(𝑏)−1 ]𝑛 .
Hence, the proof is completed. Therefore, we will show that 𝜙(𝑎𝑛 )𝜙(𝑏)−1 is central as follows.
Let 𝑦𝑘 = 𝜙(𝑎𝑘 )𝜙(𝑏)−1 . Then
𝑦1 = 𝜙(𝑎)𝜙(𝑏)−1 , 𝑎𝑘+1 = (𝑏𝑎𝑘𝑛−1 )𝑛−1 𝑎,
𝜙(𝑎𝑘+1 ) = 𝜙[(𝑏𝑎𝑘𝑛−1 )𝑛−1 ] ⋅ 𝜙(𝑎) = [𝜙(𝑏)𝜙(𝑎𝑘 )𝑛−1 ]𝑛−1 ⋅ 𝜙(𝑎).
Thus
𝜙(𝑎𝑘+1 )𝜙(𝑏)−1 = [𝜙(𝑏)𝜙(𝑎𝑘 )𝑛−1 ]𝑛−1 ⋅ 𝜙(𝑎)𝜙(𝑏)−1 .
That is,
𝑦𝑘+1 = [𝜙(𝑏)[𝑦𝑘 𝜙(𝑏)]𝑛−1 ]𝑛−1 ⋅ 𝜙(𝑎)𝜙(𝑏)−1
= [[𝑦𝑘 𝜙(𝑏)]𝑛 ⋅ 𝑦𝑘−1 ]𝑛−1 𝜙(𝑎)𝜙(𝑏)−1
= [𝑦𝑘 𝜙(𝑏)]𝑛(𝑛−1) (𝑦𝑘−1 )𝑛 𝑦𝑘 𝜙(𝑎)𝜙(𝑏)−1 .
Continue the same deduction, and use 𝑦𝑘−1 to represent 𝑦𝑘 , we have
𝑦𝑘+1 = [𝑦𝑘 𝜙(𝑏)]𝑛(𝑛−1) (𝑦𝑘−1 )𝑛 [𝑦𝑘−1 𝜙(𝑏)]𝑛(𝑛−1) (𝑦𝑘−1
−1 )𝑛 𝑦 −1 2
𝑘−1 [𝜙(𝑎)𝜙(𝑏) ] .
Thus
−1 )𝑛 𝑦
𝑦𝑛 = [𝑦𝑛−1 𝜙(𝑏)]𝑛(𝑛−1) (𝑦𝑛−1 −1
𝑛−1 𝜙(𝑎)𝜙(𝑏)
= 𝑥1𝑛 𝑥2𝑛 𝑥3𝑛 𝑥4𝑛 𝑦𝑛−2 [𝜙(𝑎)𝜙(𝑏)−1 ]2
=⋯
= 𝑥1𝑛 𝑥2𝑛 ⋯ 𝑥2𝑛−2
𝑛 𝑦1 [𝜙(𝑎)𝜙(𝑏)−1 ]𝑛−1
= 𝑥1𝑛 𝑥2𝑛 ⋯ 𝑥2𝑛−2
𝑛 𝑦1 [𝜙(𝑎)𝜙(𝑏)−1 ]𝑛 ,
𝑛
where 𝑥𝑖 ∈ 𝑆, 𝑖 = 1, … , 2𝑛 − 2. Since all 𝑥 𝑛 , 𝑥 ∈ 𝑆 are central, 𝑦𝑛 is central as desired. Therefore, ( 𝑎𝑏 ) is
central, and thus the emdedding 𝜙 is perfect embedding.
Acknowledgments
This project is partially supported by Mitacs Globalink Research Internship Canada NSERC.
72
References
[1] G. Bergman, Hyperidentities of groups and semigroups. Aequat. Math. 23 (1981), 55–65.
[2] G. Bergman, Questions in Algebra. Preprint, Berkeley, U.D. 1986.
[3] B. M. Green and J. R. Isbell, Problems and Solutions: Solutions of Elementary Problems: E2259.
Commuting powers in a group. The American Mathematical Monthly, 78(8)(1971): 909–910.
[4] S. V. Ivanov, A. M. Storozhev, On identities in groups of fractions of cancellative semigroups, Proc.
Amer. Math. Soc. 133 (2005), 1873–1879.
[5] J. Krempa and O. Macedonska, On identities of cancellation semigroups, Contemporary Mathematics,
Vol 131, 1992
[6] F. W. Levi, Notes on group theory. I, II, J. Indian Math. Soc. 8 (1944), 1–9.
[7] O. Macedonska and P. Slanina. On identities satisfied by cancellative semigroups and their groups of
fractions, (Preprint).
[8] A.I. Mal’cev, Nilpotent Groups, Ivanov Gos.Ped.Ins.Uc.zap (1953).
[9] W. McCune, Prover9, https://www.cs.unm.edu/~mccune/mace4/.
[10] G. I. Moghaddam and R. Padmanabhan, Commutativity theorems for cancellative semigroups,
Semigroup Forum 95 (2017), no. 3, 448–454.
[11] G. I. Moghaddam, R. Padmanabhan, and Yang Zhang, Automated reasoning with power maps.
Journal of Automated Reasoning, 64(4)(2020), 689–697.
[12] B.H. Neumann and T. Taylor, Subsemigroups of Nilpotent Groups, Proc. Roy. Soc. Ser. A274(1963),
pp 1-4.
[13] T. Nordahi, Semigroups satisfying (𝑥𝑦)𝑚 = 𝑥 𝑚 𝑦 𝑚 , Semigroup Forum 8(4) (1974), 332–346.
[14] O. Ore, Linear Equations in Non-Commutative Fields Annals of Mathematics, Jul., 1931, Second
Series, Vol. 32, pp.463-477.
[15] R. Padmanabhan, and Yang Zhang, Commutativity theorems in groups with power-like maps, J.
Formaliz. Reason. 12(1) (2019), 1–10.
[16] Chen-Te Yen, Note on the commutativity of cancellative semigroups. Bulletin of the Institute of
Mathematics Academia Sinica, 10(2)(1982), 149-153.
[17] Chen-Te Yen, On the commutativity of rings and cancellative semigroups. Chinese Journal of
Mathematics, 11(2)(1983), 99–113.
73