AIM Project

May 2024

Main Conjecture: Let Q be an AIM loop with nucleus N(Q) and center Z(Q). Then Q/N(Q) is an abelian group, and Q/Z(Q) is a group.

In our representation (described below), it suffices to prove 7 goals. That is,

Weak Conjecture: A high-level mathematical argument that uses some of the results presented on this page shows that AIM loops are nilpotent of class 3. This is significant because previously it was not known whether the nilpotency class of AIM loops is even bounded.

Most recent posted results:

(2023-oct-26) middle Bol => a squared 1 and 3
(2023-oct-27) mbol + aa1 squared => aa1, which completes the proof that mbol + aa1 squared => all 7 goals of the main conjecture. (Case 17)
(2023-oct-31) middle Bol + Commutativity => nilpotency class 3
(2023-nov-12) middle Bol + imord2 R => aa1, which completes the proof that mbol + imord2 R => all 7 goals of the main conjecture. (Case 18)
(2023-nov-19) aK1 + a(a(x,y,z),z,w) = 1 => nilpotency class 3. *** cleaning up for posting ***

Here is the original proof.
(2023-dec-07) 12 middle Bol lemmas
(2023-dec-11) middle Bol => nilpotency class 3
(2024-may-16) Commutativity => L3 reciprocal

Some associated pages:

The results presented here rely on the following clause representation of AIM,

formulas(assumptions).

   % loop axioms
   1 * x = x.
   x * 1 = x.
   x \ (x * y) = y.
   x * (x \ y) = y.
   (x * y) / y = x.
   (x / y) * y = x.

   % associator (right associated * a = left associated)
   (x * (y * z)) \ ((x * y) * z) = a(x,y,z) # label("associator").

   % commutator ( (x * y) * K(y,x) = y * x )
   (x * y) \ (y * x) = K(y,x) # label("commutator").

   % inner mappings
   (y * x) \ (y * (x * u)) = L(u,x,y).
   ((u * x) * y) / (x * y) = R(u,x,y).
   x \ (u * x) = T(u,x).

   % abelian inner mapping group
   T(T(u,x),y) = T(T(u,y),x).
   T(L(u,x,y),z) = L(T(u,z),x,y).
   T(R(u,x,y),z) = R(T(u,z),x,y).
   L(R(u,x,y),z,w) = R(L(u,z,w),x,y).
   L(L(u,x,y),z,w) = L(L(u,z,w),x,y).
   R(R(u,x,y),z,w) = R(R(u,z,w),x,y).

end_of_list.

and the following representation of the 7 goals.

formulas(goals).

   % aK (or "single-a") goals
   K(a(x,y,z),u) = 1     # label("Ka").
   a(K(x,y),z,u) = 1     # label("aK1").
   a(x,K(y,z),u) = 1     # label("aK2").
   a(x,y,K(z,u)) = 1     # label("aK3").

   % aa (or "double-a") goals
   a(a(x,y,z),u,w) = 1   # label("aa1").
   a(x,a(y,z,u),w) = 1   # label("aa2").
   a(x,y,a(z,u,w)) = 1   # label("aa3").

end_of_list.

Including lemmas such as the following as additional input assumptions can help with some searches.

formulas(assumptions).

   % cancellation laws (long form)

   x * y != u | x * z != u | y = z # label("*-Cancellation 1").
   y * x != u | z * x != u | y = z # label("*-Cancellation 2").

   x / y != u | x / z != u | y = z # label("/-Cancellation 1").
   y / x != u | z / x != u | y = z # label("/-Cancellation 2").

   x \ y != u | x \ z != u | y = z # label("\-Cancellation 1").
   y \ x != u | z \ x != u | y = z # label("\-Cancellation 2").

   T(x,y) != u | T(z,y) != u | x = z # label("T-Cancellation 1").
   L(z,x,y) != u | L(w,x,y) != u | z = w # label("L-Cancellation 1").
   R(z,x,y) != u | R(w,x,y) != u | z = w # label("R-Cancellation 1").

   % cancellation laws (short form)

   x * y != x * z | y = z # label("*-Cancellation 3").
   y * x != z * x | y = z # label("*-Cancellation 4").

   x / y != x / z | y = z # label("/-Cancellation 3").
   y / x != z / x | y = z # label("/-Cancellation 4").

   x \ y != x \ z | y = z # label("\-Cancellation 3").
   y \ x != z \ x | y = z # label("\-Cancellation 4").

   T(x,y) != T(z,y) | x = z # label("T-Cancellation 2").
   L(z,x,y) != L(w,x,y) | z = w # label("L-Cancellation 2").
   R(z,x,y) != R(w,x,y) | z = w # label("R-Cancellation 2").

   % compatibility

   a(x,y,z) != 1 | L(z,y,x) = z # label("Compat 1").
   L(x,y,z) != x | a(z,y,x) = 1 # label("Compat 2").
   T(x,y) != x | T(y,x) = y # label("Compat 3").
   T(x,y) != x | K(x,y) = 1 # label("Compat 4").
   K(x,y) != 1 | T(x,y) = x # label("Compat 5").

   % sometimes helpful for demodulation-free proofs

   x != y | x * z = y * z # label("Aux 1").
   x != y | z * x = z * y # label("Aux 2").
   x != y | x / z = y / z # label("Aux 3").
   x != y | z / x = z / y # label("Aux 4").
   x != y | x \ z = y \ z # label("Aux 5").
   x != y | z \ x = z \ y # label("Aux 6").

   x != y | y != z | x = z # label("Transitivity =").

end_of_list.

In addition to the results posted here, Michael Kinyon has a page, AIM Problem Again, for proofs in which all derived (non input) clauses are units. He also has a page on AIM-TT, a generalization of the AIM problem that is identical to AIM except that it omits the axiom

   T(T(u,x),y) = T(T(u,y),x).

Result 1: Equivalence of {Ka,aK1,aK2,aK3}

