AIM (Redone)

November 2020


Main Conjecture: AIM => {Ka,aK1,aK2,aK3,aa1,aa2,aa3}

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.

   % cancellation laws
   x * y = u & x * z = u -> y = z.
   y * x = u & z * x = u -> y = z.

      % other form
      x * y = x * z -> y = z.
      y * x = z * x -> y = z.

   % useful in demodulation free runs
   x != y | z * x = z * y.
   x != y | x * z = y * z.

   % 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).

   % obvious compatibility
   a(x,y,z) = 1 -> L(z,y,x) = z.
   L(x,y,z) = x -> a(z,y,x) = 1.
   T(x,y) = x -> T(y,x) = y.
   T(x,y) = x -> K(x,y) = 1.
   K(x,y) = 1 -> T(x,y) = 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).

   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").

   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.
In addition to the results presented here, Michael Kinyon 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}

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

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

   a(K(x,y),z,u) = a(x,z,K(u,y)) # label("aK1_eq_aK3").
(in, out, pf, xml)
   K(a(x,y,z),u) = a(x,y,K(z,u)) # label("Ka_eq_aK3").
(in, out, pf, xml)
   K(a(x,y,z),u) = K(x,a(u,y,z)) # label("Ka1_eq_Ka2").
(in, out, pf, xml)
An analogous result for aK2 remains open.

Result 4: Some properties of a and K

   K(x,y) * a(u,v,w) = a(u,v,w) * K(x,y) # label("aKcom").
(in, out, pf, xml)
   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").
(in, out, pf, xml)
   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").
(in, out, pf, xml)
   K(x,K(y,z * z)) = 1               # label("Ksqmap"). 
(in, out, pf, xml)

Result 5: Some properties of T, L and R

   1 / (1 / T(x,y)) = T(1 / (1 / x),y)     # label("T property").
   1 / (1 / L(x,y,z)) = L(1 / (1 / x),y,z) # label("L property").
   1 / (1 / R(x,y,z)) = R(1 / (1 / x),y,z) # 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").
(in, out, pf, xml)
   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").
(in, out, pf, xml)

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.

(in, out, pf, xml)

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.

(in, out, pf, xml)

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,
1 has 3 occurrences of K
7 have 2 occurrences of K
15 have 1 occurrence of K
9 have 0 occurrences of K
Nil3 Result 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").
(in, out, pf, xml)
Nil3 Result 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").
(in, out, pf, xml)
Nil3 Result 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").
(in, out, pf, xml)
Nil3 Result 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").
(in, out, pf, xml)

In addition to the results presented here, Michael Kinyon has a page on nil3. It includes a list of known dependencies among the 32. We are working on proving more of these dependencies.

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)

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.
Case 1
Goal clause (permutation 2413):
   a(x,K(y,z),u) = a(y,u,K(x,z)) # label("aK2_eq_aK3").
Extra assumption:
   a(a(x,y,z),z,u) = 1 # label("aa1{x3/x4}").
(in, out, pf, xml)
Case 2
Goal clause (permutation 2134):
   a(x,K(y,z),u) = a(y,x,K(z,u)) # label("aK2_eq_aK3").
Extra assumption:
   a(a(x,y,z),u,w) = a(a(x,y,u),z,w) # label("aa1_34").
(in, out, pf, xml)
Case 3
Goal clause (permutation 4123):
   a(x,K(y,z),u) = a(u,x,K(y,z)) # label("aK2_eq_aK3").
Extra assumption:
   a(x,a(y,z,u),u) = 1 # label("aa2{x4/x5}").
(in, out, pf, xml)
Case 4
Goal clause (permutation 2413):
   a(x,K(y,z),u) = a(y,u,K(x,z)) # label("aK2_eq_aK3").
Extra assumption:
   a(x,y,a(y,z,u)) = 1 # label("aa3{x2/x3}").
(in, out, pf, xml)
Case 5
Goal clause (permutation 1243):
   a(x,K(y,z),u) = a(x,y,K(u,z)) # label("aK2_eq_aK3").
