Commutativity Theorems in Groups with Power-like Maps
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...
| Main Authors: | , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
University of Bologna
2019-02-01
|
| Series: | Journal of Formalized Reasoning |
| Subjects: | |
| Online Access: | https://jfr.unibo.it/article/view/8751 |
| _version_ | 1818334431155322880 |
|---|---|
| author | Ranganathan Padmanabhan Yang Zhang |
| author_facet | Ranganathan Padmanabhan Yang Zhang |
| author_sort | Ranganathan Padmanabhan |
| collection | DOAJ |
| description | 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. |
| first_indexed | 2024-12-13T14:07:25Z |
| format | Article |
| id | doaj.art-bbeef9bafdfa4a7c9be4c67170a4b612 |
| institution | Directory Open Access Journal |
| issn | 1972-5787 |
| language | English |
| last_indexed | 2024-12-13T14:07:25Z |
| publishDate | 2019-02-01 |
| publisher | University of Bologna |
| record_format | Article |
| series | Journal of Formalized Reasoning |
| spelling | doaj.art-bbeef9bafdfa4a7c9be4c67170a4b6122022-12-21T23:42:35ZengUniversity of BolognaJournal of Formalized Reasoning1972-57872019-02-0112111010.6092/issn.1972-5787/87517885Commutativity Theorems in Groups with Power-like MapsRanganathan Padmanabhan0Yang Zhang1Department of Mathematics, University of ManitobaDepartment of Mathematics, University of ManitobaThere 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.https://jfr.unibo.it/article/view/8751prover9power-like mapsgroups |
| spellingShingle | Ranganathan Padmanabhan Yang Zhang Commutativity Theorems in Groups with Power-like Maps Journal of Formalized Reasoning prover9 power-like maps groups |
| title | Commutativity Theorems in Groups with Power-like Maps |
| title_full | Commutativity Theorems in Groups with Power-like Maps |
| title_fullStr | Commutativity Theorems in Groups with Power-like Maps |
| title_full_unstemmed | Commutativity Theorems in Groups with Power-like Maps |
| title_short | Commutativity Theorems in Groups with Power-like Maps |
| title_sort | commutativity theorems in groups with power like maps |
| topic | prover9 power-like maps groups |
| url | https://jfr.unibo.it/article/view/8751 |
| work_keys_str_mv | AT ranganathanpadmanabhan commutativitytheoremsingroupswithpowerlikemaps AT yangzhang commutativitytheoremsingroupswithpowerlikemaps |