Ka => aK1 (in, out, pf, xml)
aK1 => aK2 (in, out, pf, xml)
aK2 => aK3 (in, out, pf, xml)
aK3 => Ka (in, out, pf, xml)

Result 2: Equivalence of {aa1,aa2,aa3}

aa1 => aa2 (in, out, pf, xml)
aa2 => aa3 (in, out, pf, xml)
aa3 => aa1 (in, out, pf, xml)

Result 3: More results relating {Ka,aK1,aK2,aK3}

This section includes examples of aK (single-a) goals that are equal to permutations of their arguments in other aK goals.

   a(K(x,y),z,u) = a(x,z,K(u,y)) # label("aK1_eq_aK3 (1342)").

   K(a(x,y,z),u) = a(x,y,K(z,u)) # label("Ka_eq_aK3 (1234)").

   K(a(x,y,z),u) = K(x,a(u,y,z)) # label("Ka1_eq_Ka2 (1423)").

   a(x,K(y,z),u) = a(x,y,K(u,z)) # label("aK2_eq_aK3 (1243)").

Several special cases of aK2_eq_aK3 are posted in the Miscellaneous Results section below.

Here is a summary of results relating the 4 single-a goals.

Result 4: Some properties of a and K

   K(x,y) * a(u,v,w) = a(u,v,w) * K(x,y) # label("aKcom").

   K(K(x,y),z) = K(x,K(y,z))         # label("Kassoc").
   K(x,K(y,z)) = K(y,K(x,z))         # label("KKcom_a").
   K(x,K(y,z)) = K(x,K(z,y))         # label("KKcom_b").
   K(x,y) * K(z,u) = K(z,u) * K(x,y) # label("KKcom_c").
   K(x,y) * K(y,x) = 1               # label("KxyKyx").
   K(K(x,y),K(z,u)) = 1              # label("KofKK").
   K(x,y) = (x * y) / (y * x)        # label("K-dual").

   K(x,y) = x \ T(x,y)               # label("K_eq_T_a").
   K(x,y) = y / T(y,x)               # label("K_eq_T_b").
   K(T(x,y),T(z,y)) = K(x,z)         # label("K_eq_T_c").

   K(x,K(y,z * z)) = 1               # label("Ksqmap").

Result 5: Some properties of T, L and R

   T(x / (x / y),z) = x / (x / T(y,z))     # label("T property").
   L(x / (x / y),z,u) = x / (x / L(y,z,u)) # label("L property").
   R(x / (x / y),z,u) = x / (x / R(y,z,u)) # label("R property").

   K(x \ 1,x) = K(T(x,y) \ 1,T(x,y))       # label("KinvT").
   K(x \ 1,x) = K(L(x,y,z) \ 1,L(x,y,z))   # label("KinvL").
   K(x \ 1,x) = K(R(x,y,z) \ 1,R(x,y,z))   # label("KinvR").

   K(x,R(y,z,u)) = K(x,L(y,z,u))           # label("KRKL").
   T(x,R(y,z,u)) = T(x,L(y,z,u))           # label("TRTL").
   R(K(x,y),z,u) = L(K(x,y),z,u)           # label("RKLK 1").
   R(x,K(y,z),u) = L(x,K(y,z),u)           # label("RKLK 2").
   R(x,y,K(z,u)) = L(x,y,K(z,u))           # label("RKLK 3").
   L(K(x,y),z,u) = K(x,L(y,z,u))           # label("LKKL").

Result 6: Instances of {Ka,aK1,aK2,aK3}

%  a(K(w,x),y,z) = 1  *** original goal ***
   a(K(w,w),y,z) = 1 # label("aK1{x1/x2}").
   a(K(w,x),w,z) = 1 # label("aK1{x1/x3}").
   a(K(w,x),y,w) = 1 # label("aK1{x1/x4}").
   a(K(w,x),x,z) = 1 # label("aK1{x2/x3}").
   a(K(w,x),y,x) = 1 # label("aK1{x2/x4}").
   a(K(w,x),y,y) = 1 # label("aK1{x3/x4}").

%  a(w,K(x,y),z) = 1  *** original goal ***
   a(w,K(w,y),z) = 1 # label("aK2{x1/x2}").
   a(w,K(x,w),z) = 1 # label("aK2{x1/x3}").
   a(w,K(x,y),w) = 1 # label("aK2{x1/x4}").
   a(w,K(x,x),z) = 1 # label("aK2{x2/x3}").
   a(w,K(x,y),x) = 1 # label("aK2{x2/x4}").
   a(w,K(x,y),y) = 1 # label("aK2{x3/x4}").

%  a(w,x,K(y,z)) = 1  *** original goal ***
   a(w,w,K(y,z)) = 1 # label("aK3{x1/x2}").
   a(w,x,K(w,z)) = 1 # label("aK3{x1/x3}").
   a(w,x,K(y,w)) = 1 # label("aK3{x1/x4}").
   a(w,x,K(x,z)) = 1 # label("aK3{x2/x3}").
   a(w,x,K(y,x)) = 1 # label("aK3{x2/x4}").
   a(w,x,K(y,y)) = 1 # label("aK3{x3/x4}").

%  K(a(w,x,y),z) = 1  *** original goal ***
   K(a(w,w,y),z) = 1 # label("Ka{x1/x2}").
   K(a(w,x,w),z) = 1 # label("Ka{x1/x3}").
   K(a(w,x,y),w) = 1 # label("Ka{x1/x4}").
   K(a(w,x,x),z) = 1 # label("Ka{x2/x3}").
   K(a(w,x,y),x) = 1 # label("Ka{x2/x4}").
   K(a(w,x,y),y) = 1 # label("Ka{x3/x4}").

These are the 24 proper instances of {Ka,aK1,aK2,aK3} formed by renaming a single variable.

Result 7: Instances of {aa1,aa2,aa3}

   a(a(x,y,x),u,w) = 1 # label("aa1{x1/x3}").
   a(x,a(y,z,u),x) = 1 # label("aa2{x1/x5}").
   a(x,a(y,z,y),w) = 1 # label("aa2{x2/x4}").
   a(x,y,a(z,u,z)) = 1 # label("aa3{x3/x5}").

