Some results from order 5

Stream: Equational

[Vlad Tsyrklevich]

Out of curiosity to find more Austin laws, and also a desire to have a larger test set to test finite implication tooling, I decided to look at which laws of order 5 imply Equation 2.

Order 5 includes an additional 57,882 laws, of those 19,392 have only trivial models. One interesting, though not particularly surprising, thing I observed here is that vampire begins to really slow down. For example, the implication 23635=>2 takes around a second on my laptop to find and the resulting vampire proof is >100 steps. For implications to Eq2 of order <= 4, the slowest vampire run takes ~0.01s and has <50 steps.

Using finite magmas from the repository, as well as some I found on my own, I found 38,318 laws satisfied by a finite model. Another interesting-though-not-surprising observation here is that, if I am interpreting mace4 output correctly, I found 3 order 5 laws (modulo duality and equivalence class) that are satisfied by magmas of minimum size 17--mace4 was able to find these 3 examples quickly so they may just be the easiest examples to resolve. Note that unlike the implications above, I have not formalized this result so there is the possibility of an error.

This leaves 172 laws. Of those, 106 finite imply equation 2.

Group 1: In 10/106 cases, vampire's decision procedures terminates without finding an implication to equation 2, meaning they are inequivalent. These are Austin laws, though the non-implication from vampire can not be formalized. According to vampire, all laws in this set also do not imply each other so they are all inequivalent. Note that Kisielewicz's second Austin law, 28770, is among this set. (Vampire's decision procedure also concludes for his order 6 Austin law.)

Group 2: In 96/106 cases, vampire's decision procedure for implication to equation 2 does not terminate, so it is unclear if these laws permit infinite models. According to our experience in order <= 4, if an implication exists vampire is able to find it, so this indicates that these laws should allow infinite models, though it's not clear if this intuition about vampire's behavior continues to hold in order 5. Vampire's decision procedure also does not terminate when trying to establish equivalence between any laws in this set. Note that equation 5093, mentioned by Kisielewicz as a possible Austin law, is this in set.

Group 3: The remaining 66 reduce to 25 modulo duality and equivalence class. Of those, Vampire concludes that 1 of the 25 does not imply equation 2, though it's not clear if it allows finite models or not. For the remaining 24, I don't know if they permit finite or infinite models. There are some equivalence classes and a few implications between laws in this set.

Part of my motivation for doing this work was testing finite implications against a larger/different set. I have some ideas for finding finite implications from group 3 that I've been testing, but this has yielded nothing so far. All of the finite implications were found using the same methods from order <= 4.

[Zoltan A. Kocsis (Z.A.K.)]

Another interesting-though-not-surprising observation here is that, if I am interpreting mace4 output correctly, I found 3 order 5 laws (modulo duality and equivalence class) that are satisfied by magmas of minimum size 17--mace4 was able to find these 3 examples quickly so they may just be the easiest examples to resolve. Note that unlike the implications above, I have not formalized this result so there is the possibility of an error.

In standard configurations mace4 will exhaust any smaller possibilities before trying to construct size 17 models. I guess there are strong constraints coming from these equations which allow it to exhaust any smaller counterexamples. You should see messages on stderr informing you whenever mace4 exhausts possible models of a given size. Caveat: If you're doing something weird (e.g. running 16 parallel instances of mace4, with -n 2to -n 17, keeping the first one that terminates then killing the rest) this will not apply.

[Vlad Tsyrklevich]

Yes, I'm not using it in parallel--I'm just new enough to the tool that I'm wary about misinterpreting

[Alex Meiburg]

Could you share the equations with the minimum-size-17, and the models that Mace found?

I guess I'm hoping that there's an interesting mathematical structure that they specify, and hopefully staring at the table would make it have somewhat clear

[Vlad Tsyrklevich]

(Note: To look up equation ids you can look at line numbers in data/eq_size5.txt or use Bruno's new fast script)

Data

Equivalence class [5296, 6266, 7739, 13035, 29762, 29852]
Table [[0,2,4,9,5,7,1,14,15,10,6,13,8,3,16,11,12],[3,1,7,4,6,0,9,8,5,12,16,2,15,11,10,14,13],[9,10,2,13,14,1,12,0,11,5,8,16,3,4,15,7,6],[8,7,11,3,12,14,0,6,10,1,13,4,16,15,2,5,9],[10,8,6,5,4,16,15,2,9,3,7,14,1,12,0,13,11],[6,11,15,8,1,5,14,12,2,7,9,3,13,16,4,10,0],[13,5,10,16,0,12,6,9,7,14,3,15,4,2,11,1,8],[1,16,13,12,11,2,10,7,3,15,14,6,0,9,8,4,5],[7,13,9,1,15,4,2,11,8,16,5,12,14,0,6,3,10],[15,0,14,11,13,8,3,16,12,9,2,7,10,5,1,6,4],[11,9,0,7,16,3,4,15,6,13,10,1,5,14,12,8,2],[16,14,5,15,9,6,8,13,1,0,4,11,2,10,7,12,3],[5,3,8,14,2,15,11,10,13,4,1,0,12,6,9,16,7],[12,15,16,6,7,10,5,1,4,11,0,8,9,13,3,2,14],[2,6,12,10,3,13,16,4,0,8,11,5,7,1,14,9,15],[14,4,3,0,10,11,7,5,16,2,12,9,6,8,13,15,1],[4,12,1,2,8,9,13,3,14,6,15,10,11,7,5,0,16]]

Equivalence class [5363, 6883, 6896, 10558, 11422, 20298, 25534, 30575]
Table [[0,2,4,5,8,7,15,1,6,12,11,14,16,10,9,13,3],[3,1,5,11,12,6,0,13,2,4,14,16,10,15,8,9,7],[5,10,2,1,7,14,4,15,16,6,13,9,8,12,3,0,11],[9,5,0,3,10,12,13,11,4,15,7,6,2,1,16,14,8],[7,13,11,14,4,2,3,9,1,5,16,10,15,0,12,8,6],[12,14,7,6,0,5,8,16,11,3,2,1,13,9,15,10,4],[2,8,16,10,11,13,6,12,9,14,15,0,3,7,5,4,1],[16,3,9,8,1,15,14,7,0,13,12,4,5,11,2,6,10],[1,12,10,15,14,9,2,4,8,16,0,3,7,6,11,5,13],[10,7,8,12,13,0,16,6,3,9,4,5,11,14,1,2,15],[6,9,14,16,5,1,7,8,13,11,10,15,0,3,4,12,2],[15,6,12,4,9,3,10,2,7,8,5,11,14,16,13,1,0],[11,15,1,13,6,16,5,0,10,2,9,8,12,4,7,3,14],[8,11,3,7,15,4,9,14,5,0,6,2,1,13,10,16,12],[13,4,15,0,16,8,1,5,12,10,3,7,6,2,14,11,9],[4,16,6,2,3,11,12,10,14,7,1,13,9,8,0,15,5],[14,0,13,9,2,10,11,3,15,1,8,12,4,5,6,7,16]]

Equivalence class [22823, 35981, 40363]
[[0,2,12,6,1,3,11,9,10,13,14,5,4,16,15,8,7],[3,11,1,10,7,4,0,14,2,12,6,8,15,13,5,16,9],[6,9,5,1,8,10,14,13,7,15,12,0,2,4,11,3,16],[4,0,7,2,9,15,3,6,11,1,10,16,5,12,8,13,14],[5,4,14,0,6,8,15,2,3,9,11,12,16,7,13,1,10],[12,16,11,5,0,1,13,4,8,2,15,14,7,10,9,6,3],[1,13,0,8,3,7,12,15,16,11,5,6,9,2,14,10,4],[15,3,9,11,14,5,4,10,0,7,2,13,8,1,16,12,6],[7,12,3,16,4,9,1,5,13,0,8,10,14,11,6,2,15],[8,15,6,3,10,16,5,11,4,14,0,1,13,9,12,7,2],[9,1,4,13,15,14,7,8,12,3,16,2,6,0,10,11,5],[2,6,16,9,13,11,10,1,14,8,7,4,0,5,3,15,12],[11,10,13,14,12,0,2,7,6,16,9,15,3,8,4,5,1],[10,14,8,7,16,2,6,12,9,5,1,3,11,15,0,4,13],[13,8,2,15,11,12,16,3,5,10,4,9,1,6,7,14,0],[16,5,10,4,2,13,8,0,15,6,3,7,12,14,1,9,11],[14,7,15,12,5,6,9,16,1,4,13,11,10,3,2,0,8]]

[Bruno Le Floch]

I'm looking at the last one of your list, Equivalence class [22823, 35981, 40363] and finding some patterns. Will report in an hour or so.

[Bruno Le Floch]

The last 17-element magma listed here (for the equivalent equations 22823, 35981, 40363) is actually just the linear model $x\diamond y=2x-4y\bmod 17$. Took me a while.

I won't analyse the other examples for now. For reference, my strategy to analyse the last 17-element example was as follows. Each result appears 17 times in the multiplication table, so none is obviously distinguished. But one of the elements is idempotent, call it u. Then note that orbits of Ru have length 8 so call the elements of one orbit 0,…,7, and the other 8,…,15, then notice some cyclicity in each block, namely most i*j are i+f(j-i) mod 8 (with a different f for the various blocks). Finally return to an early observation that Lu∘Ru∘Ru is the identity; notice that for all x, there exists y such that Ly∘Rx∘Rx is the identity, and note how x,y are related. Then relabel 0,…7 into even numbers 0,…,14, and 8,…,15 into odd numbers 1,…,15, with shifts, to make it so that L(x+1 mod 16)∘Rx∘Rx is the identity. Then realize that Z/16Z could be the group of units of the field F17, and try the 8 possible isomorphisms and something popped out.

[Jose Brox]

Vlad Tsyrklevich ha dicho:

vampire's decision procedures terminates without finding an implication to equation 2, meaning they are inequivalent.

This you mean as heuristic knowledge, or in the literal meaning that Vampire's decision procedures are exhaustive in some sense? If it is the second case, are you sure about that? (I think this is not the case with Prover9, and we know the theory of magmas with one identity to be undecidable).

[Terence Tao]

For the main project we were able to get quite a few refutations by randomly selecting linear magmas over small finite fields, such as the one of order 17. So perhaps one could try that to see if it handles any outstanding laws.

[Vlad Tsyrklevich]

Jose Brox said:

Vampire's decision procedures are exhaustive in some sense

My understanding is that the decision procedure based on the superposition calculus is complete, if it terminates without finding a solution then none is possible. e.g. see Section 3.4 of https://publik.tuwien.ac.at/files/PubDat_225994.pdf

[Jose Brox]

Vlad Tsyrklevich ha dicho:

My understanding is that the decision procedure based on the superposition calculus is complete, if it terminates without finding a solution then none is possible

Thanks for the reference! The superposition calculus is (refutation) complete, but the algorithms implementing it while trying to be efficient must be fair in order to guarantee completeness. I see from the paper that they have actually checked fairness for Vampire!

In contrast, although Prover9 is also based on saturation (theoretically uses the Otter algorithm), its manual says the following:

The resolution and paramodulation inference rules are intended to be complete [...], but we have not done a rigorous analysis of the algorithms, so users should not make any assumptions about completeness.

And in fact, I have noticed the following while using it: Sometimes Prover9 terminates with the message "Exhausted: no" which I believe should be interpreted as "(pretended) saturation achieved without finding a proof" (the terminations by time limit, memory limit, etc. have corresponding exit messages), what would mean that the implication is false. This usually happens with the default parameters, but if I give it more resources (more memory and larger limits for weight, sos number, demod step, demod size), then suddenly it runs much longer on the same problem and apparently doesn't reach saturation (usually reaches the time limit), which I think doesn't make sense if it really reached saturation with more stringent limits (unless someone has a rational explanation for this!).

[Alex Meiburg]

I'm not necessarily claiming that this is what Prover9 is doing, but I have seen several programs that will (sometimes) not solve problems with higher limits but do solve them with lower limits. The reasoning being, a program can progressively see how much of its computation time has been used for something, and may adapt some heuristics to try to maximize the probability of solving within that time limit. But inevitably sometimes those heuristics will get it wrong and lead to picking an algorithm that uses more resources, tries "harder", but actually doesn't solve a problem that a quick-n-dirty algorithm happened to be able to solve.

[Jose Brox]

Alex Meiburg ha dicho:

I have seen several programs that will (sometimes) not solve problems with higher limits but do solve them with lower limits. The reasoning being, a program can progressively see how much of its computation time has been used for something, and may adapt some heuristics

I have thought about this. I know Vampire does it, but my understanding is that Prover9 does not, it just runs "the Otter loop" within its prescribed limits (well, this can be changed with specific options, also with hints and semantic guidance; but the user has to specify them)... although I'm not a big expert, I just read the manual. Perhaps @Zoltan A. Kocsis (Z.A.K.) knows better?

[Vlad Tsyrklevich]

Terence Tao said:

For the main project we were able to get quite a few refutations by randomly selecting linear magmas over small finite fields, such as the one of order 17. So perhaps one could try that to see if it handles any outstanding laws.

This was a good idea, it found a couple almost immediately.

[Vlad Tsyrklevich]

I was able to generate a few more size 17 magmas, this time explicitly linear, but with no assurance that they're minimal. The results themselves were all size 11/17 magmas which matches what I saw with many magmas I saw with mace4 earlier. Presumably any laws that were satisfiable by anything smaller were already found by exhaustive search with mace4.

[Bruno Le Floch]

I'm confused why searching has to be done randomly. If we take x*y=ax+by+c and expand the equation (in the commutative ring ℤ[a,b,c]) we should get a few polynomial equations on a,b,c, and the question becomes whether a certain ideal is all of ℤ[a,b,c] or not, which I think is decidable? (Keywords may include Groebner bases, but I'm rusty on that.)

[Will Sawin]

Bruno Le Floch said:

I'm confused why searching has to be done randomly. If we take x*y=ax+by+c and expand the equation (in the commutative ring ℤ[a,b,c]) we should get a few polynomial equations on a,b,c, and the question becomes whether a certain ideal is all of ℤ[a,b,c] or not, which I think is decidable? (Keywords may include Groebner bases, but I'm rusty on that.)

