Higman-Neumann characterization of groups

Stream: Equational

[Bruno Le Floch]

The Tour of selected equations ends with

Equation 42323216 x = y ◇ ((((y ◇ y) ◇ x) ◇ z) ◇ (((y ◇ y) ◇ y) ◇ z)): the Higman-Neumann axiom
This axiom characterizes division in a (not necessarily abelian) group, as was worked out by Higman and Neumannin in 1956. It appears to be the shortest such axiom.

It is perhaps not the only shortest one, and might not be the first in our numbering. Such an axiom has to be obeyed by the division operation x/y=xy⁻¹ in a group, has to involve at least three variables (to imply associativity), and has to involve at least three operations once squares are replaced by an identity element. These structural constraints reduce the number of equations to 10 for 6 ops and 1963 for 8 ops, respectively; for instance for 6 operations,

x = (y ◇ y) ◇ ((y ◇ z) ◇ (x ◇ (z ◇ y)))
x = (y ◇ y) ◇ ((z ◇ y) ◇ (x ◇ (y ◇ z)))
x = (y ◇ y) ◇ ((z ◇ w) ◇ (x ◇ (w ◇ z)))
x = (y ◇ z) ◇ (((x ◇ x) ◇ x) ◇ (z ◇ y))
x = (y ◇ z) ◇ (((y ◇ y) ◇ x) ◇ (z ◇ y))
x = (y ◇ z) ◇ (((z ◇ z) ◇ x) ◇ (z ◇ y))
x = (y ◇ z) ◇ (((w ◇ w) ◇ x) ◇ (z ◇ y))
x = ((y ◇ y) ◇ ((y ◇ z) ◇ x)) ◇ (z ◇ y)
x = ((y ◇ y) ◇ ((z ◇ y) ◇ x)) ◇ (y ◇ z)
x = ((y ◇ y) ◇ ((z ◇ w) ◇ x)) ◇ (w ◇ z)

What simple criteria can I use to rule out these equations as being inequivalent to groups? This would allow me to reduce further the set of 8-ops equations to check for equivalence to the Higman-Neumann axiom.

[Jose Brox]

Bruno Le Floch ha dicho:
(EDITED since I had made some mistake with the first candidate identity)

What simple criteria can I use to rule out these equations as being inequivalent to groups?

This kind of question interests me a lot too!

One first idea is to use derived identities. If the operation actually is $x*y = xy^{-1}$ then in particular, $1_y:=y*y$ should act as the identity element and $i_y(x):=(y*y)*x$ should define the inverse operator, so they must satisfy specific identities such as $x*x = y*y$, $x*(y*y) = x$, etc.

A second, more definitive idea is to slice the Higman-Neumann identity into smaller, equivalent ones. This way, each candidate identity either satisfies all the identities characterizing right division, or fails some. In the Higman-Neumann paper itself appears a set of two smaller identities characterizing a magma operation as right division in a group:

$(x*z)*(y*z) = x*y \,\, (A)$
$(x*x)*((y*y)*y) = y. \,\, (B)$

With all this we can analyze your list of candidates (I'm using Prover9/Mace4):

1) EDITED: Satisfies (B) but not (A), Vampire-SAT quickly finds a countermodel. Mace4 finds a counterexample too, of size 7, in 78s.
Mace4 Higman-Neumann 1st candidate discarded identity (A).txt
2) Does not imply $x*x = y*y$.
3) Implies (B) but not (A)! There is a countermodel of size 7 (66s to find it).
Mace4 Higman-Neumann 3rd candidate discarded identity (A)
4) Discarded by $x*x = y*y$.
5) Implies (B), (A) is hard to check! Still running after 20min.
6) Discarded by $x*x = y*y$.
7) Implies (B), (A) is hard to check, still running.
8) Implies (B) but not (A). There is a countermodel of size 5 (found in 0s).
9) Discarded by $x*x = y*y$.
10) Implies (B) but not (A). There is a countermodel of size 7 (found in 38s).

[Jose Brox]

(EDITED to include here Candidate 1 too)
Jose Brox ha dicho:

5) Implies (B), (A) is hard to check! Still running after 20min.
7) Implies (B), (A) is hard to check, still running.

Ok, Vampire-SAT solves these two really fast! It finds countermodels for (A) in less than a second.

The TPTPs are the following:

Candidate 5

fof(candidate5, axiom,
X = m(m(Y,Z),m(m(m(Y,Y),X),m(Z,Y)))
).

fof(identityA, conjecture,
m(m(X,Z),m(Y,Z)) = m(X,Y)
).

Candidate 7

fof(candidate7, axiom,
X = m(m(Y,Z),m(m(m(W,W),X),m(Z,Y)))
).

fof(identityA, conjecture,
m(m(X,Z),m(Y,Z)) = m(X,Y)
).

And for Candidate 1

fof(candidate1, axiom,
X = m(m(Y,Y),m(m(Y,Z),m(X,m(Z,Y))))
).

fof(identityA, conjecture,
m(m(X,Z),m(Y,Z)) = m(X,Y)
).

The countermodels are attached.
Vampire-SAT Higman-Neumann 1st candidate countersatisfiable.txt
Vampire-SAT Higman-Neumann 5th candidate countersatisfiable.txt
Vampire-SAT Higman-Neumann 7th candidate countersatisfiable.txt

[Jose Brox]

(deleted)

[Bruno Le Floch]

Thank you! I will try to learn Vampire and report in a few days how successful I was with filtering the order 8 equations.
Some of the magmas themselves are intriguing, for instance the one for equation 1 is not a linear one (one can check that dimension-1 linear magmas obeying that equation are just subtraction), but still has x*x = e for some constant e, and e*(e*x)=x and x*e=x.

[Bruno Le Floch]

@Jose Brox I've installed vampire. Running it on your tptp as vampire problem.p without options only gives me timeouts. Are you using any particular option?

[Jose Brox]

Bruno Le Floch ha dicho:

I've installed vampire. Running it on your tptp as vampire problem.p

What I have used is Vampire-SAT from TPTP.org, which there appears listed as a different solver than Vampire. I suppose there is some option to force the use of the SAT solver in Vampire from the start, but I don't know the program at all...

[Jose Brox]

Bruno Le Floch ha dicho:

I will try to learn Vampire and report in a few days how successful I was with filtering the order 8 equations.

In which language did you write your filtering script? Something we can do that doesn't directly involve ATPs is to verify if your order 8 equations satisfy the models which are not satisfied by Identity (A). In fact, all the order 6 candidates can be falsified by the same magma!

I have just written Python code for this, in case you want to use it:
Finite model checker.py

[Jose Brox]

Then, after a first filtering, we can use an ATP to find other countermodels for some of the remaining candidates, and filter all of them again.

[Jose Brox]

Bruno Le Floch ha dicho:

I've installed vampire.

Nevertheless, look at my message "Big difference with Mace4", now the difference with Vampire-SAT is not that relevant (and I can use Mace4 with more ease).

[Jose Brox]

Jose Brox ha dicho:

In fact, all the order 6 candidates can be falsified by the same magma!

Here I see that we are rediscovering McCune's and Kinyon's result that a magma of size 7 falsifies all candidates of sizes (15,3) and (15,4) in their terminology (so of order 6 with 3 or 4 variables, as you had). They state that this magma is the smallest nonassociative inverse loop.

[Bruno Le Floch]

It's really great that you found that! I had not read that page, it seems they have already done most of what we were thinking of here? They get all the way to 23 candidates. I guess we can double-check their work (or formalize it), and try a bit to see which of the 23 remaining candidates we can rule out.

[Bruno Le Floch]

I'm integrating your (their) 7-element example into my messy code and cleaning up a bit before posting it here.

[Jose Brox]

Bruno Le Floch ha dicho:

It's really great that you found that! I had not read that page, it seems they have already done most of what we were thinking of here? They get all the way to 23 candidates.

If I understand correctly, they look at slightly different things: 1) a single axiom for groups depending only on right division, 2) a single axiom for groups depending only on product and inverse.

Then for division 1) they check candidates of sizes (11,3),(15,3),(15,4), while Higman-Neumann is of size (19,3), and your order 8 examples must be of sizes either (19,3) or (19,4) (or more if they have more than 4 variables). Here 19 = 8 + 9 + 1 +1, 8 products and 9 variable occurrences at the RHS, 1 equal sign, 1 isolated variable $x$ at the LHS. So they have only checked the smaller sizes of the problem.

It is for product and inverse 2) where they reduced the list to 21 possible candidates (and no one ever finished this? We should look!).

[Jose Brox]

Bruno Le Floch ha dicho:

I'm integrating your (their) 7-element example into my messy code and cleaning up a bit before posting it here.

I'm not sure if they are the same magma, for most of your candidates I have found that there are 3 non-isomorphic countermodels of size 7.
Mace4 Higman-Neumann 1st candidate discarded identity (A) 3 models size 7 portable.txt

[Bruno Le Floch]

You're right that they did not rule out shorter axioms than their 8-operation axiom for division! I had only skimmed that page sorry. Regarding literature search, I will let others do it as I'm usually terrible at that. Did they publish their work anywhere as an actual article? I cannot find anything.

[Bruno Le Floch]

There are no 6-operation laws and 727 8-operation laws of the form x=RHS with at least three variables, such that every variable appears an even number of times, and that are violated by all four 7-element magmas that we mentioned.
These laws come in clusters of a parent law with many variables, that can be specialized by taking some variables to be equal. The first "parent" law is

Equation 42359357: x = y ◇ ((((z ◇ z) ◇ x) ◇ w) ◇ (((u ◇ u) ◇ y) ◇ w))

from which there are 16 specializations,

Equations 42302808, 42302852, etc

Equation 42302808: x = y ◇ ((((x ◇ x) ◇ x) ◇ y) ◇ (((z ◇ z) ◇ y) ◇ y))
Equation 42302852: x = y ◇ ((((x ◇ x) ◇ x) ◇ z) ◇ (((x ◇ x) ◇ y) ◇ z))
Equation 42302946: x = y ◇ ((((x ◇ x) ◇ x) ◇ z) ◇ (((y ◇ y) ◇ y) ◇ z))
Equation 42303040: x = y ◇ ((((x ◇ x) ◇ x) ◇ z) ◇ (((z ◇ z) ◇ y) ◇ z))
Equation 42303162: x = y ◇ ((((x ◇ x) ◇ x) ◇ z) ◇ (((w ◇ w) ◇ y) ◇ z))
Equation 42323078: x = y ◇ ((((y ◇ y) ◇ x) ◇ y) ◇ (((z ◇ z) ◇ y) ◇ y))
Equation 42323122: x = y ◇ ((((y ◇ y) ◇ x) ◇ z) ◇ (((x ◇ x) ◇ y) ◇ z))
Equation 42323216: x = y ◇ ((((y ◇ y) ◇ x) ◇ z) ◇ (((y ◇ y) ◇ y) ◇ z))
Equation 42323310: x = y ◇ ((((y ◇ y) ◇ x) ◇ z) ◇ (((z ◇ z) ◇ y) ◇ z))
Equation 42323432: x = y ◇ ((((y ◇ y) ◇ x) ◇ z) ◇ (((w ◇ w) ◇ y) ◇ z))
Equation 42357897: x = y ◇ ((((z ◇ z) ◇ x) ◇ y) ◇ (((x ◇ x) ◇ y) ◇ y))
Equation 42357991: x = y ◇ ((((z ◇ z) ◇ x) ◇ y) ◇ (((y ◇ y) ◇ y) ◇ y))
Equation 42358085: x = y ◇ ((((z ◇ z) ◇ x) ◇ y) ◇ (((z ◇ z) ◇ y) ◇ y))
Equation 42358207: x = y ◇ ((((z ◇ z) ◇ x) ◇ y) ◇ (((w ◇ w) ◇ y) ◇ y))
Equation 42358270: x = y ◇ ((((z ◇ z) ◇ x) ◇ z) ◇ (((x ◇ x) ◇ y) ◇ z))
Equation 42358364: x = y ◇ ((((z ◇ z) ◇ x) ◇ z) ◇ (((y ◇ y) ◇ y) ◇ z))
Equation 42358458: x = y ◇ ((((z ◇ z) ◇ x) ◇ z) ◇ (((z ◇ z) ◇ y) ◇ z))
Equation 42358580: x = y ◇ ((((z ◇ z) ◇ x) ◇ z) ◇ (((w ◇ w) ◇ y) ◇ z))
Equation 42358644: x = y ◇ ((((z ◇ z) ◇ x) ◇ w) ◇ (((x ◇ x) ◇ y) ◇ w))
Equation 42358811: x = y ◇ ((((z ◇ z) ◇ x) ◇ w) ◇ (((y ◇ y) ◇ y) ◇ w))
Equation 42358978: x = y ◇ ((((z ◇ z) ◇ x) ◇ w) ◇ (((z ◇ z) ◇ y) ◇ w))
Equation 42359145: x = y ◇ ((((z ◇ z) ◇ x) ◇ w) ◇ (((w ◇ w) ◇ y) ◇ w))
Equation 42359357: x = y ◇ ((((z ◇ z) ◇ x) ◇ w) ◇ (((u ◇ u) ◇ y) ◇ w))