These are 4 of the 30 proper instances of {aa1,aa2,aa3} formed by renaming a single variable.

Result 8: Nilpotency class 3 properties

Michael Kinyon originally presented 32 properties sufficient to prove that AIM loops are nilpotent of class 3. Of these 32,

Nil3 Case 1

Proofs of the 8 of 32 having > 1 occurrence of K.

   K(x,K(y,K(z,u))) = 1    # label("nil3 1, KK-C").
   K(K(x,a(y,z,u)),w) = 1  # label("nil3 2, Ka-C").
   K(a(K(x,y),z,u),w) = 1  # label("nil3 3, aK1-C").
   K(a(x,K(y,z),u),w) = 1  # label("nil3 4, aK2-C").
   K(a(x,y,K(z,u)),w) = 1  # label("nil3 5, aK3-C").
   a(K(x,K(y,z)),u,w) = 1  # label("nil3 9, KK-Nl").
   a(x,K(y,K(z,u)),w) = 1  # label("nil3 10, KK-Nm").
   a(x,y,K(z,K(u,w))) = 1  # label("nil3 11, KK-Nr").

Nil3 Case 2

{7,15,18} => the remaining 12 of 15 having exactly 1 occurrence of K

Extra assumptions:

   K(a(x,a(y,z,u),w),v5) = 1 # label("nil3 7, aa2-C").
   a(a(K(x,y),z,u),w,v5) = 1 # label("nil3 15, aK1-Nl").
   a(x,a(K(y,z),u,w),v5) = 1 # label("nil3 18, aK1-Nm").

12 goals:

   K(a(a(x,y,z),u,w),v5) = 1   # label("nil3 6, aa1-C").
%  K(a(x,a(y,z,u),w),v5) = 1   # label("nil3 7, aa2-C").
   K(a(x,y,a(z,u,w)),v5) = 1   # label("nil3 8, aa3-C").
   a(K(x,a(y,z,u)),w,v5) = 1   # label("nil3 12, Ka-Nl").
   a(x,K(y,a(z,u,w)),v5) = 1   # label("nil3 13, Ka-Nm").
   a(x,y,K(z,a(u,w,v5))) = 1   # label("nil3 14, Ka-Nr").
%  a(a(K(x,y),z,u),w,v5) = 1   # label("nil3 15, aK1-Nl").
   a(a(x,K(y,z),u),w,v5) = 1   # label("nil3 16, aK2-Nl").
   a(a(x,y,K(z,u)),w,v5) = 1   # label("nil3 17, aK3-Nl").
%  a(x,a(K(y,z),u,w),v5) = 1   # label("nil3 18, aK1-Nm").
   a(x,a(y,K(z,u),w),v5) = 1   # label("nil3 19, aK2-Nm").
   a(x,a(y,z,K(u,w)),v5) = 1   # label("nil3 20, aK3-Nm").
   a(x,y,a(K(z,u),w,v5)) = 1   # label("nil3 21, aK1-Nr").
   a(x,y,a(z,K(u,w),v5)) = 1   # label("nil3 22, aK2-Nr").
   a(x,y,a(z,u,K(w,v5))) = 1   # label("nil3 23, aK3-Nr").

Nil3 Case 3

nil3 15 => nil3 7

Extra assumption:

   a(a(K(x,y),z,u),w,v5) = 1 # label("nil3 15, aK1-Nl").

Goal:

   K(a(x,a(y,z,u),w),v5) = 1 # label("nil3 7, aa2-C").

Nil3 Case 4

{15,18} => the remaining 13 of 15 having exactly 1 occurrence of K

Extra assumptions:

   a(a(K(x,y),z,u),w,v5) = 1 # label("nil3 15, aK1-Nl").
   a(x,a(K(y,z),u,w),v5) = 1 # label("nil3 18, aK1-Nm").

13 goals:

   K(a(a(x,y,z),u,w),v5) = 1   # label("nil3 6, aa1-C").
   K(a(x,a(y,z,u),w),v5) = 1   # label("nil3 7, aa2-C").
   K(a(x,y,a(z,u,w)),v5) = 1   # label("nil3 8, aa3-C").
   a(K(x,a(y,z,u)),w,v5) = 1   # label("nil3 12, Ka-Nl").
   a(x,K(y,a(z,u,w)),v5) = 1   # label("nil3 13, Ka-Nm").
   a(x,y,K(z,a(u,w,v5))) = 1   # label("nil3 14, Ka-Nr").
%  a(a(K(x,y),z,u),w,v5) = 1   # label("nil3 15, aK1-Nl").
   a(a(x,K(y,z),u),w,v5) = 1   # label("nil3 16, aK2-Nl").
   a(a(x,y,K(z,u)),w,v5) = 1   # label("nil3 17, aK3-Nl").
%  a(x,a(K(y,z),u,w),v5) = 1   # label("nil3 18, aK1-Nm").
   a(x,a(y,K(z,u),w),v5) = 1   # label("nil3 19, aK2-Nm").
   a(x,a(y,z,K(u,w)),v5) = 1   # label("nil3 20, aK3-Nm").
   a(x,y,a(K(z,u),w,v5)) = 1   # label("nil3 21, aK1-Nr").
   a(x,y,a(z,K(u,w),v5)) = 1   # label("nil3 22, aK2-Nr").
   a(x,y,a(z,u,K(w,v5))) = 1   # label("nil3 23, aK3-Nr").

Nil3 Case 5

nil3 15 => the remaining 14 of 15 having exactly 1 occurrence of K

Extra assumption:

   a(a(K(x,y),z,u),w,v5) = 1 # label("nil3 15, aK1-Nl").