I think for order 4 laws the situation was just that no one wrote code to convert a law into a polynomial equation and do the relevant Groebner basis calculation, but an exhaustive search over small-ish p was pretty fast, and since the polynomial equations end up having pretty small degree and small coefficients there must be a solution with small p if there is any solution. For laws of larger order one might need larger primes and so exhaustive search might be infeasible, in which case going to polynomial algebra would be a good idea.

[Vlad Tsyrklevich]

Disclaimer: At the edge of my math knowledge

I'm playing with this locally and there is also the requirement that the solutions be computable symbolically in a finite domain. I'm using sympy and while I can get a basis in $\Z$ I'm not sure that I can calculate the solutions over $\Z_{17}$ without resorting to bruteforce.

[Bruno Le Floch]

See also Github issue 364 "LINEAR: Compute the implication graph for linear magmas x ◇ y = a*x + b*y" claimed by user 'few'. It might make sense to coordinate with them.

[Jose Brox]

Will Sawin ha dicho:

I think for order 4 laws the situation was just that no one wrote code to convert a law into a polynomial equation and do the relevant Groebner basis calculation

What I did, for the commutative case, is to run a Sage (Python) script for getting the system of polynomial equations, then solve it with Wolfram Alpha online (was easier than programming the rest). The code is as follows:

