Commutativity Theorems in Groups with Power-like Maps


  • Ranganathan Padmanabhan Department of Mathematics University of Manitoba
  • Yang Zhang Department of Mathematics University of Manitoba



Prover9, Power-like maps, Groups


There are several commutativity theorems in groups and rings which involve power maps f(x) = xn. The most famous example  of this kind is Jacobson's theorem which asserts that any ring satisfying the identity xn = x is commutative.  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 n 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 maps f(x) = xn and show how one can avoid having to reason explicitly with integer exponents. Implementing these new equational properties of power maps, we show how a theorem-prover can be a handy tool for quickly proving or confirming the truth of such theorems.


bibitem{[1]} F. Araujo and M. Kinyon, emph{Commutativity theorems for groups and semigroups.} Port. Math. 74 (2017), no. 3, 243 - 255.

bibitem{BM} M. Beeson, Mathematical induction in Otter-lambda. J. Automat. Reason. 36 (2006), no. 4, 311 - 344.

bibitem{[2]} J. R. Isbell, emph{Commuting Powers in a Group.} Amer. Math. Monthly, 77 (1970), 909.

bibitem{[3]} J. R. Isbell and B. M. Green, emph{E2259.} American Math Monthly, Vol 78 (1971), 909-910. (DOI: 10.2307/2316502)

bibitem{[KM]} J. Krempa and O. Macedonska, emph{On identities of cancellative semigroups.} Contemp. Math., 131, Part 3, Amer. Math. Soc., Providence, R.I. 1992.

bibitem{[4]} W. McCune, emph{Prover9, version 2009-02A.}

bibitem{[5]} W. McCune and R. Padmanabhan, emph{Automated deduction in equational logic and cubic curves.} Lecture Notes in Artificial Intelligence 1095. Springer-Verlag, Berlin, 1996.

bibitem{[6]} G. I. Moghaddam and R. Padmanabhan, emph{Commutativity theorems for cancellative semigroups. }Semigroup Forum 95(2017), no. 3, 448-454.

bibitem{[10]} G. I. Moghaddam, R. Padmanabhan and Yang Zhang, emph{Automated reasoning with power-maps.} submitted.

bibitem{[7]} B. H. Neumann, emph{Some semigroup laws in groups.} Canad. Math. Bull. 44 (2001), no. 1, 93-96.

bibitem{[8]} W. K. Nicholson and Yaqub Adil, emph{A commutativity theorem for rings and groups.}

Canad. Math. Bull. 22 (1979), no. 4, 419-423.

bibitem{[9]} G. Venkataraman, emph{Groups in which squares and cubes commute. }

arXiv: 1605.05463v1.

bibitem{Yen} Chen-Te Yen, emph{On the Commutativity of Rings and Cancellative Semigroups.} Chinese J. of Math, Vol 11 (1983), 99-113.




How to Cite

Padmanabhan, R., & Zhang, Y. (2019). Commutativity Theorems in Groups with Power-like Maps. Journal of Formalized Reasoning, 12(1), 1–10.