14 goals:

   K(a(a(x,y,z),u,w),v5) = 1   # label("nil3 6, aa1-C").
   K(a(x,a(y,z,u),w),v5) = 1   # label("nil3 7, aa2-C").
   K(a(x,y,a(z,u,w)),v5) = 1   # label("nil3 8, aa3-C").
   a(K(x,a(y,z,u)),w,v5) = 1   # label("nil3 12, Ka-Nl").
   a(x,K(y,a(z,u,w)),v5) = 1   # label("nil3 13, Ka-Nm").
   a(x,y,K(z,a(u,w,v5))) = 1   # label("nil3 14, Ka-Nr").
%  a(a(K(x,y),z,u),w,v5) = 1   # label("nil3 15, aK1-Nl").
   a(a(x,K(y,z),u),w,v5) = 1   # label("nil3 16, aK2-Nl").
   a(a(x,y,K(z,u)),w,v5) = 1   # label("nil3 17, aK3-Nl").
   a(x,a(K(y,z),u,w),v5) = 1   # label("nil3 18, aK1-Nm").
   a(x,a(y,K(z,u),w),v5) = 1   # label("nil3 19, aK2-Nm").
   a(x,a(y,z,K(u,w)),v5) = 1   # label("nil3 20, aK3-Nm").
   a(x,y,a(K(z,u),w,v5)) = 1   # label("nil3 21, aK1-Nr").
   a(x,y,a(z,K(u,w),v5)) = 1   # label("nil3 22, aK2-Nr").
   a(x,y,a(z,u,K(w,v5))) = 1   # label("nil3 23, aK3-Nr").

Nil3 Case 6

nil3 23 => the remaining 14 of 15 having exactly 1 occurrence of K

Extra assumption:

   a(x,y,a(z,u,K(w,v5))) = 1   # label("nil3 23, aK3-Nr").

14 goals:

   K(a(a(x,y,z),u,w),v5) = 1   # label("nil3 6, aa1-C").
   K(a(x,a(y,z,u),w),v5) = 1   # label("nil3 7, aa2-C").
   K(a(x,y,a(z,u,w)),v5) = 1   # label("nil3 8, aa3-C").
   a(K(x,a(y,z,u)),w,v5) = 1   # label("nil3 12, Ka-Nl").
   a(x,K(y,a(z,u,w)),v5) = 1   # label("nil3 13, Ka-Nm").
   a(x,y,K(z,a(u,w,v5))) = 1   # label("nil3 14, Ka-Nr").
   a(a(K(x,y),z,u),w,v5) = 1   # label("nil3 15, aK1-Nl").
   a(a(x,K(y,z),u),w,v5) = 1   # label("nil3 16, aK2-Nl").
   a(a(x,y,K(z,u)),w,v5) = 1   # label("nil3 17, aK3-Nl").
   a(x,a(K(y,z),u,w),v5) = 1   # label("nil3 18, aK1-Nm").
   a(x,a(y,K(z,u),w),v5) = 1   # label("nil3 19, aK2-Nm").
   a(x,a(y,z,K(u,w)),v5) = 1   # label("nil3 20, aK3-Nm").
   a(x,y,a(K(z,u),w,v5)) = 1   # label("nil3 21, aK1-Nr").
   a(x,y,a(z,K(u,w),v5)) = 1   # label("nil3 22, aK2-Nr").
%  a(x,y,a(z,u,K(w,v5))) = 1   # label("nil3 23, aK3-Nr").

Nil3 Case 7

aK1 + nil3 24 => the remaining 8/32 nil3 clauses having 0 occurrences of K.

Extra assumptions:

   a(K(x,y),z,u) = 1 # label("aK1").
   a(a(a(x,y,z),u,w),v5,v6) = 1 # label("nil3 24, aa1-Nl").

Goals:

   a(a(x,a(y,z,u),w),v5,v6) = 1 # label("nil3 25, aa2-Nl").
   a(a(x,y,a(z,u,w)),v5,v6) = 1 # label("nil3 26, aa3-Nl").
   a(x,a(a(y,z,u),w,v5),v6) = 1 # label("nil3 27, aa1-Nm").
   a(x,a(y,a(z,u,w),v5),v6) = 1 # label("nil3 28, aa2-Nm").
   a(x,a(y,z,a(u,w,v5)),v6) = 1 # label("nil3 29, aa3-Nm").
   a(x,y,a(a(z,u,w),v5,v6)) = 1 # label("nil3 30, aa1-Nr").
   a(x,y,a(z,a(u,w,v5),v6)) = 1 # label("nil3 31, aa2-Nr").
   a(x,y,a(z,u,a(w,v5,v6))) = 1 # label("nil3 32, aa3-Nr").

The following version restricts paramodulation to unit parents.

Nil3 Case 8

K(x,y) = K(y,x) => nil3 23

Extra assumption:

   K(x,y) = K(y,x) # label("Kcom").

Goal:

   a(x,y,a(z,u,K(w,v5))) = 1   # label("nil3 23, aK3-Nr").

Nil3 Case 9

aK1_1324 => nil3 15

Extra assumption:

   a(K(x,y),z,u) = a(K(x,z),y,u) # label("aK1_1324").

Goal:

   a(a(K(x,y),z,u),w,v5) = 1 # label("nil3 15, aK1-Nl").

In addition to the results presented here, Michael Kinyon has a page on nil3.

Result 9: Nilpotency class 4 properties

Here are 128 nilpotency class 4 properties derived from the 32 original nil3 properties. Many of the 128 follow simply from known nil3 properties and dependencies among the nil3 properties. This section includes nil4 results that appear (for now) to be more significant.

Goal:

   K(a(x,a(y,K(z,u),w),v5),v6) = 1 # label("nil4 19K").