var('a,b,x,y')

def prod(x,y):
    return a*x+b*y

def eq1729(x,y):
    return prod(prod(y,y),prod(prod(y,x),y))

p=eq1729(x,y)

p.coefficient(x).expand(),p.coefficient(y).expand()

The relevant Wolfram Alpha page is:
https://www.wolframalpha.com/input?i=solve+system+of+equations&assumption=%22FSelect%22+-%3E+%7B%7B%22SolveSystemOf2EquationsCalculator%22%7D%7D

[Vlad Tsyrklevich]

I've been busy with other tasks recently so I haven't spent as much time on this as I'd like. I thought I'd share the results here in case anyone wanted to look at them. Here are dual-reduced results for:

Group 1 (finite only trivial models, allows infinite models according to Vampire)

4916 x = y ◇ (x ◇ (x ◇ (y ◇ (z ◇ z))))
15535 x = y ◇ (((x ◇ (z ◇ z)) ◇ y) ◇ y)
**17522 x = (y ◇ z) ◇ (x ◇ (z ◇ (z ◇ z)))
20034 x = (y ◇ y) ◇ ((z ◇ (x ◇ x)) ◇ z)
22455 x = (y ◇ (x ◇ x)) ◇ ((y ◇ z) ◇ y)
**17522 is dual to 28770