including the Higman-Neumann axiom (z=u=y). This pattern is more general, where a (candidate) parent law can be specialized in various ways to (less likely to work candidate) laws. The first few parents (extracted by hand from the list) appear to be

First few parent laws

Equation 42359357: x = y ◇ ((((z ◇ z) ◇ x) ◇ w) ◇ (((u ◇ u) ◇ y) ◇ w))
Equation 44446458: x = y ◇ ((((z ◇ z) ◇ x) ◇ (w ◇ y)) ◇ ((u ◇ u) ◇ w))
Equation 48273989: x = y ◇ ((((z ◇ z) ◇ x) ◇ ((w ◇ u) ◇ y)) ◇ (u ◇ w))
Equation 58131773: x = y ◇ ((((z ◇ z) ◇ x) ◇ (((w ◇ w) ◇ u) ◇ y)) ◇ u)
Equation 67958395: x = (y ◇ y) ◇ (z ◇ ((x ◇ w) ◇ (((u ◇ u) ◇ z) ◇ w)))
Equation 68190031: x = (y ◇ y) ◇ (z ◇ ((x ◇ (w ◇ z)) ◇ ((u ◇ u) ◇ w)))
Equation 68654183: x = (y ◇ y) ◇ (z ◇ ((x ◇ ((w ◇ u) ◇ z)) ◇ (u ◇ w)))
Equation 69581861: x = (y ◇ y) ◇ (z ◇ ((x ◇ (((w ◇ w) ◇ u) ◇ z)) ◇ u))
Equation 70978190: x = (y ◇ y) ◇ ((z ◇ w) ◇ (x ◇ ((w ◇ u) ◇ (z ◇ u))))
Equation 71442238: x = (y ◇ y) ◇ ((z ◇ w) ◇ ((x ◇ u) ◇ ((w ◇ z) ◇ u)))
Equation 71906174: x = (y ◇ y) ◇ ((z ◇ w) ◇ ((x ◇ ((u ◇ u) ◇ z)) ◇ w))
Equation 73231955: x = (y ◇ z) ◇ (((w ◇ w) ◇ x) ◇ ((z ◇ u) ◇ (y ◇ u)))
Equation 73300470: x = (y ◇ y) ◇ (((z ◇ w) ◇ u) ◇ ((x ◇ (w ◇ z)) ◇ u))

[Bruno Le Floch]

Here is the code that produces the 727 laws in question. It takes a minute or so.
Higman_Neumann.py

[Jose Brox]

Bruno Le Floch ha dicho:

The first few parents (extracted by hand from the list) appear to be

All of them but 2 are equivalent to the Higman-Neumann axiom! Prover9 shows it in a split second for each axiom (no need of using (A) and (B) with this many variables). We need entering those clusters. Anyway the interesting candidates are those with fewest variables...

The other two parents fail the (A) axiom, and can be discarded by a magma of size 3:
[[ 1, 2, 0],[ 0, 1, 2],[ 2, 0, 1]]

The non-equivalent parents are 71442238 and 71906174:
$x = (y ◇ y) ◇ ((z ◇ w) ◇ ((x ◇ u) ◇ ((w ◇ z) ◇ u)))$
$x = (y ◇ y) ◇ ((z ◇ w) ◇ ((x ◇ ((u ◇ u) ◇ z)) ◇ w))$

[Jose Brox]

Jose Brox ha dicho:

The other two parents fail the (A) axiom, and can be discarded by a magma of size 3:
[[ 1, 2, 0],[ 0, 1, 2],[ 2, 0, 1]]

After adding this countermodel to your script, 501 candidates remain. I will keep the process going.

[Bruno Le Floch]

The three 7-elements models produced by Mace4 that you had listed are equivalent to the one of Higman-Neumann. They have an interesting structure, with three submagmas isomorphic to $\mathbb{Z}/3\mathbb{Z}$ with $x*y=y-x$.
models.py
I'm busy all day today with my day job, sorry.

[Jose Brox]

Bruno Le Floch ha dicho:

The three 7-elements models produced by Mace4 that you had listed are equivalent to the one of Higman-Neumann.

You mean that they are isomorphic? (Looking at your script, you find the permutation between them, right?). But Mace4's isofilter says they are not isomorphic! :face_with_spiral_eyes:

[Jose Brox]

Indeed, we can remove 3 of the 4 models in your script and still 727 candidates remain.

[Jose Brox]

Jose Brox ha dicho:

After adding this countermodel to your script, 501 candidates remain. I will keep the process going.

After adding another countermodel, we go down to 449. Then I've had a curious idea: I have tested your filtering code for identities with two variables, and 4 passed the test! These have given 3 countermodels of size 3, and with those we further reduce the number of candidates to 390.

[Amir Livne Bar-on]

Is it a coincidence that there is a law capturing the idea of a group? That is, are all algebraic structures definable by a magma operation and a single law? Maybe with some size limits, e.g. a single binary and a single unary operation, which need to obey laws with up to 3 variables?
That is not true in this formulation, since the axioms might not relate the two operations. But is it true with some restriction on the axioms, or with a single operation? For example, is any set of magma laws equivalent to (or definable in terms of) a single law?

[Bruno Le Floch]

@Amir Livne Bar-on The Higman-Neumann paper proves that you can go from (group axioms + any number of equations involving multiplication, inverse, identity) to (a single magma equation on division). This only answers your question for varieties of groups rather than more general magma laws.

[Jose Brox]

Jose Brox ha dicho:

with those we further reduce the number of candidates to 390.

I got the number down to 318, with the following countermodels:

models = [
   [
        [ 1, 2, 0],
        [ 0, 1, 2],
        [ 2, 0, 1]
    ],
    [
          [ 1, 2, 1],
          [ 2, 1, 0],
          [ 1, 0, 1]
    ],
      [
          [ 1, 0, 2],
          [ 0, 2, 1],
          [ 2, 1, 0]
        ],
    [
          [ 1, 0, 0],
          [ 2, 1, 0],
          [ 2, 2, 1]
    ],
           [
          [ 0, 2, 1],
          [ 2, 1, 0],
          [ 1, 0, 2]
        ],
           [
          [ 0, 1, 2, 3],
          [ 1, 2, 3, 0],
          [ 2, 3, 0, 1],
          [ 3, 0, 1, 2]
        ],
           [
          [ 0, 1, 2, 3],
          [ 2, 3, 0, 1],
          [ 3, 2, 1, 0],
          [ 1, 0, 3, 2]
        ],
 [
          [ 1, 0, 3, 4, 2],
          [ 0, 1, 2, 3, 4],
          [ 4, 2, 1, 0, 3],
          [ 2, 3, 4, 1, 0],
          [ 3, 4, 0, 2, 1]
    ],
           [
          [ 0, 2, 1, 4, 3],
          [ 4, 1, 3, 2, 0],
          [ 3, 4, 2, 0, 1],
          [ 1, 0, 4, 3, 2],
          [ 2, 3, 0, 1, 4]
        ],
    [[0,3,4,1,2,6,5],
     [1,0,5,3,6,4,2],
     [2,6,0,5,4,1,3],
     [3,1,6,0,5,2,4],
     [4,5,2,6,0,3,1],
     [5,2,3,4,1,0,6],
     [6,4,1,2,3,5,0]]]

Moreover, 42302852, 42302946 and 42323122 are equivalent to the HN axiom (42323216) and have smaller id in our classification. They are
$x = y * ((((x * x) * x) * z) * (((x * x) * y) * z)).$
$x = y * ((((x * x) * x) * z) * (((y * y) * y) * z)).$
$x = y * ((((y * y) * x) * z) * (((x * x) * y) * z)).$
Compare with
$x = y*((((y*y)*x)*z)*(((y*y)*y)*z)) \,\, (HN).$