Result 10: Permutation properties of the primary goals

   a(x,K(y,z),u) = a(u,K(z,y),x) # label("aK2 (4321)").

   a(K(x,y),z,u) = a(K(y,u),z,x) # label("aK1 (2431)").
   a(K(x,y),z,u) = a(K(u,x),z,y) # label("aK1 (4132)").
   a(x,y,K(z,u)) = a(z,y,K(u,x)) # label("aK3 (3241)").
   a(x,y,K(z,u)) = a(u,y,K(x,z)) # label("aK3 (4213)").
   K(a(x,y,z),u) = K(a(z,y,u),x) # label("Ka (3241)").
   K(a(x,y,z),u) = K(a(u,y,x),z) # label("Ka (4213)").

The Conjecture

We prove the main conjecture for various special cases, that is, for AIM extended with extra assumptions.

Note that by Results 1 and 2 above, it suffices to show any one of {Ka,aK1,aK2,aK3} and any one of {aa1,aa2,aa3}.

Case 1: Moufang

   ((x * y) * x) * z = x * (y * (x * z)) # label("Moufang").

Proof of aK1: (in, out, pf, xml)

Proof of aa1: (in, out, pf, xml)

Case 2: LC

   (x * (x * y)) * z = x * (x * (y * z)) # label("LC").

Proof of aK1: (in, out, pf, xml)

Proof of aa1: (in, out, pf, xml)

Case 3: left Bol

   (x * (y * x)) * z = x * (y * (x * z)) # label("left Bol").

Proof of aK1: (in, out, pf, xml)

Proof of aa1: (in, out, pf, xml)

Case 4: RIF + LIP

   ((x * (y * z)) * x) * y = (x * y) * (z * (x * y)) # label("RIF").

   (1 / x) * (x * y) = y # label("LIP").

Proof of aK1: (in, out, pf, xml)

Proof of aa1: (in, out, pf, xml)

Case 5: L1-distributivity

   L(x1,y,z) * L(x2,y,z) = L(x1 * x2,y,z) # label("L1dist").

Proof of aK1: (in, out, pf, xml)

Proof of aa1: (in, out, pf, xml)

Case 6: R1-distributivity

   R(x1,y,z) * R(x2,y,z) = R(x1 * x2,y,z) # label("R1dist").

Proof of aK1: (in, out, pf, xml)

Proof of aa1: (in, out, pf, xml)

Case 7: generalized Moufang

   ((1 / x) \ y) * (z * x) = x * ((y * z) * x) # label("Osborn").
   x * ((y * x) \ 1) = y \ 1 # label("WIP").

Proof of aK1: (in, out, pf, xml)

Proof of aa1: (in, out, pf, xml)

Case 8: generalized Bol

   (x * (y * x)) * ((1 / x) * z) = x * (y * z) # label("gen left Bol").
   (x * (y \ 1)) * ((y * z) * y) = (x * z) * y # label("gen right Bol").

Proof of aK1: (in, out, pf, xml)

Proof of aa1: (in, out, pf, xml)

Case 9: LCC

   ((x * y) / x) * (x * z) = x * (y * z) # label(LCC).

This result was already known when we began the AIM project.

Proof of aK1: (in, out, pf, xml)

Proof of aa1: (in, out, pf, xml)

In addition to the 7 primary goals, this case also includes a proof of KK.

   K(K(x,y),z) = 1 # label("KK").

Proof of KK: (in, out, pf, xml)

Case 10: Nuclear Squares

   (x * x) * (y * z) = ((x * x) * y) * z # label("NucSq_l").
   (x * (y * y)) * z = x * ((y * y) * z) # label("NucSq_m").
   (x * y) * (z * z) = x * (y * (z * z)) # label("NucSq_r").

Proof of aK1: (in, out, pf, xml)

Proof of aa1: (in, out, pf, xml)

Some intermediate results:

NS + aK1 => aa1
(in, out, pf, xml)
NS + aK1 => nil3_24
(in, out, pf, xml)
NS + nil3 24 => aa1
(in, out, pf, xml)

Case 11: T1-distributivity

   T(x,y) * T(z,y) = T(x * z,y) # label("T1dist").

This case is in progress.

Proof of aK1: (in, out, pf, xml)

A proof of {aa1,aa2,aa3} remains open.

Case 12: middle Bol + KK => aK1

Extra assumptions:

   x * ((y * z) \ x) = (x / z) * (y \ x) # label("middle Bol").
   K(K(x,y),z) = 1                       # label("KK").

Proof of aK1: (in, out, pf, xml)

A proof of {aa1,aa2,aa3} remains open.

Case 13: middle Bol => aK1

Extra assumption:

   x * ((y * z) \ x) = (x / z) * (y \ x) # label("middle Bol").

Proof of aK1: (in, out, pf, xml)

A proof of {aa1,aa2,aa3} remains open.

Here is the original proof that middle Bol => aK3.

Here is a demodulation-free version of the original proof.

Here are several other consequences of middle Bol.

Case 14: {KK,Kcom} => aK1

Extra assumptions:

   K(K(x,y),z) = 1 # label("KK").
   K(x,y) = K(y,x) # label("Kcom").

Proof of aK1: (in, out, pf, xml)

A proof of {aa1,aa2,aa3} remains open.

Case 15: {Osborn,Kcom}

Extra assumptions:

   ((1 / x) \ y) * (z * x) = x * ((y * z) * x) # label("Osborn").
   K(x,y) = K(y,x) # label("Kcom").

Proof of aK1: (in, out, pf, xml)

The following proof of aa1 includes the proved lemma aK1 as an assumption.

Proof of aa1: (in, out, pf, xml)

Here is a proof without the lemmas.

Proof of aa1: (in, out, pf, xml)

Case 16: KK + aK1_1324

Extra assumptions:

   K(K(x,y),z) = 1 # label("KK").
   a(K(x,y),z,u) = a(K(x,z),y,u) # label("aK1_1324").

Proof of aK1: (in, out, pf, xml)

A proof of {aa1,aa2,aa3} remains open.

Case 17: middle Bol + aa1 squared

Extra assumptions:

   x * ((y * z) \ x) = (x / z) * (y \ x) # label("middle Bol").
   a(a(x,y,z),u,w) * a(a(x,y,z),u,w) = 1 # label("aa1 squared").

