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.
1. Introduction
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 [
CEUR Workshop
ceur-ws.org
ISSN1613-0073
known example of a transferable law is, of course, the commutative law. A. I. Malcev, B. H. Neumann
and others ([
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 properties, i.e., for all , , ∈ , the following are true: (i) ⋅ = ⋅ (ii) ⋅ = ⋅ implies = , implies = .
Some properties of cancellation semigroup can be found in, for example, [
.
Next we present the proof by using Prover9 [
[
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 [
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.
commute. In particular, the two terms ⋅ and ( ( ⋅ ) ⋅ )
Following the terminology of [
Theorem 2.2. Let be a cancellation semigroup and let ∶ → that ( ⋅ ) = ( ⋅ ) . Then () is a central element in . be a power-like function and assume
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]. 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 ( ⋅ ) since ( ⋅ ) = ( ⋅ )
commute since ⋅ and ( ( ⋅ ) ⋅ )
commute. since ( ⋅ ) = ( ⋅ ) since and ( ⋅ ) since and () commute
commute () ⋅ ⋅ ⋅ ( ( ⋅ )) = ⋅ () ⋅ ⋅ ( ( ⋅ )).
⋅ = ⋅ .
from the right sides, we get () ⋅ = ⋅ ()
( ⋯ 2 1) for any ∈ holds, then is central in for any ∈ .
Theorem 2.4. In a cancellation semigroup , if there exist ≥ 2, ∈ ℤ + such that ( 1 2 ⋯ ) = 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 = and thus =
. Hence is commutative.
Next, we consider ≥ 2 . Note that
= = . ⋅ ( −1 ) . By the condition, = . Then = = ⋅ ( ⋅ ⋯ ) = ⋅ ( ⋯ ⋅ ) = ⋅ ( −1 ⋅ ) = ( −1 ) , 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 ⋅ = ⋅ semigroups, we get that the semigroup law ( ) = ( ) is also transferable. are equivalent in cancellation
Since the semigroup satisfies a non-trivial identity, it obviously satisfies the Ore left multiple principle
(the property Mv in Ore [
Theorem 3.1. The semigroup law ( ) = ( ) is transferable in a semigroup (, ⋅) . Proof. We first define the multiplication and the equality of quotients. Let in the group
−1. Thus the elements , , , and equality of two right quotients. Note that are in . We follow the idea of Ore and define the product
and be two right quotients
Hence, the identity is 0 and the inverse ( )−1
Next we define the embedding map as following: for any ∈ ,
= ⟺ ⟺ ⟺ For any , ∈ , we have
Now we prove that = ()()
−1 for any , ∈ . ∶ → −1, () = 0 0 .
for some 0 ∈ . () = 0 00 00 = 0 0( 0)−1 0( 0) . Hence = ()() . Therefore, we have the following two formats for the group of quotients: , we can verify the following four identities: () −1 () = ( ) = ( ) = ()() Next, we prove that for any , ∈ , = [()() −1 ] is central in −1 . For any ∈ −1 , we [()() −1 ] = [()() ][()() ] , we can conclude that both () ] ⋅ () [( −1 ) −1 ] Since every element in are central in −1
for all ∈ . have (() −1 ) () −1
( ) −1 = () = ( = [( = [( = ([(
⋅[( = ([(
⋅[( = ( −1 1 = , 2 = ′ −1 −1 )
) −1 ) ⋅ [()() ] [()() −1
] −1 ) ⋅ [()() ] −1 ] ] −1 ][( ′
= ([(( ⋅[( ′ ′ −1 −1 −1 ] ⋅ [((
]() ([(( ⋅[(( ) )) ′ −1 −1 ′ −1 −1 ) ) ]() −1 ] ] ]
is central, then we have Hence, the proof is completed. Therefore, we will show that ( )() −1 is central as follows.
Let = ( )() −1
. Then
[()() = [()() = [()() −1 −1
] −1 Continue the same deduction, and use −1
to represent , we have +1 = [ ()] (−1) ( −1 ) [ −1 ()] (−1) ( −1 −1 ) −1 [()() ] . = [ −1 ()] (−1) ( −1 −1 ) −1 ()()
−1 = = ⋯ = = 1 1 1 2 2 2 3 4 −2 [()() −1 −1
] −1 central, and thus the emdedding is perfect embedding. , ∈ are central, is central as desired. Therefore, ( ) is Acknowledgments This project is partially supported by Mitacs Globalink Research Internship Canada NSERC.