44390496 is proving difficult to crack. It does not have countermodels of size 7 and Mace4 can lag a lot on it depending on the order options (I'm using it as a benchmark). The search continues for sizes 8 and 9. I have to leave now, will come to this when I can.

[Bruno Le Floch]

Jose Brox said:

I got the number down to 318, with the following countermodels: […]

That was helpful, and strong motivation to push further. I'm down to 253 candidate axioms, by filtering on some more linear models, and on a few more models that Mace4 found. My usage of prover9 is pretty bad it seems, as it was only able to prove the (A) and (B) conditions starting from a handful of these candidate axioms. I will try next to prove only (A) or only (B). The code is in Higman_Neumann.py

List of 253 equation ids that might be equivalent to the Higman-Neumann axiom

[42302852, 42302946, 42303162, 42323122, 42323216, 42323432, 42358580, 42358644,
 42358811, 42358978, 42359145, 42359357, 44390496, 44390541, 44410745, 44410811,
 44445959, 44446330, 44446361, 44446423, 44446458, 48217520, 48217671, 48217845,
 48272890, 48273390, 48273536, 48273682, 48273989, 58075358, 58075659, 58095440,
 58095929, 58130160, 58130179, 58130628, 58131718, 58131745, 58131773, 67953597,
 67953691, 67953907, 67956933, 67957244, 67957681, 67957848, 67958015, 67958182,
 67958395, 68185620, 68185686, 68189029, 68189095, 68189903, 68189965, 68189996,
 68190031, 68653446, 68653573, 68653719, 68653865, 68654183, 69576965, 69577454,
 69580266, 69581164, 69581778, 69581832, 69581861, 70970200, 70973958, 70978107,
 70978190, 71546005, 71546685, 71546843, 71552063, 71553983, 71557731, 71558182,
 73151920, 73155857, 73162290, 73162309, 73169078, 73169229, 73169267, 73173015,
 73173204, 73179688, 73180065, 73180415, 73180442, 73180499, 73186121, 73198517,
 73210913, 73231927, 73231955, 73285871, 73287395, 73288447, 73290663, 73292531,
 73294472, 73298835, 73299635, 73300470, 75587462, 75597898, 75597985, 75621653,
 75646445, 75667496, 75667651, 89176740, 89177565, 89178865, 89180041, 89182328,
 89184615, 89188156, 89188210, 89188239, 90206751, 90209038, 90214894, 90252914,
 90255235, 90263396, 90265736, 90271271, 90276806, 90290863, 102398486,
 102401505, 102401815, 102402260, 102402594, 102402761, 102402975, 102743259,
 102744082, 102745815, 102747350, 102749116, 102751108, 102755257, 102755340,
 105877422, 105877516, 105877732, 105880758, 105881069, 105881506, 105881673,
 105881840, 105882007, 105882220, 110519688, 110519755, 110520065, 110520442,
 110520510, 110520844, 110521225, 113067945, 113068011, 113071354, 113071420,
 113072228, 113072290, 113072321, 113072356, 121882187, 121884950, 121884995,
 121885893, 121886499, 121886561, 121886596, 122348850, 122348895, 122350821,
 122350887, 122354997, 122355028, 122355125, 122693826, 122696042, 122697948,
 122699868, 122704164, 122704989, 122705861, 125133271, 125133544, 125133690,
 125134008, 126402180, 126402860, 126403018, 126408064, 126408238, 126410158,
 126413906, 126414357, 129416953, 129417104, 129417142, 129420890, 129421079,
 129427563, 129427940, 129428290, 129428317, 129428374, 147976057, 147976245,
 147976527, 147979351, 147979800, 147980249, 147980899, 147980911, 147980917,
 149944520, 149944702, 149948457, 149948639, 149955111, 149955500, 149955907,
 149955913, 149955925, 157254065, 157254554, 157257328, 157257366, 157258264,
 157258878, 157258932, 157258961, 163862346, 163863479, 163863870, 163864922,
 163867138, 163869006, 163870947, 163875310, 163876110, 163876945]

Speculation: I wouldn't be shocked if among those there are Austin pairs (so no finite model falsifying the equivalence). If an equation has the form x = y * (...) then all left multiplications are surjective. For finite magmas this implies that left multiplication is injective, so that there is "no loss of information". If the equation includes at some point (... * (u * u)) with u appearing nowhere else, then it may be possible to deduce that all u*u are equal (depending on the structure of the equation), which helps simplify the rest of the equation and get group axioms. But, if that is the way to prove constant squares, then squares might not be constant in infinite magmas obeying that equation.

[Jose Brox]

Bruno Le Floch ha dicho:

My usage of prover9 is pretty bad it seems, as it was only able to prove the (A) and (B) conditions starting from a handful of these candidate axioms.

Perhaps it is just that the implication is difficult... As tends to be for example with Austin pairs, as you mention. I suppose that candidates with 3 variables are more difficult to classify than those with more variables. Can you give the list of candidates you were able to prove?

For example, 42302852, 42302946, 42303162, 42323122 are easy, but 44390496 is not: I have tried Prover9 and Mace4 for HN, (A), (B), and $xx = yy$, and also Vampire and Vampire-SAT as allowed by TPTP.org, and they didn't get any conclusion (well, Mace4 is still running on sizes 8 and 9).

[Jose Brox]

Bruno Le Floch ha dicho:

My usage of prover9

For your code, take into account that showing that the identity implies (A),(B) is not enough, we must also show that (A),(B) imply the identity, otherwise it might characterize right division not for all groups, but for some subvariety of groups (e.g., it may be equivalent to Tarski's axiom, characterizing right division for abelian groups).

For Mace4 in this problem, I recommend to use the options selection_order 2, selection_measure 1, and to activate the skolems_last parameter.

[Bruno Le Floch]

The reverse implication is already checked elsewhere in the code when filtering which equations to consider in the first place.
Jose Brox said:

Can you give the list of candidates you were able to prove?

Turns out I had taken a stupid shortcut: I was looking for the string Exiting with 1 proof. in the output, but since there are two things being proven, prover9 was outputting Exiting with 2 proofs. instead. Now that I've switched to using exit codes as I should have done in the first place, my code tells me 173 candidates are equivalent to the Higman-Neumann axioms, and 80 remain unknown:

Good and unknown candidate axioms

EQUIVALENT_TO_GROUP = [42302852, 42302946, 42303162, 42323122,
 42323216, 42323432, 42358580, 42358644, 42358811, 42358978, 42359145,
 42359357, 44390541, 44410811, 44445959, 44446330, 44446361, 44446423,
 44446458, 48217845, 48272890, 48273536, 48273682, 48273989, 58075659,
 58095929, 58130179, 58130628, 58131718, 58131745, 58131773, 67953907,
 67957244, 67957681, 67957848, 67958015, 67958182, 67958395, 68189095,
 68189903, 68189965, 68189996, 68190031, 68653446, 68653573, 68653719,
 68653865, 68654183, 69577454, 69580266, 69581164, 69581778, 69581832,
 69581861, 70970200, 70973958, 70978107, 70978190, 71558182, 73169267,
 73173204, 73179688, 73180065, 73180415, 73180442, 73180499, 73186121,
 73198517, 73210913, 73231927, 73231955, 73287395, 73294472, 73298835,
 73299635, 73300470, 75621653, 75646445, 75667496, 75667651, 89176740,
 89178865, 89180041, 89182328, 89184615, 89188156, 89188210, 89188239,
 90252914, 90263396, 90271271, 90276806, 90290863, 102398486, 102401815,
 102402260, 102402594, 102402761, 102402975, 102747350, 102751108, 102755257,
 102755340, 105877516, 105877732, 105881069, 105881673, 105881840, 105882007,
 105882220, 110519688, 110520065, 110520442, 110520510, 110520844, 110521225,
 113068011, 113071420, 113072228, 113072290, 113072321, 113072356, 121882187,
 121884995, 121885893, 121886499, 121886561, 121886596, 122350887, 122355028,
 122355125, 122696042, 122699868, 122704164, 122704989, 122705861, 125133271,
 125133544, 125133690, 125134008, 126410158, 126413906, 126414357, 129417142,
 129421079, 129427940, 129428317, 129428374, 147976245, 147976527, 147979351,
 147979800, 147980249, 147980899, 147980911, 147980917, 149944702, 149948457,
 149948639, 149955111, 149955500, 149955907, 149955913, 149955925, 157254554,
 157257366, 157258264, 157258961, 163867138, 163869006, 163870947, 163875310,
 163876945]
UNKNOWN_STATUS = [44390496, 44410745, 48217520, 48217671, 48273390,
 58075358, 58095440, 58130160, 67953597, 67953691, 67956933, 68185620,
 68185686, 68189029, 69576965, 71546005, 71546685, 71546843, 71552063,
 71553983, 71557731, 73151920, 73155857, 73162290, 73162309, 73169078,
 73169229, 73173015, 73285871, 73288447, 73290663, 73292531, 75587462,
 75597898, 75597985, 89177565, 90206751, 90209038, 90214894, 90255235,
 90265736, 102401505, 102743259, 102744082, 102745815, 102749116, 105877422,
 105880758, 105881506, 110519755, 113067945, 113071354, 121884950, 122348850,
 122348895, 122350821, 122354997, 122693826, 122697948, 126402180, 126402860,
 126403018, 126408064, 126408238, 129416953, 129417104, 129420890, 129427563,
 129428290, 147976057, 149944520, 157254065, 157257328, 157258878, 157258932,
 163862346, 163863479, 163863870, 163864922, 163876110]

EDIT: Running prover9 for longer gives that 68185686, 73290663, 105881506 are also Group.

[Bruno Le Floch]

I focused on Equation 67953691: x = (y ◇ y) ◇ (y ◇ ((x ◇ z) ◇ (((y ◇ y) ◇ y) ◇ z))) because it is the first to have a single x on the RHS, among the 80 unknown equations. Assuming the magma is finite, I can show that that axiom is equivalent to Group division.

Write the equation more compactly as x = Sy ◇ (y ◇ ((x◇z) ◇ (Cy◇z))) where Sx=x◇x and Cx=(x◇x)◇x are the square and cube operations. Since x only appears once, the equation can also be written as $L_{Sy} \circ L_y \circ R_{Cy*z} \circ R_z = \text{id}$. Thus all $R_z$ are injective and all $L_{Sy}$ are surjective.

For a finite magma, this is stronger: composing functions can only give the identity if all functions are bijections, so both left and right multiplication are bijective. Taking x = Cy = Sy ◇ y and cancelling the Sy ◇ on both sides of the equation gives y = y ◇ S(Cy ◇ z). Here, Cy ◇ z can be anything, so y=y◇Sw for all y,w. We conclude here that all squares are right identities. By injectivity of $R_y$, actually, all squares are equal: $Sy = e$ for some right identity e. Evaluating the main equation for y=z=e gives x = e ◇ (e ◇ x), which gives property (B).

At this stage, the main equation reads x = e ◇ (y ◇ ((x ◇ z) ◇ ((e◇y) ◇ z))). Bijectivity of $L_e$ and $L_y$ tells us that (x ◇ z) ◇ ((e◇y) ◇ z) is z-independent. Replacing y by e◇y one learns that (x◇z)◇(y◇z) is z-independent. By taking z=y we get its value x◇y and we are done.

Trying similar techniques for equation 44390496 I got stuck. I wonder how we could impose finiteness ("injectivity equivalent to surjectivity") in prover9, to analyse the finite cases for all 80 equations.

[Vlad Tsyrklevich]

I've got some thoughts on finding finite implications. This is a good opportunity to share what I've been working on and get some feedback, but my local tooling has diverged from what's upstream. I will clean it up a bit before sharing it and seeing if it's useful to you.

[Vlad Tsyrklevich]

I'm a bit lost in the backscroll, can you clarify what implications you're looking for specifically? Is it from UNKNOWN_STATUS to each other, or to 42323216, or something else? I suspect it's bi-implication to 42323216, yes?

[Vlad Tsyrklevich]

As far as finite implications to 42323216, [67953597, 67953691, 68185686, 71553983, 71557731, 73173015, 73290663, 89177565, 90265736, 129416953, 129420890, 129427563, 129428290, 157258878, 157258932, 163863870, 163876110] appear to form a finite equivalence class and imply 42323216.
HigmanNeumann1.lean

[Vlad Tsyrklevich]

Also, I'll just note that switching left/right inverses of 42323216 yields 67953691, 105877516, 147976245. My script currently only searches for inverses of the source of the implication to the target. Searching for implications to the inverses of 42323216 as well, I was also able to find the additional implication 48273390 => 147976245 => 42323216
HigmanNeumann2.lean

[Vlad Tsyrklevich]

The above is not an exhaustive list, this is just what I proved using the inverses method. Using bijections I am also able to establish some other implications, but before continuing further I'll wait to get feedback on what exactly you're looking for.

[Bruno Le Floch]

Thanks a lot. I have real life to attend for a few days before I can learn and read the lean code. All of the equations in consideration are implied by 42323216 (which is equivalent to Equation 3737: x ◇ y = (x ◇ z) ◇ (y ◇ z) and Equation 1718: x = (y ◇ y) ◇ ((x ◇ x) ◇ x) together). So the only question is which of these (which of the UNKNOWN_STATUS) imply 42323216. In particular your equivalence class [67953597, ...] is actually finite-equivalent to 42323216.

Can you clarify what you mean by "switching left/right inverses"?

[Jose Brox]

Bruno Le Floch ha dicho:

how we could impose finiteness ("injectivity equivalent to surjectivity") in prover9, to analyse the finite cases for all 80 equations.

I guess we can use
all y all z f(y) = f(z) -> y = z <-> all v exists w (f(w) = v)
where $f$ is the function in question. For example, for left multiplication,
all x all y all z (x*y = x*z -> y=z) <-> all u all v exists w (u*w = v).

(I have some ideas too for this, but also real life to attend in the weekend... One thing, by a result of Furstenberg we can take the axioms to be Identity (A) and surjectivity of left multiplication).

[Vlad Tsyrklevich]

Bruno Le Floch said:

Can you clarify what you mean by "switching left/right inverses"?

If $x=f(g(x))$ then it is equivalent to $x=g(f(x))$ in finite domains, e.g. $g$ being a right inverse of $f$ means it is also a left inverse.

For example, for 42323216 $x = y ◇ ((((y ◇ y) ◇ x) ◇ z) ◇ (((y ◇ y) ◇ y) ◇ z))$ it is also expressible as $x=f(g(x))$ with $f(x)=y ◇ (x ◇ (((y ◇ y) ◇ y) ◇ z))$ and $g(x)=((y ◇ y) ◇ x) ◇ z$, so inverted $x=g(f(x))$ is 147976245: $x = ((y ◇ y) ◇ (y ◇ (x ◇ (((y ◇ y) ◇ y) ◇ z)))) ◇ z$. A different choice of $f$ and $g$ gives you the other inverses I mentioned.

[Vlad Tsyrklevich]

Jose Brox said:

I guess we can use
(f(y) = f(z) -> y = z) <-> (exists w (f(w) = v))
where $f$ is the function in question. For example, for left multiplication,
(x*y = x*z -> y=z) <-> (exists w (u*w = v)).

(I have some ideas too for this, but also real life to attend in the weekend... One thing, by a result of Furstenberg we can take the axioms to be Identity (A) and surjectivity of left multiplication).

Yes I've found that by bruteforcing in order <= 4, the following equivalent TPTP statements were enough to get everything I could find:

fof(eq3_inj_surj, axiom, ![A] : ?[B] : ( A = mul(B, B) ) <=> ![X,Y] : ( (mul(X, X) = mul(Y, Y) ) => X=Y) ).
fof(eq4_inj_surj, axiom, ![A,M1] : ?[B] : ( A = mul(B, M1) ) <=> ![X,Y,M1] : ( (mul(X, M1) = mul(Y, M1) ) => X=Y) ).
fof(eq5_inj_surj, axiom, ![A,M1] : ?[B] : ( A = mul(M1, B) ) <=> ![X,Y,M1] : ( (mul(M1, X) = mul(M1, Y) ) => X=Y) ).
fof(eq8_inj_surj, axiom, ![A] : ?[B] : ( A = mul(B, mul(B, B)) ) <=> ![X,Y] : ( (mul(X, mul(X, X)) = mul(Y, mul(Y, Y)) ) => X=Y) ).
fof(eq11_inj_surj, axiom, ![A,M1] : ?[B] : ( A = mul(B, mul(M1, M1)) ) <=> ![X,Y,M1] : ( (mul(X, mul(M1, M1)) = mul(Y, mul(M1, M1)) ) => X=Y) ).
fof(eq23_inj_surj, axiom, ![X] : ?[T] : ( X = mul(mul(T, T), T) ) <=> ![T1,T2] : ( (mul(mul(T1, T1), T1) = mul(mul(T2, T2), T2) ) => T1 = T2 )).
fof(eq31_inj_surj, axiom, ![X,Y] : ?[T] : ( X = mul(mul(Y, Y), T) ) <=> ![T1,T2,Y] : ( (mul(mul(Y, Y), T1) = mul(mul(Y, Y), T2) ) => T1 = T2 )).

However, for order 5 and for some of the equations I tested above, some new bijective relations are also required. My script is also able to do some bruteforcing of relationships like the above, and this is part of what I need to clean-up. There are some buggy edge cases that I know about that would be good to sand away for consumption by others.

I think it would be interesting to try to teach a higher-order theorem prover these rules and see if they explode under the combinational explosion or not, but I've been too busy with other tasks to really attempt this.

[Vlad Tsyrklevich]

Bruno Le Floch said:

learn and read the lean code

Also, just a quick note that it's mostly just auto-generated output--I'm not sure how much meaning you'll derive from reading it. I shared it because I generated the proofs to double check my work, and I figured it'd be nice to share the artifact just in case anyone else might want to look.

[Terence Tao]

[deleted]

[Jose Brox]

[EDITED TO INCLUDE THE CORRECT QUANTIFICATION OF VARIABLES]
Vlad Tsyrklevich ha dicho:

Yes I've found that by bruteforcing in order <= 4, the following equivalent TPTP statements were enough to get everything I could find:

@Bruno Le Floch Translated to Prover9 syntax those are:

all x exists y ( x = y*y ) <-> all z all w ((z*z = w*w) -> z = w).
all x all z exists y ( x = y*z ) <-> all u all v all w ((v*u = w*u) -> v = w).
all x all z exists y ( x = z*y ) <-> all u all v all w  ((u*v = u*w) -> v = w).
all x exists y ( x = y*(y*y) ) <-> all u all v ((u*(u*u) = v*(v*v)) -> u = v).
all x all z exists y ( x = y*(z*z) ) <-> all u all v all w ((v*(u*u) = w*(u*u)) -> v = w).
all x exists y ( x = (y*y)*y ) <-> all u all v ((u*u)*u = ((v*v)*v) -> u = v).
all x all z exists y ( x = (z*z)*y ) <-> all u all v all w (((u*u)*v = (u*u)*w) -> v = w).

[Terence Tao]

An inconclusive report on an attempt to resolve  Equation 67953691: x = (y ◇ y) ◇ (y ◇ ((x ◇ z) ◇ (((y ◇ y) ◇ y) ◇ z))). I believe that the following recursive construction on the carrier ${\mathbb Z}^+$ gives a counterexample to the claim that this law must come from division on a magma: $x \diamond y = z$ iff $(x,y,z)$ is a triple of one of the following forms:

1. $(a,a,2^a)$ (so $Sa = 2^a$)
2. $(2^a,a,3^a)$ (so $Ca = 3^a$)
3. $(2^b, 5^a 7^b 11^c 13^d, a)$ with $d=2,3$ (so $L_{Sb} (5^a 7^b 11^c 13^d) = a$)
4. $(b, 5^a 7^b 11^c 13^1, 5^a 7^b 11^c 13^2)$ (so $L_{Sb} L_b (5^a 7^b 11^c 13^1) = a$)
5. $(a \diamond c, 3^b \diamond c, 5^a 7^b 11^c 13^1)$ with $a \neq 3^b$ (so $L_{Sb} L_b ((a \diamond c) \diamond (Cb \diamond c)) = a$ when $a \neq Cb$)
6. $(a, 2^{3^a \diamond b}, 5^{3^a} 7^a 11^b 13^3)$ (so $L_{Sb} L_b ((a \diamond c) \diamond (Cb \diamond c)) = a$ when $a = Cb$)
7. $(a,b, 17^a 19^b)$ if $a \diamond b$ is not already defined by the above rules.

If one can find a magma operation that obeys all these rules then it obeys 67953691 without being a group ($a \diamond a= 2^a$ is not constant). However, to actually show that such an operation exists (and I think it is even unique) is a horribly recursive case check that I was not able to close in a civilized amount of time, although I believe it can be done eventually. The problem is primarily with rules 5 and 6, which require some prior knowledge about $\diamond$ in order to define new values of $\diamond$. On the other hand, I believe every positive integer has at most one representation of the form $3^b \diamond c$, and for fixed $c$, every positive integer has at most one representation of the form $a \diamond c$, so that Rule 5 at least (and, separately, Rule 6) is well-defined; but proving that Rule 5 does not collide with the other rules is highly tedious (with Rule 3 causing the biggest problems, either directly or indirectly, due to its ability to produce arbitrary outputs).

In analogy with other equations such as 1518, most likely the better way to proceed here is to impose as many simplifying additional axioms as possible to split up the law into smaller pieces, without accidentally implying axioms (A) and (B): e.g., making $S$ constant, $C$ constant, identity, or invertible, etc..

[Vlad Tsyrklevich]

Just getting back to a run I started yesterday morning: Using bijections , [105877422, 105881506, 48273390, 73288447, 73292531, 90206751, 90209038, 90214894] => 42323216. Some of these required additional rules in addition to what I posted above, e.g. ![X,Y,Z] : ?[XT] : ( X = mul(mul(XT, Y), Z) ) <=> ![XT1,XT2,Y,Z] : ( (mul(mul(XT1, Y), Z) = mul(mul(XT2, Y), Z) ) => XT1 = XT2 ) for 73288447. Unfortunately, I can't post-process the Vampire output into Lean proofs for these results, so these are results are of a lower sureness.

[Vlad Tsyrklevich]

Also, I can't test all possible bijections of functions, so this result is necessarily incomplete, but I did test, individually, all combinations up to 4 terms on the RHS.

[Vlad Tsyrklevich]

Personal life also got in the way of me finishing updates to my tooling, hopefully that'll be ready in a day or two.

[Bruno Le Floch]

@Vlad Tsyrklevich If I understand correctly the code ![X,Y,X] etc in your message states that if $R_Z\circ R_Y$ is surjective then it is injective. It can be split into two results, maybe easier to work with: if $R_Z\circ R_Y$ is surjective then $R_Z$ and $R_Y$ are surjective, and separately if these are surjective then they are injective. (The fact that composing injectives gives an injective does not depend on finiteness.)

[Jose Brox]

Terence Tao ha dicho:

most likely the better way to proceed here is to impose as many simplifying additional axioms as possible to split up the law into smaller pieces, without accidentally implying axioms (A) and (B): e.g., making S constant, C constant, identity, or invertible, etc..

I have checked with Prover9 that we cannot impose S nor C nor $x*(x*x)$ constant, nor left nor right identity element, nor $x*x = y*y$. What do you mean exactly by invertible? Invertibility of right multiplication, which is already injective? (That may be possible, Prover9 gives an error, so doesn't generate a proof).

[Bruno Le Floch]

I think he meant x↦Sx invertible, or x↦Cx invertible. For instance this (or even just x↦Cx surjective) can be helpful I suppose when the equation contains x only as Cx on the RHS. There are a few.

[Vlad Tsyrklevich]

Bruno Le Floch said:

If I understand correctly the code

In TPTP ! is $\forall$ and ? is $\exists$

Bruno Le Floch said:

It can be split into two results, maybe easier to work with

This is a good idea, I've saved to play with it. This may simplify my search a bit.

[Jose Brox]

Bruno Le Floch ha dicho:

I think he meant x↦Sx invertible, or x↦Cx invertible.

Yep, I see it now (sorry, my brain is fried most of the time... I have my 17 months old kid with me for a lot of waking hours and we are sick most of the time :grinning_face_with_smiling_eyes: He has even written some of my messages here! :stuck_out_tongue_closed_eyes: ).

Running Prover9 with the hard candidates is changelling (I'm learning quite a bit!). I have to tinker the search space parameters carefully, because if they are low the search is exhausted in a few seconds, but if they go higher then suddenly Prover9 crashes with a "too many variables" error (possibly a bug, since I put no variable limit and give it plenty of memory). My feeling is that in those cases there is no implication.

Anyway, @Terence Tao for 67953691, squaring or cubing being the identity map implies HN. On the other hand, I have managed to run a big search for 1h without finding a proof for cubing being invertible. Also checked with Vampire in TPTP.org (but there I cannot tweak parameters).

[Jose Brox]

More filtering on the list of candidates:

@Bruno Le Floch applied linear models up to size 5 in his script (which I'm heavily using!). Since there was room for improvement there, I am filtering with larger models, and we can eliminate a bunch of candidates:

Size 6-10: [58130160, 67956933, 68189029, 75597898]
Size 11-20:
[69576965, 90255235, 102401505, 110519755, 126402860, 129417104, 147976057, 163862346, 163864922]
Size 21-30: [44410745, 149944520]
Size 31-40: None
Size 41-50: [44390496, 105880758]
17 candidates less in total!
Now I'm running sizes 51-60 (can be 1h or so) and will keep going up until I see some serious stabilization.

Also, filtering with more time in Prover9, three other candidates have turned out to be equivalent to the HN axiom as computed by Bruno (and double checked by me):
[68185686, 73290663, 105881506]

All in all, this leaves us with 60 candidates! Of those, 15 are equivalent to HN at least in the finite setting as @Vlad Tsyrklevich showed, so cannot be eliminated by finite linear models.

The list of unknown candidates at the moment:

[48217520, 48217671, 48273390, 58075358, 58095440, 67953597, 67953691, 68185620, 71546005, 71546685, 71546843, 71552063, 71553983, 71557731, 73151920, 73155857, 73162290, 73162309, 73169078, 73169229, 73173015, 73285871, 73288447, 73292531, 75587462, 75597985, 89177565, 90206751, 90209038, 90214894, 90265736, 102743259, 102744082, 102745815, 102749116, 105877422, 113067945, 113071354, 121884950, 122348850, 122348895, 122350821, 122354997, 122693826, 122697948, 126402180, 126403018, 126408064, 126408238, 129416953, 129420890, 129427563, 129428290, 157254065, 157257328, 157258878, 157258932, 163863479, 163863870, 163876110]

And the list of finitely equivalent not known to be always equivalent:

[67953597, 67953691, 71553983, 71557731, 73173015, 89177565, 90265736, 129416953, 129420890, 129427563, 129428290, 157258878, 157258932, 163863870, 163876110]

[Vlad Tsyrklevich]

I think there should be 22 entries in the finite list by my count. It's missing 48273390 (last one by inverse) and the bijective entries

[Jose Brox]

@Vlad Tsyrklevich Some of them are always equivalent to HN!

[Vlad Tsyrklevich]

48273390 for example is in the unknowns list, unless I'm misinterpreting something. The others are [73288447, 73292531, 90206751, 90209038, 90214894, 105877422]

[Bruno Le Floch]

I think if I pool together the infinite-magma results, the counterexamples mentioned by Jose, and the finite implications found by Vlad, I get

• Characterize groups: 177 entries

[42302852, 42302946, 42303162, 42323122, 42323216, 42323432, 42358580, 42358644, 42358811, 42358978, 42359145, 42359357, 44390541, 44410811, 44445959, 44446330, 44446361, 44446423, 44446458, 48217845, 48272890, 48273536, 48273682, 48273989, 58075659, 58095929, 58130179, 58130628, 58131718, 58131745, 58131773, 67953907, 67957244, 67957681, 67957848, 67958015, 67958182, 67958395, 68185686, 68189095, 68189903, 68189965, 68189996, 68190031, 68653446, 68653573, 68653719, 68653865, 68654183, 69577454, 69580266, 69581164, 69581778, 69581832, 69581861, 70970200, 70973958, 70978107, 70978190, 71558182, 73169267, 73173204, 73179688, 73180065, 73180415, 73180442, 73180499, 73186121, 73198517, 73210913, 73231927, 73231955, 73287395, 73290663, 73294472, 73298835, 73299635, 73300470, 75621653, 75646445, 75667496, 75667651, 89176740, 89178865, 89180041, 89182328, 89184615, 89188156, 89188210, 89188239, 90252914, 90263396, 90271271, 90276806, 90290863, 102398486, 102401815, 102402260, 102402594, 102402761, 102402975, 102747350, 102751108, 102755257, 102755340, 105877516, 105877732, 105881069, 105881506, 105881673, 105881840, 105882007, 105882220, 110519688, 110520065, 110520442, 110520510, 110520844, 110521225, 113068011, 113071420, 113072228, 113072290, 113072321, 113072356, 121882187, 121884995, 121885893, 121886499, 121886561, 121886596, 122350887, 122355028, 122355125, 122696042, 122699868, 122704164, 122704989, 122705861, 125133271, 125133544, 125133690, 125134008, 126410158, 126413906, 126414357, 129417142, 129421079, 129427940, 129428317, 129428374, 147976245, 147976527, 147979351, 147979800, 147980249, 147980899, 147980911, 147980917, 149944702, 149948457, 149948639, 149955111, 149955500, 149955907, 149955913, 149955925, 157254554, 157257366, 157258264, 157258961, 163863870, 163867138, 163869006, 163870947, 163875310, 163876945]

• Characterize groups on finite magmas, unknown in general: 21 entries

[48273390, 67953597, 67953691, 71553983, 71557731, 73173015, 73288447, 73292531, 89177565, 90206751, 90209038, 90214894, 90265736, 105877422, 129416953, 129420890, 129427563, 129428290, 157258878, 157258932, 163876110]

• Unknown even in the finite setting: 22 entries

[48217520, 48217671, 58075358, 58095440, 73151920, 73155857, 73162290, 73162309, 73169078, 73169229, 73285871, 102743259, 102744082, 102745815, 102749116, 113067945, 113071354, 121884950, 122693826, 122697948, 157254065, 157257328]

It might be useful to get a better understanding of what the linear counterexamples do, or maybe to write by hand what would be the conditions for a linear model to obey one of the remaining unknowns in the list.

EDIT: Removed 10 equations from the unknown list by finding magmas that obey them but are not group-division: [68185620, 122348850] via large linear models, and [71546005, 71546685, 71546843, 122350821, 122354997, 126408064, 126408238, 163863479] via a 10-element magma obtained from a linear model on $(\mathbb{F}_3)^2$ by changing squares to a new unit element. Jose found a 16-element magma (octonion basis and their additive inverses, equipped with division) that eliminates [71552063, 75587462, 75597985, 122348895, 126402180, 126403018]. Moved one equation 163863870 from possibly Austin to equivalent to group division thanks to a long prover9 run by Jose.

[Jose Brox]

Vlad Tsyrklevich ha dicho:

48273390 for example is in the unknowns list, unless I'm misinterpreting something.

Ah yes, I incorrectly used an incomplete and redundant list. Thank you! 38 to go (potentially) with finite models.

[Jose Brox]

Bruno Le Floch ha dicho:

It might be useful to get a better understanding of what the linear counterexamples do, or maybe to write by hand what would be the conditions for a linear model to obey one of the remaining unknowns in the list.

Good point. For starters I have written a script in SAGE and checked that all remaining candidates unknown even in the finite setting have the "trivial" variety over $\bar{Q}$, i.e., their only linear model is $x*y=x-y$.
HIGMAN-NEUMANN - Linear models.ipynb
HIGMAN-NEUMANN - Linear models.py
From the script one can extract the polynomial system of each candidate to study it over other commutative rings.
The noncommutative case is harder to check.

[Jose Brox]

(deleted)

[Bruno Le Floch]

Using ad-hoc Mathematica code I find two more linear counterexamples (meaning these equations cannot imply Group). It is not over $\bar{\mathbb{Q}}$ but over $\mathbb{Z}/N\mathbb{Z}$ for some large $N$. But the other 36 unknown equations are indeed immune against commutative linear models. I am not planning to look into packages for noncommutative Grobner bases, which seems necessary to test non-commutative linear models.

• 68185620 by $x\diamond y=261x+33y\bmod{307}$,
• 122348850 by $x\diamond y = 31x+79y\bmod{103}$.

[Jose Brox]

Reporting new results from the morning:

1) @Bruno Le Floch has used the Steiner system $S(2,3,9)$ as countermodel of size 10 ($x*y:=-(x+y)$ if $x\neq y$ in $F_3^2$ with an added unit $0$ so that $x*x:=0$) and has eliminated the 8 candidates
[71546005, 71546685, 71546843, 122350821, 122354997, 126408064, 126408238, 163863479].
The model is

[[0, 1, 2, 3, 4, 5, 6, 7, 8, 9],
  [1, 0, 3, 2, 7, 9, 8, 4, 6, 5],
  [2, 3, 0, 1, 8, 7, 9, 5, 4, 6],
  [3, 2, 1, 0, 9, 8, 7, 6, 5, 4],
  [4, 7, 8, 9, 0, 6, 5, 1, 2, 3],
  [5, 9, 7, 8, 6, 0, 4, 2, 3, 1],
  [6, 8, 9, 7, 5, 4, 0, 3, 1, 2],
  [7, 4, 5, 6, 1, 2, 3, 0, 9, 8],
  [8, 6, 4, 5, 2, 3, 1, 9, 0, 7],
  [9, 5, 6, 4, 3, 1, 2, 8, 7, 0]]

2) I have used the octonion basis plus its additive inverses with product $x*y:=xy^{-1}$ as a countermodel of size 16 and further eliminated the 7 candidates
[71552063, 75587462, 75597985, 122348850, 122348895, 126402180, 126403018].
The model is

[[0, 9, 10, 11, 12, 13, 14, 15, 8, 1, 2, 3, 4, 5, 6, 7],
 [1, 0, 3, 10, 5, 12, 15, 6, 9, 8, 11, 2, 13, 4, 7, 14],
 [2, 11, 0, 1, 6, 7, 12, 13, 10, 3, 8, 9, 14, 15, 4, 5],
 [3, 2, 9, 0, 7, 14, 5, 12, 11, 10, 1, 8, 15, 6, 13, 4],
 [4, 13, 14, 15, 0, 1, 2, 3, 12, 5, 6, 7, 8, 9, 10, 11],
 [5, 4, 15, 6, 9, 0, 11, 2, 13, 12, 7, 14, 1, 8, 3, 10],
 [6, 7, 4, 13, 10, 3, 0, 9, 14, 15, 12, 5, 2, 11, 8, 1],
 [7, 14, 5, 4, 11, 10, 1, 0, 15, 6, 13, 12, 3, 2, 9, 8],
 [8, 1, 2, 3, 4, 5, 6, 7, 0, 9, 10, 11, 12, 13, 14, 15],
 [9, 8, 11, 2, 13, 4, 7, 14, 1, 0, 3, 10, 5, 12, 15, 6],
 [10, 3, 8, 9, 14, 15, 4, 5, 2, 11, 0, 1, 6, 7, 12, 13],
 [11, 10, 1, 8, 15, 6, 13, 4, 3, 2, 9, 0, 7, 14, 5, 12],
 [12, 5, 6, 7, 8, 9, 10, 11, 4, 13, 14, 15, 0, 1, 2, 3],
 [13, 12, 7, 14, 1, 8, 3, 10, 5, 4, 15, 6, 9, 0, 11, 2],
 [14, 15, 12, 5, 2, 11, 8, 1, 6, 7, 4, 13, 10, 3, 0, 9],
 [15, 6, 13, 12, 3, 2, 9, 8, 7, 14, 5, 4, 11, 10, 1, 0]]

3) The last 2 days I have been running Prover9 for 30min with high max_weight and sos_limit over the unknown candidates. I have found that one of them is actually equivalent to the HN axiom! It is
[163863870].
In retrospective, a quicker proof can be found with Prover9 in 23s by using max_weight 150 and sos_limit 200.

All in all, now we have 21 possible Austin pairs, and 22 candidates unknown even in the finite setting. :working_on_it:

[Alex Meiburg]

I haven't got the fortitude to read through and follow quite all of the work here -- am I correct that all these putative laws expected to be _equivalent_ to the Higman-Neumann law (or not characterizing groups)? Or is it possible that they're characterizing groups, but not equivalent to the Higman-Neumann law, i.e. one of these laws does not necessarily imply the other?

My understanding is that it's former, but I'd just like to check. If it's the latter, then I would want to add these sporadic solutions to the definability graph, because each might lead to some different collapses by letting my define associative laws. But if they're all equivalent to the Higman-Neumann law, then just adding that one law would be sufficient.

[Bruno Le Floch]

We are only studying implication in the sense of the main project, not definability. All equations listed here are implied by Higman-Neumann (we checked that they hold in the underlying group). Some are equivalent, some are only known to be equivalent in the finite case, some are unknown, and some fail to imply Higman-Neumann (typically, we have explicit finite magma counterexamples, often based on nonassociative loop). See my message upthread for the list of 177 that are equivalent, 21 that are equivalent for finite magmas, and 22 that are presently only known to be implied by Higman-Neumann and could end up either way.

[Alex Meiburg]

I see, ok, thanks. That was my understanding.

[Jose Brox]

My daily report:

Since we seem to have already taken the low-hanging fruits amenable to brute-forcing with generic techniques, yesterday I started doing some specific thinking (hence the octonion model).

More in general, I have started looking for quasigroup models for the unknown candidates. Looking with Mace4 I have been able to find two models of size 8 which discard 3 further candidates:
[58075358, 157254065, 157257328]
The first two with the model

[[ 0, 2, 3, 4, 5, 6, 7, 1],
 [ 4, 1, 6, 0, 7, 3, 5, 2],
 [ 5, 3, 2, 7, 0, 1, 4, 6],
 [ 6, 7, 4, 3, 1, 0, 2, 5],
 [ 7, 6, 1, 5, 4, 2, 0, 3],
 [ 1, 4, 7, 2, 6, 5, 3, 0],
 [ 2, 0, 5, 1, 3, 7, 6, 4],
 [ 3, 5, 0, 6, 2, 4, 1, 7]]

The third with the model

[[ 0, 5, 6, 7, 1, 2, 3, 4],
 [ 3, 2, 4, 1, 7, 5, 0, 6],
 [ 4, 7, 3, 5, 2, 1, 6, 0],
 [ 5, 0, 1, 4, 6, 3, 2, 7],
 [ 6, 1, 0, 2, 5, 7, 4, 3],
 [ 7, 4, 2, 0, 3, 6, 1, 5],
 [ 1, 6, 5, 3, 0, 4, 7, 2],
 [ 2, 3, 7, 6, 4, 0, 5, 1]]

I'm also sharing the Mace4 code, since it may be interesting. For quasigroups we need to define 3 binary operations $*$, $/$, \, where $/$ corresponds to right division. Then we need to write the identity we are interested in in terms of $/$ and look it up against the HN axiom written with $/$; if we also add the associative axiom with $*$, the search is sensibly faster. I write here down an example:

if(Mace4).   % Options for Mace4
  assign(max_seconds, -1).
  set(skolems_last).
  assign(max_megs, 2000).
  assign(selection_measure, 1).
  assign(max_seconds, -1).
  assign(max_models, 1).
end_if.

formulas(assumptions).
y = (y / x) * x.
y = (y * x) / x.
y = x * (x \ y).
y = x \ (x * y).
x = y / ((((x / x) / x) / (((y / y) / z) / y)) / z).
end_of_list.

formulas(goals).
x = y/((((y/y)/x)/z)/(((y/y)/y)/z)).
x*(y*z) = (x*y)*z.
end_of_list.

The search for the third model took 1025s. I have made runs for 1800s for the remaining candidates, without success for the moment.

On the other hand, I took the octonion model one step further and wrote the model for the sedenion basis together with its additive inverses, and product $x*y:=xy^{-1}$. I was a bit surprised that it didn't eliminate any candidates, and I'm not completely confident that I got it right (since Sage has no sedenions support, I started with the multiplication table at Wikipedia), but see below. If anyone wants to double check my model, it is in the following file:
sedenions right division.txt

In addition, since the model-for-candidates-them-all in order 6 was the smallest nonassociative inverse loop, I have tried finding nonassociative inverse loops models, without success (see below). For fun I have also determined the smallest of them (there are 3 in size 8, 5 in size 9, 45 in size 10).
For working with nonassociative inverse loops, I made the following code:

formulas(assumptions).
y = (y / x) * x.
y = (y * x) / x.
y = x * (x \ y).
y = x \ (x * y).
(x*0 = x) & (0*x = x) #label(identity_element).
f(x)*(x*y) = y #label(left_inverse).
(x*y)*f(y) = x #label(right_inverse).
f(x) = f(y) -> x = y.
end_of_list.

formulas(goals).
(x*y)*z = x*(y*z).
end_of_list.

The lack of success has made me suspect that the nongroup models of the remaining candidates (those not being equivalent to group) have a strong lack of structure. Therefore I have turned the tables and looked for identity + additional properties being equivalent to HN. I have found:
1) Adding associativity makes all of them equivalent to HN. In fact, it is enough to add alternativity. Many of them already are equivalent with left/right alternativity, flexibility, or power associativity. This affects the sedenion model viability.
2) Adding commutativity makes many of them equivalent to HN.
3) Adding the identity element, only 4 are not proven to be equivalent to HN (but for them, no unital model has been found in 1800s). This affects the viability of the sedenion model and of loops in general.
4) Adding left inverses, only 3 are not proven to be equivalent to HN. Adding symmetric inverses makes them all equivalent. This affects inverse quasigroup models.