aK1 follows from middle Bol alone. See Case 13.

Proof of aa1: (in, out, pf, xml)

Case 18: middle Bol + imord2 R

Extra assumptions:

   x * ((y * z) \ x) = (x / z) * (y \ x) # label("middle Bol").
   R(R(x,y,z),y,z) = x # label("imord2 R").

aK1 follows from middle Bol alone. See Case 13.

Proof of aa1: (in, out, pf, xml)

Miscellaneous Results

This section includes results that might be useful or interesting but don't fit in the previous two sections. Typically these will be intermediate results that (hopefully) will eventually get replaced by stronger results in the previous sections.

Misc 1: Relating aK2 to aK3 with various extra assumptions

Note that the different cases may have different permutations of the variables in the goal clause.

Note also that rather than showing an equality between aK2 and aK3 for some permutation of the variables, it suffices to show that every instance of aK2 is equal to some instance of aK3 and every instance of aK3 is equal to some instance of aK2.

Case 1

Goal clause:

   a(x,K(y,z),u) = a(y,u,K(x,z)) # label("aK2_eq_aK3 (2413)").

Extra assumption:

   a(a(x,y,z),z,u) = 1 # label("aa1{x3/x4}").

Case 2

Goal clause:

   a(x,K(y,z),u) = a(y,x,K(z,u)) # label("aK2_eq_aK3 (2134)").

Extra assumption:

   a(a(x,y,z),u,w) = a(a(x,y,u),z,w) # label("aa1_34").

Case 3

Goal clause:

   a(x,K(y,z),u) = a(u,x,K(y,z)) # label("aK2_eq_aK3 (4123)").

Extra assumption:

   a(x,a(y,z,u),u) = 1 # label("aa2{x4/x5}").

Case 4

Goal clause:

   a(x,K(y,z),u) = a(y,u,K(x,z)) # label("aK2_eq_aK3 (2413)").

Extra assumption:

   a(x,y,a(y,z,u)) = 1 # label("aa3{x2/x3}").

Case 5

Goal clause:

   a(x,K(y,z),u) = a(x,y,K(u,z)) # label("aK2_eq_aK3 (1243)").

Extra assumption:

   ((1 / x) \ y) * (z * x) = x * ((y * z) * x) # label("Osborn").

Case 6

Goal clause:

   a(x,K(y,z),u) = a(x,y,K(u,z)) # label("aK2_eq_aK3 (1243)").

Extra assumption:

   x * ((y * x) \ 1) = y \ 1 # label("WIP").

Case 7

Goal clause:

   a(x,K(y,z),u) = a(y,z,K(u,x)) # label("aK2_eq_aK3 (2341)").

Extra assumption:

   ((x * y) \ 1) * ((x \ 1) \ 1) = y \ 1 # label("DWIP").

Case 8

Goal clause:

   a(x,K(y,z),u) = a(x,y,K(u,z)) # label("aK2_eq_aK3 (1243)").

Extra assumption:

   (1 / x) * (x * y) = y # label("LIP").

Case 9

Goal clause:

   a(x,K(y,z),u) = a(y,u,K(z,x)) # label("aK2_eq_aK3 (2431)").

Extra assumption:

   T(T(x,y),y) = x # label("imord2 T").

It follows that

   K(x,y) = K(y,x) # label("Kcom").

also suffices for permutation 2431, since it is easily shown to be equivalent to imord2 T in AIM.

Case 10

Goal clause:

   a(x,K(y,z),u) = a(y,u,K(z,x)) # label("aK2_eq_aK3 (2431)").

Extra assumption:

   K(x,y) = K(y,x) # label("Kcom").

Case 11

Goal clause:

   a(x,K(y,z),u) = a(u,x,K(y,z)) # label("aK2_eq_aK3 (4123)").

Extra assumptions:

   a(a(x,y,z),u,x) = 1 # label("aa1{x1/x5}").
   a(a(x,y,z),u,w) = a(a(x,y,z),w,u) # label("aa1_45").

Case 12

Goal clause:

   a(x,K(y,z),u) = a(y,z,K(u,x)) # label("aK2_eq_aK3 (2341)").

Extra assumption:

   a(a(x,y,z),u,w) = a(a(x,y,z),w,u) # label("aa1_45").

Case 13

Goal clause:

   a(x,K(y,z),u) = a(y,u,K(x,z)) # label("aK2_eq_aK3 (2413)").

Extra assumption:

   a(a(x,y,z),u,w) = 1   # label("aa1").

The extra assumption of Case 12, clause aa1_45, is a trivial consequence of aa1, but this result is for a different permutation of aK2_eq_aK3.

Case 14

Goal clause:

   a(x,K(y,z),u) = a(y,z,K(u,x)) # label("aK2_eq_aK3 (2341)").

Extra assumption:

   ((x * (y * z)) * x) * y = (x * y) * (z * (x * y)) # label("RIF").

Case 15

Goal clause:

   a(x,K(y,z),u) = a(x,u,K(y,z)) # label("aK2_eq_aK3 (1423)").

Extra assumptions:

   % nuclear squares
   (x * x) * (y * z) = ((x * x) * y) * z # label("NucSq_l").
   (x * (y * y)) * z = x * ((y * y) * z) # label("NucSq_m").
   (x * y) * (z * z) = x * (y * (z * z)) # label("NucSq_r").

Here is a units-only derivation of

   a(x * y,y,K(z,u)) = a(x,K(u,z),y).

Rather than showing an equality between aK2 and aK3 for some permutation of the variables, this says that every instance of aK2 is equal to an instance of aK3. Substituting w/y for x and simplifying yields

   a(w,y,K(z,u)) = a(w/y,K(u,z),y).

which says that every instance of aK3 is equal to an instance of aK2.

Case 16

Goal clauses:

   a(x,y,K(y * z,u)) = a(y,K(u,x),z) # label("aK2_eq_aK3").
   a(x,y,K(w,u)) = a(y,K(u,x),y \ w) # label("aK2_eq_aK3").