Group 2 (finite only trivial models, unknown if they have infinite models)

4952 x = y ◇ (x ◇ (y ◇ (y ◇ (z ◇ y))))
4957 x = y ◇ (x ◇ (y ◇ (z ◇ (x ◇ z))))
5012 x = y ◇ (x ◇ (z ◇ (z ◇ (y ◇ z))))
5066 x = y ◇ (y ◇ (x ◇ (y ◇ (z ◇ y))))
5093 x = y ◇ (y ◇ (y ◇ (x ◇ (z ◇ y))))
5107 x = y ◇ (y ◇ (y ◇ (z ◇ (x ◇ y))))
5141 x = y ◇ (y ◇ (z ◇ (y ◇ (x ◇ y))))
5295 x = y ◇ (z ◇ (y ◇ (y ◇ (x ◇ y))))
5833 x = y ◇ (x ◇ (y ◇ ((z ◇ x) ◇ y)))
5834 x = y ◇ (x ◇ (y ◇ ((z ◇ x) ◇ z)))
5837 x = y ◇ (x ◇ (y ◇ ((z ◇ y) ◇ y)))
5947 x = y ◇ (y ◇ (x ◇ ((z ◇ x) ◇ y)))
5951 x = y ◇ (y ◇ (x ◇ ((z ◇ y) ◇ y)))
6820 x = y ◇ (y ◇ ((x ◇ y) ◇ (z ◇ y)))
6878 x = y ◇ (y ◇ ((z ◇ x) ◇ (x ◇ y)))
6895 x = y ◇ (y ◇ ((z ◇ y) ◇ (x ◇ y)))
6912 x = y ◇ (y ◇ ((z ◇ z) ◇ (x ◇ y)))
7587 x = y ◇ (x ◇ ((y ◇ (z ◇ x)) ◇ y))
7701 x = y ◇ (y ◇ ((x ◇ (z ◇ x)) ◇ y))
7755 x = y ◇ (y ◇ ((z ◇ (x ◇ x)) ◇ y))
7763 x = y ◇ (y ◇ ((z ◇ (x ◇ z)) ◇ y))
8485 x = y ◇ (x ◇ (((z ◇ x) ◇ y) ◇ y))
9337 x = y ◇ ((x ◇ y) ◇ (y ◇ (z ◇ y)))
9345 x = y ◇ ((x ◇ y) ◇ (z ◇ (y ◇ y)))
9384 x = y ◇ ((x ◇ z) ◇ (y ◇ (z ◇ z)))
9603 x = y ◇ ((z ◇ x) ◇ (y ◇ (x ◇ y)))
9663 x = y ◇ ((z ◇ y) ◇ (x ◇ (x ◇ y)))
9667 x = y ◇ ((z ◇ y) ◇ (x ◇ (y ◇ y)))
9680 x = y ◇ ((z ◇ y) ◇ (y ◇ (x ◇ y)))
10218 x = y ◇ ((x ◇ y) ◇ ((z ◇ x) ◇ y))
10222 x = y ◇ ((x ◇ y) ◇ ((z ◇ y) ◇ y))
11081 x = y ◇ ((x ◇ (y ◇ x)) ◇ (z ◇ y))
11082 x = y ◇ ((x ◇ (y ◇ x)) ◇ (z ◇ z))
11116 x = y ◇ ((x ◇ (z ◇ x)) ◇ (y ◇ y))
11205 x = y ◇ ((y ◇ (x ◇ y)) ◇ (z ◇ y))
11280 x = y ◇ ((y ◇ (z ◇ y)) ◇ (x ◇ y))
12073 x = y ◇ (((y ◇ x) ◇ x) ◇ (z ◇ z))
12087 x = y ◇ (((y ◇ x) ◇ z) ◇ (x ◇ z))
12234 x = y ◇ (((z ◇ x) ◇ y) ◇ (x ◇ y))
12857 x = y ◇ ((x ◇ (y ◇ (z ◇ z))) ◇ y)
12883 x = y ◇ ((x ◇ (z ◇ (y ◇ x))) ◇ y)
13764 x = y ◇ ((x ◇ ((z ◇ y) ◇ y)) ◇ y)
13849 x = y ◇ ((y ◇ ((x ◇ z) ◇ z)) ◇ z)
13992 x = y ◇ ((z ◇ ((x ◇ y) ◇ y)) ◇ y)
18137 x = (y ◇ x) ◇ (z ◇ ((x ◇ z) ◇ z))
18212 x = (y ◇ y) ◇ (x ◇ ((x ◇ z) ◇ z))
19966 x = (y ◇ y) ◇ ((x ◇ (x ◇ z)) ◇ z)
22619 x = (y ◇ (y ◇ x)) ◇ ((z ◇ z) ◇ z)