I'm looking at more properties, will list them tomorrow together with the actual equivalent candidates.

[Jose Brox]

Jose Brox ha dicho:

Therefore I have turned the tables and looked for identity + additional properties being equivalent to HN.

I made a mistake yesterday while looking for immunities, some $*$ and $/$ operations got mixed up (and then copy-pasted to a lot of properties :sweat_smile: ), with the ending result that the properties were tried on the operation of the identities, not on the main quasigroup operation $*$. Some of those still give interesting information, but I'm redoing the computations correctly now.

[Jose Brox]

I'm also trying to abstract some properties for the "abstract right division" operation from the properties of the supposed "main operation" lying behind "division". For example, I have shown (with Prover9) that a quasigroup is associative (has $*$ associative) if and only if the following two pseudoassociative identities of division are satisfied:
$x/(y/(z/w)) = (x/(w/z))/y$ (ARD)
$((x\setminus y)\setminus z)\setminus w = z\setminus ((y\setminus x)\setminus w)$ (ALD)
Hence, if an equation in operation $◇$ is equivalent to HN, then it must imply (ARD) for $◇$.

[Jose Brox]

You are going to laugh: While looking for countermodels to ARD, I have found that the following 4 candidates are discarded by a model of size 3 :scream: :
[73151920, 73155857, 73162290, 73162309]
(This quartet appeared together before, for example, as the only candidates not being equivalent to HN when a right identity element is added).
The model is just

      [ [ 0, 1, 2],
          [ 1, 0, 0],
          [ 2, 0, 0]]