Extra assumption:

   % automorphic inverse property (AIP)
   (1 / x) * (1 / y) = 1 / (x * y) # label("AIP").

The proof was initially found by running with different lexical orderings, accumulating partial results along the way. The proof was found at the 10th iteration, with results from 4 of the 9 previous orderings contributing to the proof.

Case 17

Goal clause:

   a(x,K(y,z),u) = a(z,y,K(x,u)) # label("aK2_eq_aK3 (3214)").

Extra assumption:

   % automorphic inverse property (AIP)
   (1 / x) * (1 / y) = 1 / (x * y) # label("AIP").

AIP is covered in Case 16, but this version is for a nicer goal.

Case 18

Goal clause:

   a(x,K(y,z),u) = a(x,y,K(u,z)) # label("aK2_eq_aK3 (1243)").

Extra assumptions:

   (x * y) * x = x * (y * x) # label("flex").

Case 19

Goal clause:

   a(x,K(y,z),u) = a(u,z,K(x,y)) # label("aK2_eq_aK3 (4312)").

Extra assumption:

   % antiautomorphic inverse property (AAIP)
   (1 / x) * (1 / y) = 1 / (y * x) # label("AAIP").

Case 20

Goal clause:

   a(x,K(y,z),u) = a(z,x,K(u,y)) # label("aK2_eq_aK3 (3142)").

Extra assumption:

   % generalized left Bol
   (x * (y * x)) * ((1 / x) * z) = x * (y * z) # label("gen left Bol").

Case 21

Goal clause:

   a(x,K(y,z),u) = a(x,z,K(y,u)) # label("aK2_eq_aK3 (1324)").

Extra assumption:

   K(K(x,y),z) = 1 # label("KK").

Case 22

Goal clause:

   a(x,K(y,z),u) = a(x,y,K(u,z)) # label("aK2_eq_aK3 (1243)").

Extra assumption:

   a(a(K(x,y),z,u),w,v5) = 1 # label("nil3 15, aK1-Nl").

The extra assumption is a lemma (but not yet proved with Prover9), so this is a general AIM result.

We now have a proof of aK2_eq_aK3 (1243) with no extra assumptions. This is posted in the Result 3 section above.

Here is a summary of results relating the 4 single-a goals.

Consequences of aK2_eq_aK3 (1243)

The result for permutation (1243) => the result for 11 other permutations of aK3.

48 of the 96 permutations of single a goals (12 for each) then follow as trivial corollaries.

We do not yet have the aK2_eq_aK3 result for any of the other 12 permutations of aK3, but we have a proof that the result for permutation (1234) => the result for the remaining 11.

Misc 2: A proper instance of aK3 suffices to prove aK3

Extra assumption:

   a(x,y * ((L(z,y,x) \ 1) \ T((L(z,y,x) \ 1) * z,u)),K(u,L(z,y,x) \ 1)) = 1 # label("aK3 instance").

Misc 3: generalized Bol => Osborn

   (x * (y * x)) * ((1 / x) * z) = x * (y * z) # label("gen left Bol").
   (x * (y \ 1)) * ((y * z) * y) = (x * z) * y # label("gen right Bol").

   ((1 / x) \ y) * (z * x) = x * ((y * z) * x) # label("Osborn 1").
   (x * y) * (z / (x \ 1)) = (x * (y * z)) * x # label("Osborn 2").
   (1 / x) \ (((1 / x) * y) * z) = (y * (z * x)) / x # label("Osborn 3").
   x \ ((x * y) * z) = (y * (z * (x \ 1))) / (x \ 1) # label("Osborn 4").

Proof: (in, out, pf, xml)

The 4 versions of the Osborn condition are equivalent, but all 4 are included as goals here for the additional hints taken from the proofs.

Misc 4: Three proper instances of aa1 suffice to prove aa2

Extra assumptions:

   a(a(x,1 / T(y,z * w),u),(((a(x,1 / T(y,z * w),u) \ ((x * ((1 / T(y,z * w)) * u)) \ (x * u))) * z) * w) / (z * w),z * w) = 1 # label("aa1_1").

   a(a(x,1 / T(y,z * w),u),a(x,1 / T(y,z * w),u) \ ((x * ((1 / T(y,z * w)) * u)) \ (x * u)),z) = 1 # label("aa1_2").

   a(a(x,1 / T(y,z * w),u),(a(x,1 / T(y,z * w),u) \ ((x * ((1 / T(y,z * w)) * u)) \ (x * u))) * z,w) = 1 # label("aa1_3").

Misc 5: All 32 nil3 clauses assuming 2 extra assumptions

Extra assumptions:

   a(a(x,y,z),u,x) = 1 # label("aa1{x1/x5}").
   a(a(x,y,z),u,w) = a(a(x,y,z),w,u) # label("aa1_45").

Proofs 1-23

Proofs 24-32

Misc 6: Other results with extra assumption aa1_45

Extra assumption:

   a(a(x,y,z),u,w) = a(a(x,y,z),w,u) # label("aa1_45").

Case 1

aa1_45 => nil3 {7,15,18}

   K(a(x,a(y,z,u),w),v5) = 1 # label("nil3 7, aa2-C").
   a(a(K(x,y),z,u),w,v5) = 1 # label("nil3 15, aK1-Nl").
   a(x,a(K(y,z),u,w),v5) = 1 # label("nil3 18, aK1-Nm").

Case 2

aa1_45 => all 15 of the 32 original nil3 properties having exactly 1 occurrence of K

This combines the following posted nil3 results.

Case 3