Group 3 (unknown if they allow finite models or infinite models)

12294 x = y ◇ (((z ◇ y) ◇ x) ◇ (x ◇ y))
13102 x = y ◇ ((z ◇ (x ◇ (x ◇ z))) ◇ y)
17286 x = (y ◇ x) ◇ (z ◇ (z ◇ (x ◇ z)))
20911 x = (y ◇ y) ◇ (((z ◇ x) ◇ x) ◇ z)
21714 x = (y ◇ (y ◇ x)) ◇ (x ◇ (x ◇ z))
21864 x = (y ◇ (z ◇ x)) ◇ (x ◇ (x ◇ y))
21865 x = (y ◇ (z ◇ x)) ◇ (x ◇ (x ◇ z))
21866 x = (y ◇ (z ◇ x)) ◇ (x ◇ (x ◇ w))
22446 x = (y ◇ (x ◇ x)) ◇ ((x ◇ z) ◇ z)
23337 x = ((y ◇ x) ◇ x) ◇ (z ◇ (x ◇ z))
23357 x = ((y ◇ x) ◇ y) ◇ (x ◇ (y ◇ z))

Group 4 (One equation that is unknown whether it allows finite models, but according to Vampire allows infinite models)

17260 x = (y ◇ x) ◇ (z ◇ (x ◇ (z ◇ z)))

EDIT: See https://teorth.github.io/equational_theories/blueprint/order-5-austin-laws.html

[Vlad Tsyrklevich]

Inspired by @Jose Brox's mace4 script I did a run last night with a different selection_measure and got one hit. I will try some other values over the next few nights and see what I find. Given how few equations there are in Group 3+4 I've also begun to track the maximum order that mace4 reaches for them, with the idea to only start searches at that order in the future but also as a metric to indicate how likely a particular law may have no finite models. Currently all laws in Group 3+4 have been exhaustively searched up to at least order 10.

[Jose Brox]

Vlad Tsyrklevich ha dicho:

Inspired by @Jose Brox's mace4 script I did a run last night with a different selection_measure and got one hit. I will try some other values

Yes, the search parameters make a big difference! Specially the combination of selection_order and selection_measure. I have been benchmarking those, but didn't finish yet so I didn't write about it here.

A summary: different combinations work better for different identities, but some combinations are usually advantageous. It seems that the best pairs (order, measure) are
(2,1), (2,3), (0,1), (0,3), and
very important in my experience, always set on the skolems_last parameter (with the command set(skolems_last).), because it speeds up the search greatly.

Changing from (2,4) to (2,1,skolems_last) I have sometimes seen an improvement of 5000x in the search! No kidding!

What I do to choose the best combination for a particular identity is to make a small run (up to size 6 or 7) for each combination, time them, then decide for the long search. And don't forget the skolems_last! :grinning_face_with_smiling_eyes:

[Vlad Tsyrklevich]

Jose Brox said:

(2,1), (2,3), (0,1), (0,3)

I assume this is (selection_order, selection_measure) yes? max_weight is for the Prover9 runs, right?

[Jose Brox]

Vlad Tsyrklevich ha dicho:

Jose Brox said:

(2,1), (2,3), (0,1), (0,3)

I assume this is (selection_order, selection_measure) yes? max_weight is for the Prover9 runs, right?

