Tarski's axiom 543

Stream: Equational

[Terence Tao]

I just learned today that Equation 543 x = y ◇ (z ◇ (x ◇ (y ◇ z))) was discovered by Tarski in 1938 as the axiom that captures the notion of subtraction in abelian groups. It's interesting that our project just sort of silently completed the analysis for this equation without flagging anything special about it! It does imply a reasonably large number (162) of other identities (as one would expect from a law codifying abelian groups), though it is far from the record-holder in this regard. I wonder if it has any other anomalous features that could have been picked up from our analysis; who knows what else we are missing out there in our graph!

[Junyan Xu]

Found this from Math.SE

[Harald Husum]

Huh, interesting. A bit of a side track, but it is implied by Equation 895, which interests me for other reasons.

That makes Equation 895 some special case of subtraction in abelian groups?

[Terence Tao]

Yes, it is equivalent to 1571, which is the law for subtraction (or equivalently, addition), in abelian groups of exponent 2. Hmm, I see that due to this equivalence 1571 doesn't show up much on equation explorer, as a temporary fix I will add a commentary to 895 with a pointer.

[Alex Meiburg]

I was thinking about this and it's actually quite a shame that we don't "capture" the relationship between Equation 543 and the associative (or commutative) laws in the graph. I understand why we don't, of course, the subtraction operation isn't commutative or associative, but I think this kind of fact ("this is an Abelian group!") is by some standards much more exciting! So I spent a while trying to think about how to formally extend this to a problem we could check off as yes/no.

I want to be able to say something like, "If a Magma M has operation * obeying equation A, then it has a _compatible_ operation obeying equation B." -- or, that it doesn't. This is absolutely the kind of language I would use about talking a particular equation pair, like 543<-->Associative. But "compatible" is a bit of a weasel word here, which would conventionally be defined in a way that explicitly relates the two operations. Since a magma doesn't otherwise have any structure, I could always just put some group structure on it and claim that the resulting operation is 'compatible', so that's not useful on its own.

I think the right notion here is relative first order definability. I would say that operations A and B are compatible if there's a first order formula to define each from the other with a first order formula. In this case with operations "-" and "+", that would be Forall x, y, z: x+y = z \iff x=z-y. Or, maybe alternatively, x+y := ExistsUnique z, x=z-y to be a bit more 'constructive'. There could then be a graph of which types of operations let us define other compatible operations. It would also form a DAG. I think this would be a great extension of the project.

[Alex Meiburg]

Proofs can be constructive (like the above). Disproofs, I think, would mostly look something like the form:

There is a magma [[1,0],[0,1]] which supports the operation x op1 y, and we want to know if there's a compatible x op2 y. But the only op2-magmas on two elements have no nontrivial automorphisms, and this magma does have an automorphism, so there can't be a op2 definable from the op1.

[Bhavik Mehta]

I think m(c, b) = c-((b-b)-b) should define addition from 543, so we could view compatibility as the derived magma operation m satisfying associativity using only 543 axioms? That is, if op1 satisfies 543 then op2(x, y) defined analogously to the above satisfies associativity

[Alex Meiburg]

Yes, so I guess in this case it's actually definable without quantifiers, which is a separate and stronger statement. That one doesn't go the other way: there's no way to define 543 from the group operation without quantifiers, but it can be defined with quantifiers.

[Adam Topaz]

Yes, the standard notion of a "definable function" in model theory is that the graph of the function is a definable subset (where definable allows quantifiers). We do have a model theory library in mathlib that could be used to phrase these things.

[Alex Meiburg]

That's something I would enjoy trying to formalize in Lean, I think. Maybe this weekend. See if I can get a definition written down and prove the 543 implication, and some non-implication. Even if it doesn't become a whole project to try to get as many as possible, it would be nice to have this kind of fact written down.

[Adam Topaz]

To point you in the right direction, here is the predicate saying that a subset is definable: docs#Set.Definable

[Adam Topaz]

I don't see a predicate for definable functions though.

[Adam Topaz]

There is also the related notion of "interpretability" in model theory, but as far as I know mathlib doesn't yet have a general framework to talk about interpretations.

[Floris van Doorn]

Adam Topaz said:

I don't see a predicate for definable functions though.

A function is definable iff (by definition?) its graph is definable, so it should be quite easy to get it from a definable set.

[Adam Topaz]

Yeah I know, I was hoping that we had a quality of life alias that would let us write Function.Definable f. Note that docs#Function.graph is not too convenient since it gives a relation, which means you would have to uncurry to get the predicate defining the graph as a subset.

[Michael Bucko]

This is a perhaps a good example of where AI could be helpful - discovery of known facts and connections. The entire knowledge base (one could chat with it) about all these equations could be generated in a couple of days.

A fun fact: the LLM insisted that the most interesting equation was 1323 (our mirror of "Ramanujan")

It also connected 543 with self-similarity and associativity, and 1323 with group-like structures, closure properties, and symmetries.

Here's the output:

• Equation 543: x=y◇(z◇(x◇(y◇z)))

  • Complex nested relationships with dependencies involving multiple variables.

  • Equation 1323: x=y◇(((y◇y)◇x)◇y)

  • Shows repeated operations, potentially representing associative-like properties.

  • Equation 1516: x=(y◇y)◇(x◇(x◇y))

  • Suggests imbalanced growth with mixed nesting of different elements.

  • Equation 1729: x=y◇((x◇(y◇y))◇x)

  • Includes a double-nested structure that may exhibit non-trivial symmetry.

  • Equation 1485: x=(y◇x)◇(x◇(z◇y))

  • Displays a mix of different elements with repeated references to x.

  • Equation 854: x=(y◇(z◇w))◇(x◇y)

  • Involves a balanced combination of four variables with consistent nesting.

  • Equation 500: x=y◇(z◇(x◇(w◇y)))

  • A multi-level nested equation showing dependencies between x, y, z, and w.

  • Equation 250: x=(y◇(z◇w))◇(x◇z)

  • Includes a balanced operation with a focus on the variable w.

  • Equation 333: x=(x◇(y◇z))◇(w◇y)

  • Suggests a more symmetric relationship involving all variables.

  • Equation 999: x=y◇(z◇((x◇y)◇w))

  • Features multiple levels of nesting and a cross-term operation.

  • Equation 777: x=(x◇y)◇(z◇(y◇w))

  • Reflects an associative-like chain involving multiple distinct terms.

  • Equation 1200: x=y◇(((y◇z)◇x)◇w)

  • Showcases multiple nested relationships between y, z, x, and w.

  • Equation 444: x=(y◇y)◇((x◇z)◇w)

  • Double-nested structure focusing on pairs of terms.

  • Equation 1300: x=y◇(((x◇z)◇y)◇y)

  • Emphasizes repeated interactions involving y.

  • Equation 222: x=(y◇x)◇(y◇(w◇z))

  • Demonstrates a complex interrelation among the variables.

  • Equation 111: x=(x◇y)◇((z◇w)◇y)

  • Reflects an imbalanced structure involving four variables.

  • Equation 888: x=y◇((z◇w)◇(x◇y))

  • A cross-term involving z, w, x, and y.

  • Equation 1600: x=(y◇z)◇(y◇(w◇x))

  • Features a multi-level interaction involving four variables.

  • Equation 300: x=(y◇(x◇z))◇(w◇y)

  • Shows dependencies between all four terms in a balanced form.

  • Equation 1500: x=(y◇x)◇(z◇(w◇u))

  • Displays a balanced multi-level nested form involving u.

[Alex Meiburg]

Started writing this down more precisely, how you can get a group structure x☐y = x◇((y◇y)◇y) out, and I noticed a kind of silly thing: the operation in Equation 543 also implies a different associative, commutative operation. x☐y = (y◇y). That is, the one that maps everything to a constant (the identity). Of course now there's no inverses.

But this is general. Anything that satisfies equation 40, x ◇ x = y ◇ y, lets you do this trick of building an operation that assigns everything to the same output. The result satisfies equation 46 x ◇ y = z ◇ w (which we mostly identify by the equivalent equation 41, x ◇ x = y ◇ z). Equation 46 turn implies many equations -- all the equations that have at least one operation on each side, including commutativity and associativity.

[Alex Meiburg]

The Hasse diagram for which equations have definable structure in terms of each other includes the Hasse diagram for implications, because you can always just define the new operation as precisely the old one. But this is a case of an interesting little collapse. Equation 41 implies Equation 40, so Equation 40 is definable from Equation 41. But Equation 41 is also definable from Equation 40, so they're in the same equivalence class.