aa1_45 => all 9 of the 32 original nil3 properties having 0 occurrences of K

   a(a(a(x,y,z),u,w),v5,v6) = 1 # label("nil3 24, aa1-Nl").
   a(a(x,a(y,z,u),w),v5,v6) = 1 # label("nil3 25, aa2-Nl").
   a(a(x,y,a(z,u,w)),v5,v6) = 1 # label("nil3 26, aa3-Nl").
   a(x,a(a(y,z,u),w,v5),v6) = 1 # label("nil3 27, aa1-Nm").
   a(x,a(y,a(z,u,w),v5),v6) = 1 # label("nil3 28, aa2-Nm").
   a(x,a(y,z,a(u,w,v5)),v6) = 1 # label("nil3 29, aa3-Nm").
   a(x,y,a(a(z,u,w),v5,v6)) = 1 # label("nil3 30, aa1-Nr").
   a(x,y,a(z,a(u,w,v5),v6)) = 1 # label("nil3 31, aa2-Nr").
   a(x,y,a(z,u,a(w,v5,v6))) = 1 # label("nil3 32, aa3-Nr").

Comment

aa1_45 => all 32 of the original nil3 properties

This follows from the following posted results.

Combining the 32 proofs in a single run: (in, out, pf, xml)

It follows that in order to prove that AIM loops are nilpotent of class 3, it suffices to prove any one of {aa1,aa2,aa3}.

Case 4

aa1_45 + aK1 => aa1

Additional extra assumption:

   a(K(x,y),z,u) = 1 # label("aK1").

Proved clause:

   a(a(x,y,z),u,w) = 1 # label("aa1").

It follows that in order to prove the primary AIM conjecture, it suffices to prove any one of {Ka,aK1,aK2,aK3} and aa1_45.

Misc 7: AIM loops are nilpotent of class at most 3

This result relies on a high-level mathematical argument that makes use of the following Prover9 lemmas. To complete the proof with Prover9, it will suffice, for example, to prove that middle Bol + KK => aa1.

In addition to the results posted here, Michael Kinyon has a page here.

Part 1: middle Bol + KK => 6 instances of the aa goals

Extra assumptions:

   x * ((y * z) \ x) = (x / z) * (y \ x) # label("middle Bol").
   K(K(x,y),z) = 1                       # label("KK").

Proved clauses:

   a(a(x,x,z),u,w) = 1 # label("aa1{x1/x2}").
   a(a(x,y,y),u,w) = 1 # label("aa1{x2/x3}").
   a(x,a(y,y,u),w) = 1 # label("aa2{x2/x3}").
   a(x,a(y,z,z),w) = 1 # label("aa2{x3/x4}").
   a(x,y,a(z,z,w)) = 1 # label("aa3{x3/x4}").
   a(x,y,a(z,u,u)) = 1 # label("aa3{x4/x5}").

Part 2: middle Bol + KK + 6 instances of the aa goals => Ka

Extra assumptions:

   x * ((y * z) \ x) = (x / z) * (y \ x) # label("middle Bol").
   K(K(x,y),z) = 1                       # label("KK").

   a(a(x,x,z),u,w) = 1 # label("aa1{x1/x2}").
   a(a(x,y,y),u,w) = 1 # label("aa1{x2/x3}").
   a(x,a(y,y,u),w) = 1 # label("aa2{x2/x3}").
   a(x,a(y,z,z),w) = 1 # label("aa2{x3/x4}").
   a(x,y,a(z,z,w)) = 1 # label("aa3{x3/x4}").
   a(x,y,a(z,u,u)) = 1 # label("aa3{x4/x5}").

Proved clause:

   K(a(x,y,z),u) = 1 # label("Ka").

Combining results: middle Bol + KK => aK1

Extra assumptions:

   x * ((y * z) \ x) = (x / z) * (y \ x) # label("middle Bol").
   K(K(x,y),z) = 1                       # label("KK").

Proved clause:

   a(K(x,y),z,u) = 1     # label("aK1").

Other results

We know from posted lemmas that middle Bol => the 23/32 nil3 clauses having at least one occurrence of K. It remains to prove the 9/32 having 0 occurrences of K.

Here is a proof that it suffices to prove just one of the 9, for example,

   a(a(a(x,y,z),u,w),v5,v6) = 1   # label("nil3 24, aa1-Nl").

Proof: (in, out, pf, xml)

Misc 8: Consequences of two versions of aK2_eq_aK3

Michael Kinyon's AIM Problem Again page includes some results with the following two extra assumptions.

   a(x,K(y,z),u) = a(x,y,K(u,z)) # label("aK2_eq_aK3 (1243)").
   a(x,K(y,z),u) = a(x,u,K(y,z)) # label("aK2_eq_aK3 (1423)").

Results:

all 15 of the 32 nil3 properties having exactly 1 occurrence of K

aK3 with squares

a(x,y,K(z,u)) * a(x,y,K(z,u)) = 1  # label("aK3_aK3").
a(x * x,y,K(z,u)) = 1              # label("aK3_xx").
a(x,y * y,K(z,u)) = 1              # label("aK3_yy").
a(x,y,K(z * z,u)) = 1              # label("aK3_zz").
a(x,y,K(z,u * u)) = 1              # label("aK3_uu").

Misc 9: Consequences of UFlex

Extra assumption:

   (((x / u) * (v \ y)) / u) * (v \ x) = (x / u) * (v \ ((y / u) * (v \ x))) # label("UFlex").

Results:

UFlex => AAIP

Goal:

   (1 / x) * (1 / y) = 1 / (y * x) # label("AAIP").

Proof: (in, out, pf, xml)

UFlex => middle Bol

Goal:

   x * ((y * z) \ x) = (x / z) * (y \ x) # label("middle Bol").

Proof: (in, out, pf, xml)

Misc 10: Reciprocals behaving like 1

Reciprocals:

   (x / y) * (y / x) 
   (x \ y) * (y \ x)

Results:

Commutativity => L3 reciprocal

   L(x,y,(x \ z) * (z \ x)) = x # label("L3 reciprocal").

Proof: (in, out, pf, xml)

This work was supported in part by the AI4REASON ERC Consolidator grant nr. 649043, the Czech project AI&Reasoning CZ.02.1.01/0.0/0.0/15_003/0000466 and the European Regional Development Fund.