Oops yes, that's correct! Order and measure (I will edit above, thanks!). And it was a 5000x* speed up.

[Jose Brox]

Also, the experimental options are always set on in the GUI, and they also seem advantageous to have: lnh, negprop, neg_assign, neg_assign_near, neg_elim, neg_elim_near. I don't know if they are set on by default in the command line.

[Vlad Tsyrklevich]

According to this manual page they are.

[Jose Brox]

Jose Brox ha dicho:

summary: different combinations work better for different identities, but some combinations are usually advantageous. It seems that the best pairs (order, measure) are
(2,1), (2,3), (0,1), (0,3), and
very important in my experience, always set on the skolems_last parameter (with the command set(skolems_last).), because it speeds up the search greatly.

Changing from (2,4) to (2,1,skolems_last) I have sometimes seen an improvement of 5000x in the search! No kidding!

This rule of (2,1),(2,3) better than (2,4) has applied most of the time for the identities I have studied, but there also are exceptions. An important one is the weak central groupoids identity, which is explored by Mace4 way faster with (2,4), and the skolems_last parameter seems to be mostly irrelevant.

[Vlad Tsyrklevich]

I found an order 26 magma satisfying 12820 $x = y ◇ ((x ◇ (x ◇ (z ◇ z))) ◇ y)$. For this equation I have only exhaustively bruteforced magmas up to order 13, so this is not evidence that it is minimal, but vampire found no other satisfying magmas at lower orders within some time constraints.

 0  1  2  3  4  5  6  7  8  9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25
 8  0 12 18 25 10  5 13 21  7  6 24  4 14 11  9  3  2 15  1 23 16 20 22 17 19
10  5  0 22  6 14  9 18 20 21  4 13  8 24 15  1  2 23 12 25  7 11 16  3 19 17
 7  9 20  0  5  1 12  6  4 24 18 14 21 25 23  3 17 22  8 11 19 13 10  2 15 16
 2 17 16 23  0  7 10 25  9 11 22  6 19  5  1 12 15  3 20 13 24 18  4 14 21  8
13  7 11 21 19  0 25  2  3 22  8 23 14 18 10 17 12  6  4  9  1 20 15  5 16 24
 3 16 23 15 17  8  0 24 22 10  2  4  7 20 19 14 18 25 21  5 11 12  9  1  6 13
24 11 13  9 20 25  7  0 17  1 14 19 18  8 21  6 22 15 10  4 16 23  5 12  3  2
25  4 19 13  7  6 17  5  0  2  9 12 23 22 18 20 14 24 16 21 10  8  3 15 11  1
17 24 25 16  1 15  4  8  6  0  3  2 11 21  9  5 23 12 19 18 14 10 13 20  7 22
22 23  3 17 10  9  8 16 13 25  0 15  6 12 24 21  4  1  7 20 18 19  2 11  5 14
23 20 17 14  3 11  2 21 12 16  1  0 25 10  7 22 19  9  5 24  4  6 18 13  8 15
 9 15  6  1  8 19 22  3 10 14  5 17  0  4 13 16 21 20 24  2 12  7 11 25 18 23
11 14 21 19  9  2 20  1 24 12 23  5 22  0  8  4  6 16 13 15  3 17 25 18 10  7
12  2 18  6 15 16 21 23 11 17 13  8 20  9  0 10  1 14 25  3  5 24 19  7 22  4
 6 10  4  7 11 17 24 15  5  8 12 21  2 16  3  0  9 13  1 14 25 22 23 19 20 18
 4 12 10  8 22 18 11 19  1  6 16 20 13 15 25  2  0  7  3 23 21  9 24 17 14  5
20 22  8  2 18 21 13  4 15 23 19  1 17  6 12 24 11  0 14 16  9  5  7 10 25  3
 5  6  1  4 13 23 19 22  7 15 24 18 10 11 20  8 25 21  0 17  2  3 14 16  9 12
21  8  9 12 24  3 18 14 19 13 15  7 16  2  6 11 20  5 17  0 22 25  1  4 23 10
14 13  5 11 23 12 15 10 16 20 25  3  9  1 17 19 24 18 22  7  0  4 21  8  2  6
 1 19 15  5 14 20 23  9 25  4 17 10  3  7 16 18  8 11  2 22 13  0  6 24 12 21
16 21 22 25  2 24  1 20 18  3  7  9 15 17  5 13 10 19 23 12  8 14  0  6  4 11
18  3  7 10 21 13 16 12 14 19 20 22 24 23  2 25  5  4 11  6 17 15  8  0  1  9
15 18 14 24 16 22  3 17 23  5 11 25  1 19  4  7 13  8  9 10  6  2 12 21  0 20
19 25 24 20 12  4 14 11  2 18 21 16  5  3 22 23  7 10  6  8 15  1 17  9 13  0

[Vlad Tsyrklevich]

As I'm wrapping up these results, I thought I'd also document the maximum order of finite models that I had exhaustively searched up to (and including) for the remaining unknowns:

