Bol/Moufang loops

Stream: Equational

[Alex Meiburg]

Since there's a couple of "special" equations added in the database, I would like to suggest adding the left/right Bol loop axioms, and the Moufang loop axiom(s), as well. These are two equations that have been studied a good deal, but usually in the context of loops, i.e. cancellative magmas with the identity. In that context, several relationships with other (short) equations are known, like Moufang loops being alternative. It is known that the Moufang axiom together with cancellativity implies the existence of an identity.

But I don't know if anything much is known about these equations in isolation. I've started a draft pr at equational#785, but I also don't know how to get the correct equation numbers. Could someone maybe run one of the automated tools to try to find easy examples / counterexamples? I'm hoping that they can just be placed in the graph without much extra work. :)

[Alex Meiburg]

Or I should say, maybe not much is known besides the fact that they're all implied by associativity.

[Terence Tao]

In principle one could find the equation numbers by running https://github.com/teorth/equational_theories/blob/main/scripts/generate_eqs_list.py with EQ_SIZE=6 and outputting to a file to find line numbers, but the file produced is rather large.

[Amir Livne Bar-on]

I checked why the find_equation_id.py script doesn't do it, and opened this PR to fix it:
https://github.com/teorth/equational_theories/pull/786

The first version of the identities in the Wikipedia article is
Equation 914612: x ◇ (y ◇ (x ◇ z)) = ((x ◇ y) ◇ x) ◇ z

[Eric Taucher]

Amir Livne Bar-on said:

PR to fix it

In the PR text is noted

search by Id

Is there an algorithm to go from id to equation and equation to id?

[Amir Livne Bar-on]

Currently not, there's an issue to find one. It would be easy to skip entire shape categories, except for symmetry breaking which changes the numbering a bit.

[Alex Meiburg]

equational#785 is ready for review. But, I realize now that none of the equations above 4696 actually show up on the Equation Explorer ... or on Graphiti it seems, even with "Show Sporadic Equations" checked.

e.g. https://teorth.github.io/equational_theories/graphiti/?render=true&limit_equations=1%2C2%2C28770&show_sporadic_equations=on doesn't show 28770, even though there @[equational_result]s about it relating to 1 and 2.

[Alex Meiburg]

Oh, it seems the CI failed saying "Install elan" failed. I have no clue why that would happen.

[Kevin Buzzard]

Might be a transient network issue. Try rerunning CI and see if it still fails.

[Vlad Tsyrklevich]

Alex Meiburg said:

or on Graphiti it seems, even with "Show Sporadic Equations" checked

The only results are a refutation (which Graphiti doesn't show), or a finite implication, which it does not yet support displaying. But yes there is an issue open for Equation Explorer displaying the sporadic equations.

[Vlad Tsyrklevich]

374794 shows, but as is typical for the sporadic equations, no implications/refutations have really been determined