I have checked and this model is found instantly when looking against HN, so I think it should have been found before. Perhaps some search parameter was different, or I started the search from size 7... I'm running a new search against HN for the rest of candidates, just in case.

[Terence Tao]

One could perhaps repurpose some existing code to brute force the candidates against all small models and randomly chosen linear models. [EDIT: I see the linear models have already been checked, ignore the second suggestion.]

[Terence Tao]

Also, for HN models of prime order, I think any column not coming from a unit determines the whole magma. So one could fill in one column of an order p magma with some shift map and ask an ATP if a given law then forces all the rest of the magma; if not, then this already refutes the equivalence to HN even in the finite setting. (Actually I think this works even for non-prime order, as long as the column is a cyclic permutation.)

[Jose Brox]

(deleted)

[Jose Brox]

Terence Tao ha dicho:

One could perhaps repurpose some existing code to brute force the candidates against all small models

If I understand you correctly, this is what I already do most of the time: @Bruno Le Floch wrote Python code which allows to call Prover9 or Mace4 against a bunch of identities, and I try different implications/antiimplications with sufficient/necessary conditions over all the candidates. That's why I said that the low-hanging fruits should have all been collected (but they weren't! Something went wrong in the process).

This is how Mace4 works: you give it a list of assumed identities A and a list of "goal" identities B, and it exhaustively searches all models, increasing in size, that satisfy all identities in A and none in B, i.e., it looks for models of A that are countermodels to all identities in B.

