Jordan identity

Stream: Equational

[Jose Brox]

For the extended equations, it may be interesting to add the (second) Jordan algebras axiom (the first one is commutativity of the product):

$(x ◇ y) ◇ (x ◇ x) = x ◇ (y ◇ (x ◇ x))$

I tend to use it sometimes. For example, I have checked that 1323 with identity element, partial commutativity ($y^2x = xy^2$) and Jordan identity satisfies 2744 (with Prover9).

[Shreyas Srinivas]

Isn't this trivially true for non-commutative but associative operations?

[Jose Brox]

Yes, of course: the Jordan identity is a consequence of the associative identity.

[Terence Tao]

What is the equation number of this axiom?

[Vlad Tsyrklevich]

EDIT: I believe the original number was wrong.

[Vlad Tsyrklevich]

$ grep -n "x ◇ (y ◇ (x ◇ x)) = (x ◇ y) ◇ (x ◇ x)" data/eq_size6.txt
906021:x ◇ (y ◇ (x ◇ x)) = (x ◇ y) ◇ (x ◇ x)

I confirmed a few of the other order 6 equations to verify that this method returned consistent results with what we already have. Previously I had some spurious newlines at the top of my local file

[Terence Tao]

I've added it to the tour page at https://github.com/teorth/equational_theories/wiki/Tour-of-selected-equations . Anyone interested is also welcome to PR a commentary file, though currently I don't think commentary for extended equations is actually implemented.

[Ibrahim Tencer]

I also thought of this in the context of 1323, it's how I figured power associativity was possible.

[Amir Livne Bar-on]

Vlad Tsyrklevich said:

$ grep -n "x ◇ (y ◇ (x ◇ x)) = (x ◇ y) ◇ (x ◇ x)" data/eq_size6.txt
906021:x ◇ (y ◇ (x ◇ x)) = (x ◇ y) ◇ (x ◇ x)

This checks out with the find_equation_id.py script