• 12294: 12
• 13102: 17
• 17260: 10
• 17286: 18
• 20911: 13
• 21714: 17
• 21864: 13
• 21865: 16
• 21866: 34
• 22446: 14
• 23337: 10
• 23357: 12

[Bruno Le Floch]

None of these equations have non-trivial finite linear models (commutative or non-commutative). I used that surjectivity ⇔ injectivity so I did not rule out infinite linear models. I am not 100% sure about the last one (23357) because I had to manipulate by hand some pretty messy polynomials.

[Bruno Le Floch]

If someone wants to think about these equations, here they are. Equation 21866 implies 21714, 21864, 21865.

Challenge: find non-trivial models for these order-5 equations

Equation 12294: x = y ◇ (((z ◇ y) ◇ x) ◇ (x ◇ y))
Equation 13102: x = y ◇ ((z ◇ (x ◇ (x ◇ z))) ◇ y)
Equation 17260: x = (y ◇ x) ◇ (z ◇ (x ◇ (z ◇ z)))
Equation 17286: x = (y ◇ x) ◇ (z ◇ (z ◇ (x ◇ z)))
Equation 20911: x = (y ◇ y) ◇ (((z ◇ x) ◇ x) ◇ z)
Equation 21714: x = (y ◇ (y ◇ x)) ◇ (x ◇ (x ◇ z))
Equation 21864: x = (y ◇ (z ◇ x)) ◇ (x ◇ (x ◇ y))
Equation 21865: x = (y ◇ (z ◇ x)) ◇ (x ◇ (x ◇ z))
Equation 21866: x = (y ◇ (z ◇ x)) ◇ (x ◇ (x ◇ w))
Equation 22446: x = (y ◇ (x ◇ x)) ◇ ((x ◇ z) ◇ z)
Equation 23337: x = ((y ◇ x) ◇ x) ◇ (z ◇ (x ◇ z))
Equation 23357: x = ((y ◇ x) ◇ y) ◇ (x ◇ (y ◇ z))

[Bruno Le Floch]

Concerning equation 21866, x = (y ◇ (z ◇ x)) ◇ (x ◇ (x ◇ w)). Define a graph with y→x iff ∃t, x = y◇t. If there is an arrow y→x then applying the equation with y,z replaced by a◇(b◇y),y for any a,b,w gives

x = ((a ◇ (b ◇ y))  ◇ (y ◇ (y ◇ t))) ◇ (x ◇ (x ◇ w)) = y ◇ (x ◇ (x ◇ w)) .

This in turn implies, for any u,z,

y = (u ◇ (z ◇ y)) ◇ (y ◇ (y ◇ (x◇(x◇w)))) = (u ◇ (z ◇ y)) ◇ (y ◇ x) ∈ {a◇(b◇x)|a,b∈M} .

Conversely, if y ∈ {a◇(b◇x)|a,b∈M} then equation 21866 immediately gives x = y ◇ (x ◇ (x ◇ w)) so y→x. So we have a graph associated to any 21866 magma. I think it also works for 21865 magmas and 21864 magmas (but not 21714 magmas). I get the impression that the graph does not capture the operation completely, but it might still be useful.
EDIT: Some more facts. For any x, z there must exist at least one path of length 2 between them, and one has the set equality {y|x→y→z} = {x*(w*z)|w∈M}. For any path x→y→z one has x◇(y◇z)=y. I'm convinced that there is more structure there.

[Vlad Tsyrklevich]

I forgot to mention, but the summary of the current state (with equations) is also now in the blueprint: https://teorth.github.io/equational_theories/blueprint/order-5-austin-laws.html

[Bruno Le Floch]