Then bruteforcing small models is a matter of running Mace4 in a loop with the ongoing candidate in A (perhaps together with more restrictions, as having an underlying quasigroup structure) and HN (or (A), (B), ADR...) in B, or even a redundant combination of them, since this can speed up the search.

The problem with this approach is the time explosion: we either stop Mace4 with a limit in time, memory, model size, or number of models found (for looping only time or very small model size makes sense). The runtime depends strongly on the identities and parameters, but typically size 7 can be exhausted quite easily, and perhaps up to size 9, in a reasonable time (like 30min) and with the right combination of search parameters.

Concrete examples: to conduct a longer search against the remaining candidates, I'm timing two examples:
1) Candidate 48217520 as right division in a quasigroup against HN plus associativity of the * product (redundant). Size 9 was exhausted in 83min; for size 10 has been running for 7 hours already.
2) Same candidate against ADR. Has been running from size 2 for 5h45min and is still exploring size 8.

Against batches of candidates, I usually run Mace4 (or Prover9) for 30min each (well, first I try to sieve the easy ones, then do this for the hard ones).

[Jose Brox]

Jose Brox ha dicho:

I have shown (with Prover9) that a quasigroup is associative (has ∗ associative) if and only if the following two pseudoassociative identities of division are satisfied:
x/(y/(z/w))=(x/(w/z))/y (ARD)
((x∖y)∖z)∖w=z∖((y∖x)∖w) (ALD)
Hence, if an equation in operation ◇ is equivalent to HN, then it must imply (ARD) for ◇.

It turns out that ARD is a quite strong condition for this problem:

1) All remaining candidates are immune to ARD; i.e., those identities together with ARD already imply HN. In particular, no countermodel to HN can be found for them within associative quasigroups. Out of curiosity, I have checked the immunity of the 5450 original candidates of order 8 generated by @Bruno Le Floch , and only 657 (12%) are not easily shown to imply HN together with ARD.

