QG-Ring Examples from R. Padmanabhan

    From: Ranganathan Padmanabhan
    Subject: Re: loops, quasigroups, nonassociative systems
    Date: Fri, 17 Jun 2005
    To: William McCune
    
    On Jun 15, 2005, at 9:43 AM, William McCune wrote:

    > RP,
    >
    > I'll be giving an invited talk on July 7 at the Denver conference
    > on loops, quasigroups, and nonassociative systems.  See
    >
    >         http://www.math.du.edu/milehigh/
    >
    > This talk will be the official release of Prover9.  I plan to
    > give several detailed example problems and proofs, though
    > I haven't yet decided on the problems.
    >
    > Can you suggest some problems that would be of interest to that
    > audience?  I'm looking for easy problems as well has medium
    > and harder ones, and also counterexample problems for Mace4.

    Hi Bill,
    
    Here is a Problem on quasigroups which might be amenable for  
    treatment by Otter, Mace and Prover9.
    
    A Sample Theorem (due to R.P. and Barry Wolk)
    
    Let K be the set of all algebras of type (2) satisfying the four  
    identities given below.
    
         1. (x * E) * x = x.
         2. x* (x * y) = y.
         3. (x * y) * (z * u) = (x * z) * (y * u).
         4. ((x * x) * x) * x = ((y * y) * y) * y  (=E).
    
    Then K satisfies all the identities valid in the ring model (Z[7]; 3x- 
    y). In other words, the variety K has a solvable word problem!
    Also every model of K is imbeddable in a quasigroup.
    
    Solution to the word problem is given like this: An identity f=g is a  
    consequence of {1,2,3,4} if and only if it is true in the ring model  
    mentioned above.
    
    Applying MACE and OTTER to prove the above statements.
    
    Step#1.
    MACE. Get a ring model. A non-trivial one must be x*y = 3x - y (mod 7).

    Step#2.
    Use Otter to derive the two cancellation laws.
    Right cancellation is obvious: x*y = x*z  => x*(x*y) = x*(x*z)  =>   
    y=z  by (2).
    Left cancellation law: x*z = y*z => x=y also follows from the above  
    but not obvious and Otter will love proving this.

    Step#3
    Prove that E (defined in Id #4) is idempotent.

    Human Steps.
    By a result of M. Sholander, any cancellative medial groupoid with an  
    idempotent element is imbeddable in a medial quasigroup satisfying  
    the same identities of the original algebra. So any algebra belonging  
    to K is a sugroupoid of such a quasigroup. Finally, the classic  
    Toyoda-Bruck theorem asserts that every medial quasigroup is isotopic  
    to an abelian group i.e. a ring model. So x*y = ax + by and plugging  
    in the above four equations, one shows that 3x-y (mod 7) is the only  
    solution for this set of equations.
    
    In particular, the identity ((x * y) * z) * u = ((u * y) * z) * x,  
    which is true in the ring model 3x-y (mod 7), must now be an  
    equational  consequence of the four identites. This creates new  
    problems for Otter, Prover9.
    Prove this using Otter or Prover9.
    Again, two methods.
    
    Method I
    Prove directly    {1,2,3,4} ==> ((x * y) * z) * u = ((u * y) * z) * x.

    Method II.
    Prove ((x * y) * z) * u = ((u * y) * z) * x from {1,2,3,4, quasigroup  
    property, skolemize i.e. type (2,2,2) with*,/,\ }.

    Obviously Method I is preferable.
    
    Thus we have a very good example of a theorem differentiating the  
    "simplicity-and-elegance" of a human proof compared to the  
    "complexity-in-details" of a first order proof. Also, there is no  
    immediate first order human proof of
    {1,2,3,4} ==> ((x * y) * z) * u = ((u * y) * z) * x.
    But theorem-provers can do this.
    
    Conjecture: This variety defined by the four identities above is one- 
    based.
    If true, only machines can do this (using, of course, human designed  
    equational filters to eliminate "bad" guys).
    
    
    Other (relatively easy) Problems:
    
    Prove that x*(y*(y*x)) = y*x  implies y*(y*x) = x*y in quasigroups  

    but not in cancellative groupoids.

    Prove that (xy)(zu) = (xz)(yu) implies (x(yz))((uv)w) = (x(uz))((yv)w)
    in cancellation groupoids with an idempotent or under (gL)
    but not in general.  (Prover9, Otter with gL), Mace).

    Good luck with your conference.
    
    R. P.