That will in turn cause a collapse with several other equations into the same equivalence class, like 314/316/317/319/368/371/372 (and that's it among 3-digit equations) ... which are all otherwise distinct classes.

[Alex Meiburg]

Working on this, I got a PR. Based on what @Will Sawin suggested, I have separate notions of "definable" -- which includes kind of silly cases like x*y = x being definable from _anything_ -- and "structural", meaning that there's an operation that captures all of the information of the magma in an equivalent way. And then there's the distinction between FO-definable and term-definable (resp FO/term-structural). Where term-definable captures the notion of having an expression to spell it out.

Under this definition, the associative law (and commutative law) is structural for Equation 543: given the group operation x+y I can recover the 543-operation with the FO formula (-).graph = {(x,y,z) | x = y+z}. The associative law is also term-definable: I can define it as x+y := x-((x-x)-y), which is just a term. But it does not appear to be term-structural, as I currently have it defined, because there's no way to recover - from + with just a term. You would need the inverse operation. So - to + is a term, and + is structural, but the recovery map + to - can't be written as a term. Of course we could define "term-structural" differently without requiring this, but having it be terms both ways seemed most natural. And we can't go the other way. ... Right?

I've been thinking about it more and there's some more interesting subtleties going on here. When talking about how to define one operation from the other, one first talks about the realization of an operation in a magma, and then definability is always relative to a structure. There's two different ways to do this then:

• op1 is definable from op2 if, in every magma obeying op2, there's a FO formula that defines op1.
• op1 is definable from op2 if there's a FO formula such that, in every magma obeying op2, the formula defines op1.
  These are a different ordering of quantifiers (existential over formulas, and universal over magmas). They could in principle be different: it could be that an operation could always be recovered from the other by _some_ formula, but that formula is magma-dependent. That seemed kind of strange though and I didn't think it would happen, so I didn't worry about it.

[Terence Tao]

There might be a way to get uniformity in the FO formula for free. If there is no uniformity, then each FO formula will fail to obey op2 for some magma, and then by taking the direct product of all of these magmas one should be able to produce an (infinite) magma obeying op1 but for which op2 fails for every FO formula. (One may also be able to get this claim through the compactness theorem in model theory.)

[Alex Meiburg]

(cont. previous message)
But that kind of happens actually in this case with Equation 543 -- at least for finite magmas! In any finite magma obeying equation 543, we can recover the - operation from the +, with just a term, without needing an inverse operation. But that term depends on the magma! The + magma is an abelian group, and so (by looking at the order of the group and finding a number k that's congruent to -1 modulo all the unitary divisors) we can always write something like x-y = x+(y+y+y+y+y+y...).

So equation 543 is "term-structural" in this sense for finite magmas, but not for infinite magmas (like integer addition). But if we swapped the order of the quantifiers, it would no longer have this property for finite magmas either.

[Alex Meiburg]

Right, I think what you're saying is exactly the case. So I think when we include infinite magmas in the discussion these are equivalent, by compactness. But for finite magmas they can be different, at least in this sense of term-definability.

[Alex Meiburg]

While working on this some more, I found https://www.cs.unm.edu/~mccune/projects/gtsax/ which gives a single-axiom equation for not-necessarily-abelian groups:

x ◇ ((((x ◇ x) ◇ y) ◇ z) ◇ (((x ◇ x) ◇ x) ◇ z)) = y.

it has 8 operations. On that page, they explain that they searched and showed there was no axiom for groups on 6 operations or smaller ... their wording (going up in length=ops+vars in units of 4, instead of 2) implies that there's a reason why a minimal axiom can't be on 5 or 7 operations, but the reasoning isn't clear to me.

[Bruno Le Floch]

Alex Meiburg said:

[...] why a minimal axiom can't be on 5 or 7 operations, but the reasoning isn't clear to me.

If the operation is $x\diamond y=xy^{-1}$, then the number of each variable has to be even for the identity to be correct in the group with 2 elements (say), and the positions of the variables is also quite constrained to make the identity correct in more general groups.

[Alex Meiburg]

Oh right, that makes sense. Thanks

[Alex Meiburg]

The self-distributive axiom(s) of a rack is a 5-operation equation that is also structurally implied by a group structure: x ◇ y := x * y * x⁻¹. The rack equation (written for left-oriented racks) is

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

The dual of this equation is for "right" racks. A rack is given by an operation that (1) obeys this is equation and (2) the function (x ◇ ⬝) is a bijection for all x.

This is trivial for abelian groups though (it becomes the right-projection magma). But, there's a different natural rack given by x ◇ y := x * y⁻¹ * x, which is nontrivial on abelian groups (iff the group is not of exponent 2). These are called the Conj and Core quandles. These are also some nice equations we could include; I will want to have them to show that they are definable from the group axioms above, but I think they're of good interest otherwise too.

In particular I wonder if there's a single-equation definition of a rack (or quandle)

[Bruno Le Floch]

A putative single-equation for racks needs to have one side without operation (an LHS of $x$): if it has $\diamond$ on both sides, then the equation is satisfied by $x\diamond y=c$ for some constant element $c$, which violates the bijectivity axiom of racks. It has to have at least three variables, both appearing at least twice in total. In fact the counting of variables is quite constrained in order for the equation to be obeyed both by $x\diamond y=y$ and $x\diamond y=2x-y$ in the group $\mathbb{Z}$. Consistency for the first operation requires the right-most letter in the equation to be $x$. Consistency for the second operation requires the number of each variable, weighted by a factor of $2$ when it appears as the left operand of $\diamond$ and $-1$ on the right, to be the same on the LHS and RHS. By hand, I think the only four-operation equations obeying these counting conditions are

x = y◇(y◇(z◇(z◇x))) equation 528
x = y◇(z◇(z◇(y◇x))) equation 575
x = y◇((z◇(z◇y))◇x) equation 1184
x = (y◇z)◇((y◇z)◇x) equation 1780
x = (y◇(y◇z))◇(z◇x) equation 1949

These are consequences of equation 16, $x=y\diamond(y\diamond x)$ obeyed by the operation $x\diamond y = xy^{-1}x$ in non-abelian groups, but they are not obeyed by conjugation in non-abelian groups.

In fact, looking at equations with LHS $x$ and up to 6 operations I don't see any that is obeyed by both $x\diamond y=xy^{-1}x$ and by conjugation. There may be a simple argument for why it is impossible. Actually, I don't see how to get all copies of the variables $y,z$ to disappear when expanding any RHS: there is always $y$ to the left of $y^{-1}$ with some other variables in between.

Maybe a more promising idea would be to go the way of the Tarski axiom and define an auxiliary operation combining $x\lhd y$ and $x\rhd y$, but I failed.

[Alex Meiburg]

I think x needs to appear somewhere other than just the LHS and right edge of the RHS. If you have a valid axiom, then as you expand out

x = w1 ◇ (w2 ◇ ... (wn ◇ x))

where wi are some other words, you'll end up with either x = [something involving w_i's] x⁻¹ [something involving w_i's] or x = [something involving w_i's] x [something involving w_i's] depending on how deep it was. In the free (non-abelian) group, this clearly can't hold unless x is also in one of the w_i's.

[Alex Meiburg]

Actually, yeah, by looking at the Core rack (the x ◇ y := x * y⁻¹ * x) on the free non-abelian group on infinitely many generators, you get the really hard limitations. Because if x only occurred at the end, you could always take x to be a fresh symbol with no relations to any of the y, z, w... that you're otherwise using.

[Alex Meiburg]

The first [something] becomes S1 = w1 * w2⁻¹ * w3 * w4⁻¹ ... w2k⁻¹ for some k (since it must be even depth). The second one is instead backward: S2 = w2k⁻¹ ... w4⁻¹ * w3 * w2⁻¹ * w1. The w's themselves are not reversed, though.

Then we have the constraint that x = S1 * x * S2.

[Alex Meiburg]

For the Conj rack, it's a similar story but instead S3 = w1 * w2 * w3 * w4 ... w2k and S4 = w2k⁻¹ ... w4⁻¹ * w3⁻¹ * w2⁻¹ * w1⁻¹, and the constraint is x = S3 * x * S4 again.

We need words wi in the free group that satisfy these equations for all x, y, z (and possibly other variables in place). Satisfying it for the free group is obviously enough then to make it work for Conj and Core on any group. (It doesn't mean it's a legitimate rack, though, there are racks which don't arise this way.) Note that these words wi will be different between the Core and Conj racks, unless they're atoms (variables by name).

[Alex Meiburg]

Oh .. actually! We can see that S1 = S2 = id is a necessity. Proof:

In Core[free group], all words produced by the rack operation are symmetric. (This is obvious by induction). So then the reversal of S2 really is S1, not just the word-wise reversal. Write S1 as a word in the free group on its variables (x, y, z etc.) in its reduced form. Our equation is that x = S1 * x * [Reversal of S1]. We can write S1 in the form S1 = S0 * x^n for some integer n, and S0 doesn't end in in x or x⁻¹. Then it's x = S0 * x^(2n+1) * [Reversal of S0], and since S0 doesn't end in x's, the the right hand side is already in its reduced form. Thus S0 = id and n = 0.

[Alex Meiburg]

A similar argument applies in Conj[free group]. Now S4 = S3⁻¹, so - writing S3 = S0 * x^n - we have x = S0 * x^n * x * x^(-n) * S0⁻¹. This simplifies to x = S0 * x * S0⁻¹. In the free group, this means that S0 must be the identity. So the only difference in Conj is that the words can evaluate to something that involves any power of x's.

[Alex Meiburg]

This would be easier to reason about if we need what the free rack looked like, because not all racks arise as Conj or Core.

A quick google tells me that we know what the free rack is: https://ri.conicet.gov.ar/bitstream/handle/11336/12170/CONICET_Digital_Nro.6651_A.pdf?sequence=2

Let X be a non empty set and let F (X) be the free group on X. The free rack R(X) on X always exists, and it is the set X × F (X) endowed with the rack operation

(x, α) ◇ (y, β) := (y, β * α⁻¹ * x * α)      for x, y ∈ X, α, β ∈ F (X).

The map f : X → R(X) is given by f(x) = (x, 1).

(Note that I switched the notation in the statement from the paper, because their racks go left instead of right.)

[Alex Meiburg]

Ah, okay, this has led me to a simple proof that there can't be a one-equation definition of racks in terms of the rack operation.

Proof: Define a rack on ℕ+ × ℤ as

(p, x) ◇ (q, y) := (q, y+p)

It's easy to verify that this is a rack. But also, x ◇ y is always strictly greater than y under the lexicographic ordering. We already established that any single axiom would need to have the form

x = w1 ◇ (w2 ◇ ... (wn ◇ x))

where w_i's are some other expressions (possibly variable names, possibly tree). But if we evaluate any expression of the form

w1 ◇ (w2 ◇ ... (wn ◇ x))

this will be strictly greater than x, so this cannot possibly equal x.

So any single-equation theory would have to be in terms of some other operation.

It's still possible that there's a single-equation theory of quandles (which include Core and Conj).

[Alex Meiburg]

Alright, sounds like the free quandle is basically just the conjugacy quandle on the free group. Okay, for Conj we had that

S3 = w1 * w2 * w3 * w4 ... w2k

where w_i's are some expressions in terms of our variables, this is multiplication in the free group, and a necessary and sufficient condition is that S3 evaluates to x^n for some n. If that's true, it's also true when we abelianize the group. In the abelianized group, the quandle operation is just x ◇ y = y though, so all of the wi's are just going to evaluate to their rightmost variable. In particular, this means that they must all be expressions with x as their rightmost element. So an equation like

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

could be okay, because the two words w1 := (z◇(y◇(z◇x))) and w2 := ((x◇y)◇x) both end in x. But

x = y◇(y◇x)

couldn't be okay, because the words w1 := y, w2 := y don't end in x.

So, each wi is a word in the free group that abelianizes to x. But any word coming from Conj takes the form T s T⁻¹ where s is the rightmost symbol in the quandle expression. So then we have

S3 = (T1 * x * T1⁻¹) * (T2 * x * T2⁻¹) * ... (Tn * x * Tn⁻¹) = x^n

This is clearly only possible in the free group if all of the Ti's are equal to the identity. So really, each w_i is equal to x, exactly.

[Alex Meiburg]

So if (suppose) we had some putative equation like

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

this would mean that when we evaluate w1 := (z◇(y◇(z◇x))) or w2 := ((x◇y)◇x)) in Conj, it must simplify to x for both of them.

But now we've reached a circle, a contradiction. Because x = w1 ◇ (w2 ◇ x)was the kind of equation we were originally reasoning about, saying that the right hand side has to evaluate to just x in the free group. But now we're shown that w1 also takes the form like w3 ◇ (w4 ◇ x) and evaluates to just x in the free group. So, by induction, _all_ variables in the equation must be x. But this cannot be true because it must be at least a two-variable equation.

So, this proves there is also no single-equation description of quandles, in terms of the quandle operation. It would have to be in terms of some other function. :tada:

[Alex Meiburg]

Progress on the PR for the original 543 -> Group statement. Most of the FO-logic boilerplate is done at least

[Bruno Le Floch]

Some inconclusive thoughts on operations built from the rack operation. Consider the rack operations x⊲y and y⊳x (unique element such that x⊲(y⊳x)=y). Consider a binary operation x◇y=(any tree in ⊲ and ⊳ involving only x,y) that is not reduced to x nor y by the rack axioms. I conjecture that this binary operation cannot satisfy any equation of the form x=(tree in ◇ involving any variables).

For any tree in ⊲ and ⊳ involving any number of variables, let me define the "central leaf" c=(one of the variables) as the result of evaluating the tree for the rack x⊲y=y and y⊳x=y. For instance, the central leaf of (x⊲(y⊳z))⊲((w⊳u)⊳v) is w.

Consider next the conjugacy rack (which is a quandle) of a general group, namely x⊲y=xyx⁻¹ and y⊳x=x⁻¹yx. Then all trees in ⊲ and ⊳ in any number of variables evaluate to expressions of the form (word)c(word)⁻¹, where c is the central leaf of that tree and word is a word in the variables. Without loss of generality we can assume that the central leaf of x◇y is y. Then x◇y = f(x,y) y f(x,y)⁻¹ where f can be an arbitrary word depending on the definition of ◇. The putative equation on ◇ must thus take the form x=w1◇(w2◇...(wn◇x)) as in your posts. In the conj rack we must have

f(w1,w2◇...(wn◇x)) ... f(wn,x)=1

(equation in the underlying group). Here, each wi is a tree in ◇, and thus it evaluates to (word)ci(word)⁻¹ for some central leaf ci. In particular its overall degree in the variables x,y,... is 1, so all arguments of f that are involved in the equation are of degree one. Thus, we need f(a,b) to be of degree zero in a,b, for instance f(a,b)=ab⁻¹.

[Bruno Le Floch]

Alex Meiburg said:

https://www.cs.unm.edu/~mccune/projects/gtsax/ which gives a single-axiom equation for not-necessarily-abelian groups:

x ◇ ((((x ◇ x) ◇ y) ◇ z) ◇ (((x ◇ x) ◇ x) ◇ z)) = y.

As far as I can tell this is equation 42323216 x = y ◇ ((((y ◇ y) ◇ x) ◇ z) ◇ (((y ◇ y) ◇ y) ◇ z)).

[Terence Tao]

I've added this to the tour.

[Bruno Le Floch]

Thanks. In "Equation 345169 x = y ◇ ((x ◇ y) ◇ y) ◇ (x ◇ (z ◇ y)): the Sheffer stroke law", parentheses are missing around the first four variables of the RHS. I got worried for a minute that my code was wrong.

[Terence Tao]

Corrected, thanks. (So much of mathematics is associative that it takes real effort to remove that as the default working assumption in one's notation.)

[Alex Meiburg]

I've been continuing work on formalizing this in Lean. So far the main results I've written up are:

• Implication (the main effort of the equational theories project) implies these other four notions, the strongest one being "term-structural" and the weakest being "first-order definable" (or just, definable).
• Equations are always term-structural in terms of their duals, so duals are equivalence classes.
• Associative and commutative laws are term-definable, and first-order structural, for equation 543 (which is in turn implied by a number of other laws).
• The constant law is term-definable from any law of the form f(x,y) = f(z,w) -- or likewise, with any number of disjoint variables on the left and right hand side. For instance, equation 4336 x ◇ (y ◇ x) = z ◇ (w ◇ z) lets you define a constant law as x * y := x ◇ (y ◇ x). Since these laws are also implied by the constant law, this leads to a sizable collapse into an equivalence class.
• The commutative law is term-definable from any law of the form f(x,y) = f(y,x). One could state this more generally for any equation of the form e.g. f(x,y,w) = f(y,x,z) or f(x,y,x) = f(y,x,z), but these imply the corresponding equation f(x,y) = f(y,x), so we don't need to explicitly do that. As one example, equation 4321 x ◇ (y ◇ x) = y ◇ (x ◇ y) yields the commutative law as x * y := x ◇ (y ◇ x).
• I would also like to check Eq42323216 x = y ◇ ((((y ◇ y) ◇ x) ◇ z) ◇ (((y ◇ y) ◇ y) ◇ z)) (for non-abelian groups), if it's easily implied by any of our <4-op laws, since that gives an associative law (and a constant law). That would probably be a computer search.

In terms of non-implications, where first-order definability is strongest:

• Obviously if equation A has models of size k and equation B does not, then B is not definable from A.
• First-order defining an equation commutes with automorphisms of the original magma. So if a magma on type M obeying equation A has an automorphism φ : M -> M, but no magma on M obeying equation B obeys that automorphism, then B can't be definable from A.
• If B is structural from A, then they must have isomorphic automorphism groups, and the same number of magmas on any type.
  I haven't actually searched to try to find any examples of these. The first point should be the easiest to check, since I know we have data for the smallest nontrivial models of most (each?) equation. Is that data proved, though, and where can I find it?

Anyway, I hope to actually compute the transitive closure of those first implications tonight. I'm mostly curious to see how much the equivalence classes already collapse.

[Vlad Tsyrklevich]

Alex Meiburg said:

• Is that data proved, though, and where can I find it?

If you're talking about lean formalized, I don't believe it is. See data/smallest_magma*

[Alex Meiburg]

Thanks. Oh, and I forgot to mention, that the left (and right) projection laws are term definable from anything, so that also leads to several collapses.

[Bruno Le Floch]

@Alex Meiburg If I understand, (term/FO)-structural means that from an op1 obeying eq1 we (term/FO)-define an op2 obeying eq2. But there is a further distinction: does eq2 capture everything about eq1. For instance Tarski's 543 term-structurally produces a new operation x+y=x◇((y◇y)◇y) that obeys commutativity and associativity, has an identity and an inverse, but none of these equations alone imply that the subtraction is FO-definable and satisfies 543.

[Alex Meiburg]

Ah, no, that would be "definable". I'm using "structural" -- I don't think there's a standard term for this otherwise -- to mean:

Given a magma M with operation op1, there's a FO definition of op2 in terms of op1, so that (1) op2 obeys equation 2, and (2) op1 can be FO defined in terms of op2 again.

[Alex Meiburg]

It's intended exactly to be the 'capture everything about eq1' that you describe.

[Alex Meiburg]

So for instance, from equation 4321 with op1 obeying x ◇ (y ◇ x) = y ◇ (x ◇ y), we can define op2 as x * y := x ◇ (y ◇ x) and this will satisfy the commutative law. But we can't in general recover from op1 from op2, so this isn't "structural", it's just commutativity is "definable" from 4321.

But, as in 543, the commutative/associative operations op2 x+y=x◇((y◇y)◇y) has enough to FO-recover the original 543 op1, so that's structural.

As a sort of more trivial example, the associative law is also structural from the constant law. If I have an op1 obeying x◇y = w◇z, then defining op2 as x*y := x◇y(so, the same operation) gives an associative law. And obviously op1 can be recovered from op2 then, so this is structural. This is a consequence of the fact that the constant law implies the associative law. This is a specific example of the general theorem, that implication of laws implies structurality(?) of laws.

[Bruno Le Floch]

I had understood that but misspoke (miswrote?) badly. What I meant is that your notion of structural does not capture everything about eq1, but rather everything about op1. Namely I remark that the functor from the category Magma(543) to the category of commutative-associative magmas is injective, but not surjective. Equation 543 on ◇ is more constraining than commutativity and associativity of x+y=x◇((y◇y)◇y). What I propose is close to asking for F0-structural in both directions, but that's not enough because of course the two functors don't have to be inverses of each other.

[Bruno Le Floch]

Another interesting example of term-definable-equivalence is that a magma obeying Equation 168 x = (y ◇ x) ◇ (x ◇ z), the central groupoid law, briefly described in the Tour can be turned into a different magma obeying the same equation by defining

x*y = ((x◇x)◇(y◇y))◇((x◇x)◇(y◇y))

This is actually an involution.

[Alex Meiburg]

Mm, I see. I think what you're talking about can be precisely stated as: given eq A and eq B, there is a definition of op2 in term of op1, so that op1 obeys eqA iff op2 obeys eqB.

That's symmetric so it's an equivalence relation. It's at least as strong as A and B being "structural" for each other, but could be stronger. It's stronger than the 543 thing because as you said it's not surjective (for instance, there are commutative semigroups).

I would be surprised if there are many instances this. There's equations that are duals, and equations that imply each other (in the usual sense of the project).

I guess if we had another single-equation axiom for abelian groups, that would be equivalent to 543.

[Bruno Le Floch]

Not only "another single-equation axiom", but it would have to be also another operation, and here is a proof that it cannot be (other than swapping x,y).

Proposition: the only binary operation that is term-definable in terms of the abelian group operations (identity, inverse, multiplication), and from which the group operations are term-definable is subtraction x◇y↦x-y (and of course x◇y↦y-x).

Conjecture: for non-abelian groups only (x,y)↦xy⁻¹ (and its obvious symmetries (x,y)↦y⁻¹x, (x,y)↦yx⁻¹, (x,y)↦x⁻¹y) are mutually term-definable to the group operations.

Term-definability means that the operation is x◇y=f(x,y) for some (reduced) word f in the free group with two elements. Since the group operations are term-definable in terms of ◇, then in any group G, the submagma 〈x〉 generated by any given element x and by ◇ coincides with the subgroup of G generated by x.

Abelian story. Taking G = Integers we have x◇y=kx+ly for some integers k,l. Obviously gcd(k,l)=1 lest ◇ can only term-define operations with values in multiples of gcd(k,l), which addition is not. Next, the submagma 〈1〉 generated by x=1 is contained in 1+(k+l-1)Z, so that we need k+l=2 or k+l=0 to reach all integers. In the first case k+l=2, if |k|>1, then x◇y=ly mod k, so that the reduction of 〈1〉 modulo k consists precisely of powers of l (coprime with k), which do not include zero, so that 〈1〉 does not include zero. Likewise if |l|>1, so we are left with k=l=1, but then 〈1〉 consists of all positive integers. In the second case k+l=0, we have gcd(k,l)=|k| so we need k=-l=±1, so the operation is subtraction (up to swapping arguments). Conclusion: among abelian groups, only subtraction works.

[Bruno Le Floch]

So all this is to say that you are probably right that such examples of structural equivalence are very rare. I suspect an example can be cooked up like the central groupoid one, but involving a mixture of squares and cubes, but it would be quite artificial.

[Alex Meiburg]

Why would it "have to" be another operation? If there was an equation equivalent to 543 (so that it also defines subtraction) would you not call that "structurally equivalent"?

Or are you just saying that would be uninteresting case of equivalence arising from equivalent equations

[Bruno Le Floch]

Alex Meiburg said:

Or are you just saying that would be uninteresting case of equivalence arising from equivalent equations

Yes, that is what I meant: it would simply be equivalence in the usual sense. I just saw that the Higman-Neumann mentions subtraction as being the only operation (in the abelian case) and leaves open the nonabelian case. It could be interesting to spend a bit of effort in this direction at some point, for instance to see if (x,y)↦x²y⁻¹x⁻¹ might work. Some cases can be excluded trivially because they do not reduce to subtraction in the abelian case, others can be excluded by reflection groups: for instance it is not possible to express group operations in terms of (x,y)↦xyxy⁻¹x⁻¹y⁻¹, because in the dihedral group generated by s,t with s²=t²=(st)³=1 the submagma generated by s,t is simply {1,s,t}. Presumably clever enough groups may be enough to rule out everything. A natural attempt is to consider the group with two generators s,t, subject to the relations $f(s^k,t^l),f(t^k,s^l) \in \{s^m,t^m\mid m\in\mathbb{Z}\}$ for all k,l, but it seems hard to make that general.

[Alex Meiburg]

Okay, with what I have so far, the "term definable" equations actually collapse into just _138_ equivalence classes from the original 4694. That's a small enough you could make a Hasse diagram a person could actually look at and take in! :)

[Alex Meiburg]

List of representatives from each class

1, 2, 14, 40, 43, 63, 66, 73, 115, 118, 125,
167, 168, 313, 332, 335, 464, 467, 474, 477, 481, 492,
501, 504, 508, 511, 543, 546, 556, 667, 670, 677, 680,
692, 695, 704, 707, 714, 870, 873, 880, 883, 887, 895,
898, 907, 910, 917, 978, 1073, 1076, 1083, 1086, 1110, 1113,
1117, 1276, 1279, 1286, 1289, 1313, 1316, 1323, 1479, 1480, 1482,
1483, 1485, 1486, 1489, 1492, 1496, 1516, 1519, 1523, 1526, 1682,
1685, 1692, 1695, 1719, 1722, 1729, 3269, 3272, 3279, 3342, 3345,
3350, 3352, 3355, 3364, 3417, 3472, 3475, 3482, 3545, 3548, 3555,
3558, 3588, 3601, 3607, 3620, 3675, 3678, 3748, 3751, 4273, 4290,
4293, 4295, 4297, 4303, 4305, 4321, 4325, 4343, 4364, 4369, 4386,
4405, 4408, 4411, 4413, 4415, 4421, 4423, 4443, 4458, 4461, 4482,
4485, 4497, 4531, 4535, 4541, 4544

[Alex Meiburg]

Size of each class

1 : 2075
2 : 1496
14 : 8
40 : 735
43 : 1
63 : 2
66 : 4
73 : 2
115 : 2
118 : 2
125 : 2
167 : 1
168 : 3
313 : 2
332 : 3
335 : 2
464 : 2
467 : 2
474 : 2
477 : 2
481 : 2
492 : 30
501 : 2
504 : 2
508 : 6
511 : 2
543 : 12
546 : 12
556 : 12
667 : 2
670 : 2
677 : 2
680 : 2
692 : 8
695 : 4
704 : 2
707 : 2
714 : 4
870 : 2
873 : 2
880 : 2
883 : 2
887 : 6
895 : 6
898 : 6
907 : 2
910 : 2
917 : 2
978 : 6
1073 : 6
1076 : 2
1083 : 2
1086 : 2
1110 : 2
1113 : 2
1117 : 2
1276 : 2
1279 : 2
1286 : 2
1289 : 2
1313 : 2
1316 : 2
1323 : 2
1479 : 2
1480 : 2
1482 : 2
1483 : 2
1485 : 2
1486 : 2
1489 : 2
1492 : 2
1496 : 2
1516 : 2
1519 : 2
1523 : 2
1526 : 2
1682 : 2
1685 : 2
1692 : 2
1695 : 2
1719 : 2
1722 : 2
1729 : 2
3269 : 2
3272 : 2
3279 : 2
3342 : 2
3345 : 2
3350 : 4
3352 : 2
3355 : 2
3364 : 8
3417 : 2
3472 : 2
3475 : 2
3482 : 2
3545 : 2
3548 : 2
3555 : 2
3558 : 2
3588 : 2
3601 : 2
3607 : 2
3620 : 3
3675 : 1
3678 : 2
3748 : 2
3751 : 1
4273 : 4
4290 : 2
4293 : 2
4295 : 6
4297 : 2
4303 : 6
4305 : 2
4321 : 2
4325 : 2
4343 : 2
4364 : 2
4369 : 2
4386 : 2
4405 : 1
4408 : 2
4411 : 6
4413 : 1
4415 : 1
4421 : 2
4423 : 2
4443 : 1
4458 : 1
4461 : 2
4482 : 1
4485 : 6
4497 : 1
4531 : 1
4535 : 5
4541 : 1
4544 : 1

[Amir Livne Bar-on]

What does it mean to be definable from Eq 1?

[Alex Meiburg]

So 44% end up being equivalent to equation 1, 31% end up being equivalent to equation 2, and 16% end up being equivalent to equation 40 x ◇ x = y ◇ y (the class also includes equation 46, the constant law).

Well, those percentages are lower bounds, it could be there are more collapses.

[Alex Meiburg]

It means that given _any_ operation, no matter what it's like, it's possible to write an operation that satisfies your equation. The main reason this collapse happens is the (left) projection law: x ◇ y := x can always be defined, no matter what. You don't need any information about the existing magma you're building off of.

And so then, any other equations that are implied by the left projection law (anything with the same first letter on LHS and RHS) work by this definition too, and end up also being definable.

[Alex Meiburg]

equational#761 finally has the actual proof that first-order definability is transitive (which is a thing that can hopefully get upstreamed to mathlib). That was a big sorry for quite a while. Was surprisingly hard and messy to prove!

(Actually longer than everything in mathlib4/Mathlib/ModelTheory/Definability.lean put together ... huh)

[Alex Meiburg]

With that, I think it should be ready to merge

[Terence Tao]

Just an observation that there is an additional flavor of definability: conditional definability, where one can define one operation in terms of another but only under an additional hypothesis. This showed up recently in https://leanprover.zulipchat.com/#narrow/channel/458659-Equational/topic/Austin.20pairs/near/483169215 where we figured out a way to turn a 503 magma into a 476 magma but only under the additional hypothesis of left-cancellability, which is available in finite magmas but need not hold in general.

[Alex Meiburg]

I saw that, I was thinking about whether that fits in cleanly one way or another. Of course any kind of implication could be extended to a 'conditional' version of implication, where we say for instance EqA & EqB -> EqC. And collecting all the two-equation conditions probably is too big to try to deal with, at least without some much larger automation.

But finiteness is certainly a nice kind of extra side condition, I think seeing it as an edge within the finite definability graph (as opposed to the general definability graph / finite implication graph) fits in better.

It's still a bit of a zoo! So we have "implication", "finite implication", and then these four different kinds of definability. All the kinds of definability have their own finite version. So we have a Hasse diagram of 10 different Hasse diagrams, each of which is a refinement of their parents. :dizzy:

[Jose Brox]

Just sharing a nonassociative-algebras perspective on the subject/definitions of definability, etc.:

In the nonassociative algebras setting, the same (or very close) notion of term-definability is called admissibility: as you know, given an associative algebra $(A,+,\cdot)$, we can term-define a new operation $[x,y]:=xy-yx$, which makes $(A,+,[\cdot,\cdot])$ into a Lie algebra (satisfies anticommutativity and the Lie identity); and analogously, $x\bullet y:=xy+yx$ makes $(A,+,\bullet)$ a Jordan algebra (satisfies commutativity and the Jordan identity). Accordingly, Albert called any nonassociative algebra $(A,+,\cdot)$ Lie-admissible if $[x,y]:=xy-yx$ endows $(A,+)$ with a Lie algebra structure (here the operation is already chosen as the bracket to ensure anticommutativity). Analogously, Albert also defined Jordan-admissible algebras starting with the bullet product, and later Myung defined Malcev-admissible algebras starting with the bracket. For this reason, I call (e.g. in an unpublished preprint) admissibility to the following relation: given varieties of nonassociative (and related) algebras $V$ and $W$, $W$ is admissible in $V$ if there is a universal product $*$ (term-)defined from the product in $W$ such that $(A,+,*)\in V$ for any $(A,+,\cdot)\in W$ (e.g. $V=\text{Lie}$, $W=\text{Ass}$, $x*y:=[x,y]$).
Perhaps for varieties of magmas we want to also call this relation admissibility instead of definability?

A closely related notion, which could also interesting be to study in the project (but harder), is that of representability: [EDITED] given varieties $V, W$ of nonassociative (or related) algebras, $V$ is representable in $W$ if there is a univeral product $*$ (term-)defined from the product in $W$ such that for any $A\in V$ there is $(B,+,⋅)\in W$ such that $A$ is isomorphic to a subalgebra of $(B,+,∗)$.

Lastly, there is also the notion (that I also generalize from the Lie, Jordan, and Malcev settings) of speciality. Note that representability doesn't ensure that $(B,+,*)\in V$ for all $B\in W$, only for some of them; speciality binds together the notions of admissibility and representability: $V$ is special in $W$ if there is a universal (term-)defined product $*$ in $W$ such that 1) all algebras in $W$ endowed with $*$ are algebras in $V$, and 2) moreover any algebra in $V$ can be seen as a subalgebra of some algebra in $W$ endowed with $*$ (e.g., Lie algebras over fields are special in associative algebras via the universal enveloping algebra, but Jordan algebras are not since the Albert algebra is exceptional, i.e., not representable in an associative one via the bullet product).

[Jose Brox]

In addition, I have just found out that in the universal algebra setting, term-definability is called interpretability. This is an excerpt from the AMS memoir The lattice of interpretability types of varieties:

Interpretability excerpt.JPG

Facts already mentioned above seen in this light: the varieties of sets and semigroups are equi-interpretable (any set with $xy = x$ is a semigroup), any variety interprets in the variety of trivial algebras ($x=y$), etc.

[Bruno Le Floch]

In this language, how do you view the following fact: a magma obeying Eq 313 x*x = y*(x*y) has a submagma (the set of squares) obeying Eq 14 x=y*(x*y) (and also x=x*x in this submagma).

[Alex Meiburg]

Thanks for the references+context, Jose! So I guess admissibility would be another word for term-definable? The word "term-definable" does exist in literature but only a tiny handful of uses, so it's not really standard by any means.

For speciality, is there a reason you only require that V is a subalgebra of some W, as opposed to the whole algebra? Representability, as you wrote it, doesn't seem to have that aspect...

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

I must admit, I would feel a bit uneasy if the main Equational Theories Project publication announced findings on term-equivalence and related matters surrounding models of our 4684 equations, unless we can get input from an expert in universal algebra ahead of time.

From what I understand, term-equivalence belongs firmly in the set of problems that classical universal algebra has traditionally devoted significant effort to addressing, and where various well-established, sophisticated tools might be available. Tame Congruence Theory (polynomial equivalence, a weaker notion, features heavily) and a whole bunch of techniques introduced to resolve the CSP Dichotomy Conjecture come to mind.

Without engaging thoroughly with this body of work, there's a risk of producing a bunch of results that miss obvious simplifications that experts in the field would recognize, or do something that seems needlessly complicated to conclude something that's obvious in light of the existing literature. Reviewers with expertise will surely be unhappy if it appears to them that a bunch of physicists, logicians, and other "outsiders" have rediscovered concepts addressed more effectively in their literature decades ago. Fair or not, this would not reflect well on the project.

[Jose Brox]

Alex Meiburg ha dicho:

For speciality, is there a reason you only require that V is a subalgebra of some W, as opposed to the whole algebra? Representability, as you wrote it, doesn't seem to have that aspect...

Oops, I tried to simplify the representability definition and I ended oversimplifying it: $V$ is representable in $W$ if there is a univeral product $∗$ (term-)defined from the product in $W$ such that for any $A\in V$ there is $(B,+,⋅)\in W$ such that $A$ is isomorphic to a subalgebra of $(B,+,∗)$ (what I had in mind for the simplication was taking the smallest $W$-algebra generated by $A$ inside $B$, but this does not work). I'm editing above, thank you!