2) On the other hand, most of the original candidates can be discarded by a small countermodel to ARD, only 686 survive against a 5s run with Mace4, and only 657 against a 10s run (are those the same 657 as before? I didn't check yet, but possibly those candidates already imply ARD while not implying HN...).

For comparing the strengh of ARD in this matter, I have also run the original candidates against HN, (A), (B), x^2 = y^2, and having right identity element (always with 5s). The ranking is the following:

1. (A) 583 survivors (10.7%).
2. HN 590 survivors (10.8%).
3. ARD 686 survivors (12.6%).
4. Right identity 2102 survivors (38.6%).
5. (B) 2322 survivors (42.6%).
6. (A)+(B) 2333 survivors (42.8%).
7. x^2 = y^2 4112 survivors (75.4%).
   (We can also compute the intersections of the survivors, etc. in order to try to get a smaller final list, with smaller countermodels).

3) I have shown that a magma operation is right division for a group iff it satisfies ARD, has all squares equal, and has a right identity element (this is possibly known, I didn't check). The proof:

Proposition. Let $(G,\cdot)$ be a magma. Then $\cdot$ is $xy = x*y^{-1}$ for some operation $*$ making $(G,*)$ a group if and only if $x(y(zu)) = (x(uz))y$, $xx = yy$, and there exists an element $e\in G$ such that $xe = x$ for all $x,y,z,u\in G$.

Proof: First suppose $(G,*)$ is a group with unit $e$. Then $xy:=x*y^{-1}$ satisfies
$x(y(zu)) = x(y(z*u^{-1})) = x(y*u*z^{-1}) = x*z*u^{-1}*y^{-1} = (x*z*u^{-1})y = (x(u*z^{-1}))y = (x(uz))y$,
$xe = x*e^{-1} = x$, and $xx = x*x^{-1} = e = yy$.
Now let $(G,\cdot)$ satisfy the properties of the statement, define $x*y:=x(ey)$ and $x^{-1}:=ex$, and note that $xx = ee = e$ for all $x$. Then
$(x*y)*z = (x(ey))(ez) = x((ez)(ye)) = x((ez)y) = x((e(ze))y) = x(e(y(ez))) = x(*y*z)$,
$x*x^{-1} = x(e(ex)) = (x(xe))e = xx = e$,
$x^{-1}*x = (ex)(ex) = e$, $x*e = x(ee) = xe = x$, and
$e*x = e(ex) = (xx)(ex) = (x(xe))(ex) = x((ex)(ex)) = xe = x$.

[Vlad Tsyrklevich]

Bruno Le Floch said:

Vlad Tsyrklevich If I understand correctly the code ![X,Y,X] etc in your message states that if $R_Z\circ R_Y$ is surjective then it is injective. It can be split into two results, maybe easier to work with: if $R_Z\circ R_Y$ is surjective then $R_Z$ and $R_Y$ are surjective, and separately if these are surjective then they are injective. (The fact that composing injectives gives an injective does not depend on finiteness.)

tl;dr Ordering of axioms in a TPTP input is important, and redundant axioms may be helpful for a guiding a search.

As Bruno noted, one of my axioms could be simplified, and indeed looking at the original input I found that that axiom was actually redundant to other earlier axioms.

Original TPTP

%---- 73288447 => 42323216
fof(hypothesis, axiom, ![X,Y,Z] : X = mul(mul(Y, Y), mul(mul(mul(Y, X), Z), mul(mul(X, mul(X, Y)), Z))) ).
fof(goal, conjecture, ![X,Y,Z] : X = mul(Y, mul(mul(mul(mul(Y, Y), X), Z), mul(mul(mul(Y, Y), Y), Z))) ).
fof(inverse1, axiom, ![X,Y,Z] : X = mul(mul(mul(Y, mul(mul(Y, Y), X)), Z), mul(mul(mul(mul(Y, Y), X), mul(mul(mul(Y, Y), X), Y)), Z))).
fof(eq3_surj_inj, axiom, ![X] : ?[T] : ( X = mul(T, T) ) => ![T1,T2] : ( (mul(T1, T1) = mul(T2, T2) ) => T1 = T2 )).
fof(eq3_inj_surj, axiom, ![T1,T2] : ( (mul(T1, T1) = mul(T2, T2) ) => T1 = T2 ) => ![X] : ?[T] : ( X = mul(T, T) )).
fof(eq4_surj_inj, axiom, ![X,Y] : ?[T] : ( X = mul(T, Y) ) => ![Y,T1,T2] : ( (mul(T1, Y) = mul(T2, Y) ) => T1 = T2 )).
fof(eq4_inj_surj, axiom, ![Y,T1,T2] : ( (mul(T1, Y) = mul(T2, Y) ) => T1 = T2 ) => ![X,Y] : ?[T] : ( X = mul(T, Y) )).
fof(eq5_surj_inj, axiom, ![X,Y] : ?[T] : ( X = mul(Y, T) ) => ![Y,T1,T2] : ( (mul(Y, T1) = mul(Y, T2) ) => T1 = T2 )).
fof(eq5_inj_surj, axiom, ![Y,T1,T2] : ( (mul(Y, T1) = mul(Y, T2) ) => T1 = T2 ) => ![X,Y] : ?[T] : ( X = mul(Y, T) )).
fof(eq8_surj_inj, axiom, ![X] : ?[T] : ( X = mul(T, mul(T, T)) ) => ![T1,T2] : ( (mul(T1, mul(T1, T1)) = mul(T2, mul(T2, T2)) ) => T1 = T2 )).
fof(eq8_inj_surj, axiom, ![T1,T2] : ( (mul(T1, mul(T1, T1)) = mul(T2, mul(T2, T2)) ) => T1 = T2 ) => ![X] : ?[T] : ( X = mul(T, mul(T, T)) )).
fof(eq11_surj_inj, axiom, ![X,Y] : ?[T] : ( X = mul(T, mul(Y, Y)) ) => ![Y,T1,T2] : ( (mul(T1, mul(Y, Y)) = mul(T2, mul(Y, Y)) ) => T1 = T2 )).
fof(eq11_inj_surj, axiom, ![Y,T1,T2] : ( (mul(T1, mul(Y, Y)) = mul(T2, mul(Y, Y)) ) => T1 = T2 ) => ![X,Y] : ?[T] : ( X = mul(T, mul(Y, Y)) )).
fof(eq23_surj_inj, axiom, ![X] : ?[T] : ( X = mul(mul(T, T), T) ) => ![T1,T2] : ( (mul(mul(T1, T1), T1) = mul(mul(T2, T2), T2) ) => T1 = T2 )).
fof(eq23_inj_surj, axiom, ![T1,T2] : ( (mul(mul(T1, T1), T1) = mul(mul(T2, T2), T2) ) => T1 = T2 ) => ![X] : ?[T] : ( X = mul(mul(T, T), T) )).
fof(eq31_surj_inj, axiom, ![X,Y] : ?[T] : ( X = mul(mul(Y, Y), T) ) => ![Y,T1,T2] : ( (mul(mul(Y, Y), T1) = mul(mul(Y, Y), T2) ) => T1 = T2 )).
fof(eq31_inj_surj, axiom, ![Y,T1,T2] : ( (mul(mul(Y, Y), T1) = mul(mul(Y, Y), T2) ) => T1 = T2 ) => ![X,Y] : ?[T] : ( X = mul(mul(Y, Y), T) )).
fof(new_bijectivity_axiom, axiom, ![X,Y,Z] : ?[XT] : ( X = mul(mul(XT, Y), Z) ) <=> ![XT1,XT2,Y,Z] : ( (mul(mul(XT1, Y), Z) = mul(mul(XT2, Y), Z) ) => XT1 = XT2 ) ).

Solving the original TPTP takes ~6s on my laptop, and while the new_bijectivity_axiom is derivable from the two eq4 axioms, removing it causes the run not to finish after 10 minutes. By manually removing individual axioms and timing the runs, I managed to get the following TPTP that takes ~1s to finish.

Minimized TPTP

fof(fof(goal, conjecture, ![X,Y,Z] : X = mul(Y, mul(mul(mul(mul(Y, Y), X), Z), mul(mul(mul(Y, Y), Y), Z))) ).
fof(inverse1, axiom, ![X,Y,Z] : X = mul(mul(mul(Y, mul(mul(Y, Y), X)), Z), mul(mul(mul(mul(Y, Y), X), mul(mul(mul(Y, Y), X), Y)), Z))).

fof(eq4_surj_inj, axiom, ![X,Y] : ?[T] : ( X = mul(T, Y) ) => ![Y,T1,T2] : ( (mul(T1, Y) = mul(T2, Y) ) => T1 = T2 )).
fof(eq4_inj_surj, axiom, ![Y,T1,T2] : ( (mul(T1, Y) = mul(T2, Y) ) => T1 = T2 ) => ![X,Y] : ?[T] : ( X = mul(T, Y) )).
fof(eq5_surj_inj, axiom, ![X,Y] : ?[T] : ( X = mul(Y, T) ) => ![Y,T1,T2] : ( (mul(Y, T1) = mul(Y, T2) ) => T1 = T2 )).
fof(eq5_inj_surj, axiom, ![Y,T1,T2] : ( (mul(Y, T1) = mul(Y, T2) ) => T1 = T2 ) => ![X,Y] : ?[T] : ( X = mul(Y, T) )).
fof(eq23_surj_inj, axiom, ![X] : ?[T] : ( X = mul(mul(T, T), T) ) => ![T1,T2] : ( (mul(mul(T1, T1), T1) = mul(mul(T2, T2), T2) ) => T1 = T2 )).
fof(eq23_inj_surj, axiom, ![T1,T2] : ( (mul(mul(T1, T1), T1) = mul(mul(T2, T2), T2) ) => T1 = T2 ) => ![X] : ?[T] : ( X = mul(mul(T, T), T) )).
fof(eq31_inj_surj, axiom, ![Y,T1,T2] : ( (mul(mul(Y, Y), T1) = mul(mul(Y, Y), T2) ) => T1 = T2 ) => ![X,Y] : ?[T] : ( X = mul(mul(Y, Y), T) )).

fof(new_bijectivity_axiom, axiom, ![X,Y,Z] : ?[XT] : ( X = mul(mul(XT, Y), Z) ) <=> ![XT1,XT2,Y,Z] : ( (mul(mul(XT1, Y), Z) = mul(mul(XT2, Y), Z) ) => XT1 = XT2 ) )., axiom, ![X,Y,Z] : ?[XT] : ( X = mul(mul(XT, Y), Z) ) <=> ![XT1,XT2,Y,Z] : ( (mul(mul(XT1, Y), Z) = mul(mul(XT2, Y), Z) ) => XT1 = XT2 ) ).

Now Vampire finishes in ~2.8s after removing the redundant new_bijectivity_axiom. However, playing with it further I noticed that the behavior really depends on ordering as well: moving eq5_inj_surj to the bottom position speeds it up to ~0.7s, but then on top of that moving eq4_inj_surj up one place slows the run down to 22s.

Up to now, I had not given much thought to ordering, but clearly the possible variance is massive. This unfortunately means that to try to exhaustively search for an implication with a non-trivial input set of axioms, there is a fairly large combinatorial space of orderings and inclusions that have to be considered.

[Vlad Tsyrklevich]

The combinatorial space was too large to exhaustively search, but just to experiment I sampled the 8 minimzed axioms in different orders/subsets and ran Vampire for 1s and found at least a few orderings/subsets of axioms that took under 0.4s. Interestingly in all of the fastest cases the ordering was alway that injective=>surjective axioms were ordered first and then surjective=>injective, but I don't know if this generalizes to other implications or initial choices of axioms.

There were quite a few successful runs with the initial choice of the minimized axioms, so I also tried running it against a sampling of orders/subsets of of the original 14 axioms (e.g. minus the redundant new_bijectivity_axiom). I could probably think of a way to sample more evenly than what I did, but out of 21,600 samples I took, vampire found the implication in 7 of them in under 1s. Indeed one of the runs had only 3 axioms. This suggests that sampling many different orderings/subsets of the bijectivity axioms and running them with short timeouts for the remaining open finite implications may be worth a try.

[Jose Brox]

Reporting some success:

The remaining candidates are:
[48217520, 48217671, 48273390, 58095440, 67953597, 67953691, 71553983, 71557731, 73169078, 73169229, 73173015, 73285871, 73288447, 73292531, 89177565, 90206751, 90209038, 90214894, 90265736, 102743259, 102744082, 102745815, 102749116, 105877422, 113067945, 113071354, 121884950, 122693826, 122697948, 129416953, 129420890, 129427563, 129428290, 157258878, 157258932, 163876110]

I have been exploring immunities. Recall that immunity of identity A to property B with respect to identity C is defined by the following equivalent assertions (which have a different feel to them):
1) There is no model of A which satisfies B but not C.
2) A+B implies C.
It also has the following consequence:
3) If A is immune to B with respect to C and A implies B then A implies C.

Since the remaining candidates present a lot of immunities to properties related to right division in groups, I'm trying to exploit consequence 3) to show that some candidates are in fact equivalent to HN.

I have shown the following immunities with Prover9:
1) All remaining candidates are immune to ARD.
2) All remaining candidates are immune to the existence of a right identity element.
3) All remaining candidates are immune to $x^2 = y^2$, but 2 of them which remain unknown:
[102745815, 102749116]
(I'm running most expensive searches against them now).

On the other hand, I have been able to show that one candidate implies $x^2 = y^2$, so it is in fact equivalent to HN:
[71557731]
The shortest (in time and length) proof I have been able to find after tweaking has run in 278s. I attach the two relevant proofs (immunity plus implication).
PROVER9 71557731 implies xx=yy PROOF2 expanded.txt
PROVER9 71557731 with xx=yy implies HN PROOF.txt

The immunities are found quickly and easily, but the $xx=yy$ implication has turned out to be very sensitive to the search parameters (I'm benchmarking it now). The smaller the max_weight and sos_limit values the better, but not so low that the search is exhausted without finding the proof; on the other hand, the search time looks more sensitive to an increment in sos_limit than in max_weight.

(I know there are several proposed ideas by @Terence Tao and @Bruno Le Floch that I need to check, I will come to them, I'm just lagging a bit behind with all my running experiments and my eventual electrical blackouts at home :big_smile: ).

[Jose Brox]

Jose Brox ha dicho:

1) All remaining candidates are immune to ARD.
2) All remaining candidates are immune to the existence of a right identity element.
3) All remaining candidates are immune to x2=y2, but 2 of them which remain unknown:
[102745815, 102749116]

Note that this implies that potential countermodels to the remaining candidates cannot satisfy ARD, nor $x^2=y^2$, nor have right identity element, so if there indeed are countermodels to some of them, they must be quite far removed from being right division in a group.

[Terence Tao]

@Jose Brox If I understand correctly, you have found a positive implication between (somewhat lengthy) laws that can be proven by an ATP, but only after a significant period of time? Having such an example would be worth noting in the paper. As I understand it, all the positive implications in the standard graph (i.e., between equations at most 4) can be done in seconds in Vampire (actually, it would be good to get statistics for this on the paper also).

Actually, I'll start a separate thread about this shortly.

[Vlad Tsyrklevich]

This is a very interesting example, vampire only reaches step 21 of your proof in 14s, it's slowing down very quickly at each additional step. I have not learned about tweaking vampire parameters up until now, but this example makes me re-think the assumption that if a proof exists, vampire will find it relatively quickly. I wonder if the remaining order 5 unknowns may be similarly solvable.

[Jose Brox]

Vlad Tsyrklevich ha dicho:

but this example makes me re-think the assumption that if a proof exists, vampire will find it relatively quickly.

Well, this depends on the size of the identities, but I'm pretty sure the we should be able to concoct a family of implications $\{I_n\}$ with $I_n:=p_n\implies q_n$ such that if $T_n$ is the time Vampire needs to solve $I_n$ then $\frac{T_n}{f(n)}\to\infty$ for any polynomial $f$.

[Jose Brox]

Jose Brox ha dicho:

On the other hand, I have been able to show that one candidate implies x2=y2, so it is in fact equivalent to HN:
[71557731]

With hindsight, now I have made Prover9 find a direct proof of 71557731 implies HN in 357s, by using max_weight 300 and sos_limit 200.

[Vlad Tsyrklevich]

Vlad Tsyrklevich said:

This suggests that sampling many different orderings/subsets of the bijectivity axioms and running them with short timeouts for the remaining open finite implications may be worth a try.

I ran long brute forces with 10k samples per unknown implication and 1.5s per run, no new finite implications for order4/5 and H-N.

[Jose Brox]

Vlad Tsyrklevich ha dicho:

I ran long brute forces with 10k samples per unknown implication

Can you make runs with implication to the following necessary conditions, instead to the full HN identity, to see if we get something?
1) Associative right division:
m(X,m(Y,m(Z,W))) = m(m(X,m(W,Z)),Y)
2) Equal squares:
m(X,X) = m(Y,Y)
3) Existence of right identity:
?[E]: ![X]: m(X,E) = X

[Vlad Tsyrklevich]

Just so I'm up-to-date, can you give me the list of laws for which the finite implication is currently unknown?

[Jose Brox]

Vlad Tsyrklevich ha dicho:

Just so I'm up-to-date, can you give me the list of laws for which the finite implication is currently unknown?

Here it is!
[48217520, 48217671, 58095440, 73169078, 73169229, 73285871, 102743259, 102744082, 102745815, 102749116, 113067945, 113071354, 121884950, 122693826, 122697948]

[Jose Brox]

Jose Brox ha dicho:

Can you make runs with implication to the following necessary conditions

@Vlad Tsyrklevich Just to clarify, I mean one at a time, not altogether (otherwise they imply HN).