Law 13102 x = y◇((z◇(x◇(x◇z))◇y), currently in the "unknown" list (we didn't know anything about whether it has finite or infinite models), admits the piecewise linear infinite model (over $\mathbb{Q}$, or just dyadics)

$$x \diamond y = \begin{cases} (y - x)/2 & \text{if } 0\leq y \leq x , \\ y - x/2 & \text{if } y \leq 0 \leq x , \\ y - x & \text{otherwise} . \end{cases}$$

Indeed, one checks $y\diamond(x\diamond y) = -x$ for $x\leq 0$ and $-x/2$ for $x\geq 0$, and one checks similarly that $y\diamond(x\diamond(x\diamond y)) = -2x$ for $x\leq 0$ and $-x$ for $x\geq 0$, and that these two functions compose to the identity.

Regarding finite models, I get tantalizingly close to showing that this law has no finite model. In the finite setting left and right multiplications are bijective, all squares are equal (say, $x\diamond x=0$), one has $y\diamond(x\diamond y)=x\diamond 0=:B(x)$ and $y\diamond(x\diamond(x\diamond y))=x\diamond B(x)=:Q(x)$, and these two maps are inverse bijections. Using Prover9 I got that $B$ has no cycles of lengths $\leq 13$, but the proofs for each cycle lengths are not uniform. Starting from a given element $x$ and considering $L_x^k(x)$ I can work out large parts of the multiplication table, which is how I got to the piecewise linear model above. But there are gaps in what I can fill, which seem related to powers of 2 somehow. I also ruled out any finite model of size up to 50 using Mace4 (together with the above observations).

EDIT: I forgot to include that in the finite case (and in the piecewise linear model) $B$ (and $Q$) are automorphisms of the magma.

[Bruno Le Floch]

If we can prove that E13102⊨(finite)E2 as I expect, then this law may answer one of our "future-work" questions.

The piecewise linear model over $\mathbb{Q}$ is surjunctive in the following one-variable sense. For any one-variable function $f$ constructed from the operation $\diamond$ and constants, such as for instance $f(x) = ((x\diamond 3)\diamond ((-1/2)\diamond x))\diamond 2$, if $f$ is injective then it is surjective. Indeed, such a function is piecewise linear with finitely many pieces, so that in particular the function is asymptotically linear in both limits $x\to\pm\infty$; then injectivity implies surjectivity.

[Matthew Bolan]

A comment is that we may already have examples going the other way (surjectivity implying injectivity in this 1 variable sense), since given the nature of the greedy algorithm it is very hard to cook up 1 variable surjective maps of this sort from a greedily constructed magma to itself, and so the condition has a good chance of holding vacuously. The current counterexample to $3308 \to 3511$ may already be of this sort - I think it has elements which are not the product of any other two elements.

[Matthew Bolan]

Even if it isn't of that sort, you can take the direct product of it and a magma with constant multiplication

[Matthew Bolan]

That latest suggestion also cause trouble for building injective maps

[Matthew Bolan]

That example shows that $\text{E}3308, \neg\text{E}3511$ admits (vacuously) surjunctive models in the $n$-ary sense and no finite models, but the paper asks for equational theories specifically. It's hard to get the same tricks to work for an equational theory since the proof you cannot define non-trivial surjective maps boils down to the fact that $\diamond$ is not surjective, but equational theories which allow such multiplications admit models with constant multiplication. The proof one cannot build non-trivial injective maps is in similar trouble. Still, I feel that its quite likely for there to be some equational theory with vacuously surjunctive models.

[Bruno Le Floch]

Nice! Since groups are called "surjunctive" if injective ⇒ surjective (for definable maps of any number of variables), let me call the opposite implication "injunctive".

Your example of multiplying by a magma with constant multiplication provides a vacuuously surjunctive and injunctive model, which means that proving E3308⊨(finite)E3511 requires more than just injective⇔surjective. And indeed, the Lean proof uses Finite.f_ffg_implies_f_fgf, based on periodicity of f. This can help explain why some of your finite-magma investigations with Leo are failing.

[Matthew Bolan]

I suppose it is still somewhat conceivable that one could prove it via the fact injective⇔surjective on a proper subset of the magma, for example the image of $\diamond$.

[Bruno Le Floch]

I'm failing to get anywhere on E3308⊨(finite)E3511 with just injective⇔surjective on some subset.

The piecewise linear model of E13102 over $\mathbb{R}$ is surjunctive in the multivariate sense (I'm pretty sure it also holds over rationals). Namely any injective definable map from $\mathbb{R}^n$ to itself is surjective (but there are surjective non-injective maps). Indeed, every definable map is piecewise linear with finitely many pieces and we'll show that injectivity ⇒ surjectivity for this class of functions.

(GPT-5 Thinking Mini, checked and rewritten by me.) Consider an injective piecewise linear map defined by $f(v)=A_iv+b_i$ for $v\in R_i\subset\mathbb{R}^n$. In each region, $A_i$ is an invertible matrix by injectivity of $f$, so in each non-compact region at infinity one has the growth $|f(v)|=|A_iv+b_i|\gtrsim |v|$ at infinity. Overall, $|f(v)|\gtrsim|v|$ as $|v|\to+\infty$, and in particular $f$ is proper. Proper continuous maps are closed, so $f(\mathbb{R}^n)$ is closed. This image is also open by Brouwer's Invariance of Domain theorem, so it is all of $\mathbb{R}^n$.

[Bruno Le Floch]

One case of your idea, @Matthew Bolan, is the finite equivalence E3588⊨(finite)E3994, E3994⊨(finite)E3588, proven in the blueprint by using either one of injectivity⇒surjectivity or surjectivity⇒injectivity on the image of ◇. Maybe a more robust notion of surjunctivity and of injunctivity concerns maps between definable subsets? Or maybe we're simply reaching a zoo of different notions of surjunctivity and injunctivity depending on which lemmas we wish to impose.

[Matthew Bolan]

Oh, nice find! And yeah, I think that notion is fairly natural and will be more robust against this kind of cheap trick, though you'll want to make sure that you only consider maps from some definable subset to itself to avoid things like the injective but not surjective map $f:\{a\}\to \{a \diamond a, b\}$ given by $f(x) = x \diamond x$. Alternately I guess you could ask that if $S_1, S_2$ are definable sets and you have definable surjections both ways then any definable surjection between them is an injection, but this is maybe opening the zoo for business.