Extra assumption:
   ((1 / x) \ y) * (z * x) = x * ((y * z) * x) # label("Osborn").
(in, out, pf, xml)
Case 6
Goal clause (permutation 1243):
   a(x,K(y,z),u) = a(x,y,K(u,z)) # label("aK2_eq_aK3").
Extra assumption:
   x * ((y * x) \ 1) = y \ 1 # label("WIP").
(in, out, pf, xml)
Case 7
Goal clause (permutation 2341):
   a(x,K(y,z),u) = a(y,z,K(u,x)) # label("aK2_eq_aK3").
Extra assumption:
   ((x * y) \ 1) * ((x \ 1) \ 1) = y \ 1 # label("DWIP").
(in, out, pf, xml)
Case 8
Goal clause (permutation 1243):
   a(x,K(y,z),u) = a(x,y,K(u,z)) # label("aK2_eq_aK3").
Extra assumption:
   (1 / x) * (x * y) = y # label("LIP").
(in, out, pf, xml)
Case 9
Goal clause (permutation 2431):
   a(x,K(y,z),u) = a(y,u,K(z,x)) # label("aK2_eq_aK3").
Extra assumption:
   T(T(x,y),y) = x # label("imord2 T").
(in, out, pf, xml)
Case 10
Goal clause (permutation 2431):
   a(x,K(y,z),u) = a(y,u,K(z,x)) # label("aK2_eq_aK3").
Extra assumption:
   K(x,y) = K(y,x) # label("Kcom").
(in, out, pf, xml)
Case 11
Goal clause (permutation 4123):
   a(x,K(y,z),u) = a(u,x,K(y,z)) # label("aK2_eq_aK3").
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").
(in, out, pf, xml)
Case 12
Goal clause (permutation 2341):
   a(x,K(y,z),u) = a(y,z,K(u,x)) # label("aK2_eq_aK3").
Extra assumption:
   a(a(x,y,z),u,w) = a(a(x,y,z),w,u) # label("aa1_45").
(in, out, pf, xml)

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").
(in, out, pf, xml)

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").
(in, out, pf, xml)

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
Proved nil3 clause:
   K(a(x,a(y,z,u),w),v5) = 1 # label("nil3 7, aa2-C").
(in, out, pf, xml)
Case 2
Proved nil3 clause:
   a(a(K(x,y),z,u),w,v5) = 1 # label("nil3 15, aK1-Nl").
(in, out, pf, xml)
Case 3
Proved nil3 clause:
   a(x,a(K(y,z),u,w),v5) = 1 # label("nil3 18, aK1-Nm").
(in, out, pf, xml)
Case 4
aa1_45 => all 15 of the 32 original nil3 properties having exactly 1 occurrence of K.
(in, out, pf, xml)
This combines the following posted nil3 results.
aa1_45 => nil3 15

aa1_45 => nil3 18

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

Case 5
Proved nil3 clause:
   a(x,a(y,a(z,u,w),v5),v6) = 1 # label("nil3 28, aa2-Nm").
(in, out, pf, xml)
Notes concerning aa1_45 and the 32 original nil3 properties
Subject to review and confirmation, we believe we have aa1_45 => all 32 nil3 properties based on the following.
All 8 of the 32 nil3 properties having > 1 occurrence of K are AIM lemmas. (posted)

aa1_45 => all 15 of the 32 nil3 properties having exactly 1 occurrence of K. (posted)

aa1_45 => nil3 28 (posted)

aa1_45 => nil3 31 (under review)

aa1_45 + nil3 31 => nil3 25 (under review)

aa1_45 + nil3 {25,28,31} => nil3 {24,26,27,29,30,32} (under review)

Case 6
Additional extra assumption:
   a(K(x,y),z,u) = 1 # label("aK1").
Proved clause:
   a(a(x,y,z),u,w) = 1 # label("aa1").
(in, out, pf, xml)
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.
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.