[Vlad Tsyrklevich]

A quick run with just inverses + simple bijections doesn't have any hits for any of those 3, I'll run a bruteforce overnight with sampled bijections.

[Vlad Tsyrklevich]

73285871 => 40 can be established using inverses+bijections as demonstrated by the following TPTP

%---- 73285871 => 40
fof(hypothesis, axiom, ![X,Y,Z] : X = mul(mul(Y, Y), mul(mul(mul(X, Y), Z), mul(mul(X, mul(Y, X)), Z))) ).
fof(goal, conjecture, ![X,Y] : mul(X, X) = mul(Y, Y) ).
fof(inverse, axiom, ![X,Y,Z] : X = mul(mul(mul(mul(mul(Y, Y), X), Y), Z), mul(mul(mul(mul(Y, Y), X), mul(Y, mul(mul(Y, Y), X))), Z))).
fof(eq23_surj_inj, axiom, ![X] : ?[T] : ( X = mul(mul(T, T), T) ) => ![T1,T2] : ( (mul(mul(T1, T1), T1) = mul(mul(T2, T2), T2) ) => T1 = T2 )).
fof(eq10_inj_surj, axiom, ![T1,T2,Y] : ( (mul(T1, mul(Y, T1)) = mul(T2, mul(Y, T2)) ) => T1 = T2 ) => ![X,Y] : ?[T] : ( X = mul(T, mul(Y, T)) )).
fof(eq31_inj_surj, axiom, ![Y,T1,T2] : ( (mul(mul(Y, Y), T1) = mul(mul(Y, Y), T2) ) => T1 = T2 ) => ![X,Y] : ?[T] : ( X = mul(mul(Y, Y), T) )).
fof(eq3_inj_surj, axiom, ![T1,T2] : ( (mul(T1, T1) = mul(T2, T2) ) => T1 = T2 ) => ![X] : ?[T] : ( X = mul(T, T) )).

[Vlad Tsyrklevich]

I gave the runs 1.5s each and this run finished in 1.499 s. Maybe I should re-run with higher timeouts after this.

[Vlad Tsyrklevich]

By the way, just to distribute the knowledge, after equational#943 lands you could have done the same thing I've done by generating a CSV with entries comma-seperated values like:

48217520,912704
48217520,40
48217671,912704

etc.

and then using it like so cat input.csv | ruby equational_theories/Generated/FiniteImplicationSearch/src/generate_tptp.rb --inverses --bruteforce-bijections2 5000 output_dir. After that, you just need to run vampire against the TPTPs in that dir. A command line to generate those commands is given in FiniteImplicationSearch/README.md For the identity condition though I did have to do something slightly custom since it's not in the form of one of our equations.

[Vlad Tsyrklevich]

The finite implication workflow is basically to just generate a dir of TPTP files with various axioms depending on the input parameters, and then run vampire against them.

[Jose Brox]

Vlad Tsyrklevich ha dicho:

73285871 => 40 can be established using inverses+bijections

Nice! :tada:

[Jose Brox]

Vlad Tsyrklevich ha dicho:

By the way, just to distribute the knowledge

Thank you very much, this is very informative. I'm working in Windows, so I use Ubuntu in the virtual machine, but I have some problems with CMake and haven't been able to compile Vampire yet (didn't give it much thought, didn't have the time). Also I'm really newbie to GitHub, yesterday I started reading tutorials...

[Vlad Tsyrklevich]

You should also be able to do the same on Windows using something like WSL. Instead of building vampire on Linux, you can just download a binary from https://github.com/vprover/vampire/releases

[Jose Brox]

Vlad Tsyrklevich ha dicho:

73285871 => 40 can be established using inverses+bijections

Since 73285871 together with 40 implies HN (i.e., it is immune to 40), your result implies that 73285871 is Austin equivalent to HN, so one more for the list! :tada:

The proof is found in 0.38s with Prover9 max_weight 100, sos_limit 200.
PROVER9 73285871 with xx=yy implies HN proof extended.txt

So now we have 21 candidates (at least) Austin equivalent and 14 completely unknown.

[Jose Brox]

Btw, recall that the only identities not known to be immune to 40 are
[102745815, 102749116], so if any of the rest happen to imply 40 in the finite setting, we can repeat the process. Similarly with right identity element and with ARD (all remaining candidates are immune to both).

[Vlad Tsyrklevich]

Instead of 5000 samples at 1.5s, I re-ran with 500 samples at 4s, and got multiple hits for 73285871 => 40 but nothing else.

[Jose Brox]

Another candidate, 102744082, turns out to be equivalent to HN!

As you know, I'm running long Prover9 searches with different conditions, because I'm not convinced we have discarded all equivalent candidates yet (since order 8 is way more difficult for ATPs than order 4, the analogy with the main project is not perfect). Note that this one we didn't even know to be Austin equivalent to HN!

In a 10h run per candidate I have found that 102744082 has right multiplication injective, and this candidate together with this property is easily shown to be equivalent to HN by Prover9. I attach the proof of the second fact (not of the first because these proofs coming from long searches for all remaining candidates tend not to be optimized, so I am now running a specific search for this candidate with lower parameters).

PROVER9 102744082 with right mult injective implies HN PROOF extended.

Now we have 179 equations equivalent to HN, 21 at least Austin equivalent, and 13 completely unknown.

[Jose Brox]

Here is the proof of 102744082 implies right multiplication injective (970s with max_weight 300 sos_limit 200).

PROVER9 102744082 implies right mult injective PROOF extended

[Jose Brox]

For comparison, I have tried a direct proof of 102744082 implies HN with the same parameters (300,200): it has run for 24000s without finding a proof. I will try now giving right multiplication injective as a hint for Prover9 (my last try with hints didn't produce real advantage, although it could have).

[Jose Brox]

Jose Brox ha dicho:

I will try now giving right multiplication injective as a hint for Prover9

Killed after 20500s with the hint without finding a proof.

[Jose Brox]

Jose Brox ha dicho:

Here is the proof of 102744082 implies right multiplication injective (970s with max_weight 300 sos_limit 200).

@Vlad Tsyrklevich I am now running Vampire directly from the binary in WSL (thank you!), currently doing some tests to get the hold of it. I have given it 2000s in default mode, and 1000s in casc mode, and it failed to prove that 102744082 implies right multiplication injective. My TPTP is the following:

fof(102744082, axiom,
 X = m(m(m(Y , Y) , m(m( X , Z) ,  X)) , m(m(Z , U) , m( X , U)))
).

fof(right_injective, conjecture,
 m(Y,X) = m(Z,X) => Y = Z
).

The calls are:

./vampire -t 2000 TPTP102744082injective.p
./vampire --mode casc -t 1000 TPTP102744082injective.p

Do you think there is anything wrong? I'm getting a "perf_event_open failed (instruction limiting will be disabled)" error (which doesn't disappear even when setting kernel.perf_event_paranoid=-1 as root as Vampire asks, do you have any suggestions?), but I've seen proofs found with this error.

If not, can you replicate this? It would mean that in this case Prover9 (with chosen parameters) finds the proof faster than Vampire.

[Vlad Tsyrklevich]

That TPTP looks right to me. You don't need --mode casc, just the first call should be fine (--mode casc will run the TPTP with a number of options split for smaller periods of time, which while it may be useful, is probably not as useful as finding the options you think are specifically the ones you need.) You can ignore the perf_event_open line I think, that's just a consequence of WSL but it shouldn't be serious.

[Vlad Tsyrklevich]

I think in this case it is possible that Prover9 is faster, indeed I was not able to get some of your previous examples to finish in Vampire, though I have not spent much time looking at configuration options for vampire that may replicate the ones you use with Prover9

[Jose Brox]

Reporting some negative results (or at least negative for the moment being):

A while ago, @Bruno Le Floch noticed that candidate 71546843 was implied by the Putnam equation 14, and wondered which other candidates were implied by smaller identities.

Accordingly, I am running a search in which I determine which smaller equations don't imply HN, then I see if any of them implies any of the 13 remaining candidates (the ones we don't know to be Austin equivalent to HN). The rationale is that if A -> B and A -/> C then B-/>C (since A->B->C implies A->C).

What I actually do is to first determine the implications and antiimplications to HN in a range of "small" identities by running the candidate implication in Prover9 and Mace4 for a while; after the process we either know the status of the implication, or it is inconclusive. Then I test the antiimplications to HN against the HN candidates: if we find any implication, we get a hit and discard the candidate. After that, I test the inconclusive implications against the candidates: if we find any implication, we need to study further that inconclusive implication with Mace4, hoping that it actually is an antiimplication.

At the moment I have run this process up to equation 16000 (recall that HN has id number 42323216). All antiimplications to HN found have resulted to also be antiimplications to the remaining candidates, so no luck there (I have checked against older candidates, and some can be discarded by the process).

Interestingly, there has been no luck either with the 71 inconclusive implications found: they are also inconclusive for all the candidates with the chosen parameters, so more computing time needs to be dedicated to them.

[Jose Brox]

Another idea I'm exploring: if a candidate really implies HN (or Austin implies), then this must be still true if we add some other condition to the candidate (candidate + P -> HN + P). E.g., if the underlying group operation is commutative, then we expect the candidate to satisfy Tarski's axiom 543 (we can easily show that this is so iff right division satisfies $x(yz) = z(yx)$, which is 4369).

Hence with inconclusive candidates we can let P run and check candidate+P -> HN (resp. also with added finiteness conditions). The more implications we can prove, heuristically the more probable is that the candidate indeed implies HN in all cases (resp. in the finite case), and on the contrary, if most implications remain inconclusive, then either the candidate is only Austin equivalent or not equivalent at all.

I will report on this when I come back, but feel free to explore this yourself if you have the time and Prover9/Mace4 installed (I attach a Jupyter notebook with Python code [EDITED WITH BETTER VERSION]):
HIGMAN-NEUMANN - Antiimplications to Tarski's axiom with commutativity-COMPLETELY UNKNOWN CANDIDATES.ipynb

[Jose Brox]

Jose Brox ha dicho:

Another idea I'm exploring: if a candidate really implies HN (or Austin implies), then this must be still true if we add some other condition to the candidate (candidate + P -> HN + P). Hence with inconclusive candidates we can let P run and check candidate+P -> HN (resp. also with added finiteness conditions). The more implications we can prove, heuristically the more probable is that the candidate indeed implies HN in all cases (resp. in the finite case), and on the contrary, if most implications remain inconclusive, then either the candidate is only Austin equivalent or not equivalent at all.

Here we have the results of that test with P running in the range [2,5000]:

AUSTIN CANDIDATES

48273390: 37,
67953597: 271,
67953691: 130,
71553983: 21,
73173015: 32,
73285871: 242,
73288447: 362,
73292531: 72,
89177565: 98,
90206751: 252,
90209038: 300,
90214894: 60,
90265736: 15,
105877422: 260,
129416953: 296,
129420890: 153,
129427563: 14,
129428290: 10,
157258878: 41,
157258932: 27,
163876110: 23

COMPLETELY UNKNOWN CANDIDATES

48217520: 303,
48217671: 279,
58095440: 364,
73169078: 193,
73169229: 316,
102743259: 298,
102745815: 281,
102749116: 43,
113067945: 199,
113071354: 268,
121884950: 319,
122693826: 396,
122697948: 35

Taking <1% and >5% thresholds respectively, we can guess that:

1) From the Austin equivalent candidates, those probably being equivalent to HN are
{48273390, 71553983, 73173015, 90265736, 129427563, 129428290, 157258878, 157258932, 163876110},
while those probably not being equivalent to HN are
{67953597, 73288447, 90206751, 90209038, 105877422, 129416953}.
We cannot decide for
{67953691, 73285871, 73292531, 89177565, 90214894, 129420890}.

2) From the completely unknown candidates, those probably being equivalent to HN are
{102749116, 122697948},
while those probably not being equivalent to HN are
{48217520, 48217671, 58095440, 73169229, 102743259, 102745815, 113071354, 121884950, 122693826}.
We cannot decide for
{73169078, 113067945}.

I have yet to run a test with extra finiteness conditions to sieve those completely unknown candidates which may be Austin equivalent to HN.

More work to do: This test can be refined in at least two ways. We can exclude those P such that candidate+P implies x=y, and we can expand the range above 5000.