Tour of selected equations - teorth/equational_theories GitHub Wiki
1 x = x
: the trivial law
Equation This is the weakest law, satisfied by all magmas. No other law is equivalent to this law.
2 x = y
: the singleton law
Equation This is the strongest law, satisfied only by the trivial magmas: the singleton and empty magmas. Many laws are equivalent to this law; informally, they are so ``overdetermined'' that they can only be satisfied by trivial magmas. In fact, from our list of 4694 laws, exactly 1495 other laws are equivalent to this one.
14 x = y ◇ (x ◇ y)
, 29 x = (y ◇ x) ◇ y
: 2001 Putnam laws
Equations Problem A1 of the 2001 Putnam asked to show (in our language) that Equation 14 implies Equation 29. In fact, the two laws are equivalent. (Idempotent) magmas obeying the Putnam laws are equivalent to a directed version of a Steiner triple system, known as a Mendelsohn directed triple system.
43 x ◇ y = y ◇ x
: the commutative law
Equation One of the most famous laws in all of algebra.
46 x ◇ y = z ◇ w
: the constant law
Equation A very strong law, that makes the entire multiplication table constant.
65 x = y ◇ (x ◇ (y ◇ x))
"Asterix", and 1491 x = (y ◇ x) ◇ (y ◇ (y ◇ x))
"Obelix"
Equations A surprisingly subtle pair of equations to analyze, see this discussion. The "Asterix" equation implies the "Obelix" equation for finite magmas, but not for infinite ones; similarly for the converse implication. The analysis of this pair led us to develop "greedy" methods for constructing counterexamples, which has turned out to be a fruitful and flexible approach that (after suitable modifications) resolved many other challenging implications.
168 x = (y ◇ x) ◇ (x ◇ z)
: the central groupoid law
Equation This law defines central groupoids, which are magmas with some interesting combinatorial structure. For instance, all finite central groupoids have a cardinality that is necessarily a square number. This paper of Knuth establishes many of the basic properties of these objects.
381 x ◇ y = (x ◇ z) ◇ y
, 3722 x ◇ y = (x ◇ y) ◇ (x ◇ y)
, 3744 x ◇ y = (x ◇ z) ◇ (w ◇ y)
: 1978 Putnam laws
Equations Problem A4 of the 1978 Putnam asked to show (in our language) that Equation 3744 implies Equations 3722 and 381. This Putnam question referred to 3744 as a "bypass law".
387 x ◇ y = (y ◇ y) ◇ x
: a law from MathOverflow
Equation This response by pastebee to a MathOverflow question established that there was an equational law strictly between the constant law 46 and the commutative law 43, namely Equation 387.
477 x = y ◇ (x ◇ (y ◇ (y ◇ y)))
: a confluent law
Equation This law is a non-trivial example of a confluent law: a law in which every word has a unique shortest reduction using the law. This makes it possible to easily determine which other equations are implied by this law, giving anti-implications that were not obtainable by other means. See this discussion.
543 x = y ◇ (z ◇ (x ◇ (y ◇ z)))
: Tarski's axiom
Equation In 1938, Tarski showed that this law describes abelian groups: a magma obeys this law if and only if it has the structure of an abelian group, for which the magma operation is given by subtraction: x ◇ y = x - y
.
854 x = x ◇ ((y ◇ z) ◇ (x ◇ z))
: A "liquid" law.
Equation Most laws tend to feel either "solid", in that their models have a lot of algebraic structure (or are forced to be almost trivial), or "gaseous", in that there is extensive freedom in their models, and little structure. This law is at an unusual intermediate state, that one might call "liquid". One the one hand, it implies many other laws and its models have intriguing structure, including a an associated directed graph and pre-order. Its free magma, while difficult to describe, does obey some interesting laws, such as a unique factorization property that can already be used to refute some implications. On the other hand, there are many sporadic solutions, including a specific example of order 12 that was discovered through an ATP and could also refute implications. Furthermore, given a finite magma solving this law, it is often possible to extend it by adding one more element, in sharp contrast to say the situation with finite groups, creating quite a large class of additional examples of this law.
917 x = y ◇ ((y ◇ y) ◇ (x ◇ y))
"Hardy", 1729 x = (y ◇ y) ◇ ((y ◇ x) ◇ y)
"Ramanujan", and 2541 x = (y ◇ ((y ◇ y) ◇ x)) ◇ y
"Littlewood"
Equations Three closely related equations. They are known to be equivalent for finite magmas. For infinite magmas, Ramanujan implies Littlewood, but the other five implications between these laws are now known to be false (with rather sophisticated counterexamples in some cases).
1485 x = (y ◇ x) ◇ (x ◇ (z ◇ y))
: the weak central groupoid law
Equation A weaker form of the central groupoid law (Equation 168). Has some intriguing structure; for instance, all known finite examples have cardinality that is either a perfect square, or twice a perfect square, and such weak central groupoids can be associated to a directed graph obeying an intriguing axiom on its 5-cycles. A specific such example, of order 32, has led to the development of a "twisting semigroup" method that can rule out a small number of select implications. Discussed extensively here.
1571 x = (y ◇ z) ◇ (y ◇ (x ◇ z))
: a law for abelian groups of exponent 2
Equation It was shown by Mendelsohn and Padmanabhan that this law characterizes abelian groups of exponent 2.
1689 x = (y ◇ x) ◇ ((x ◇ z) ◇ z)
: a non-trivially singleton law
Equation This law was identified by Kisielewicz as a law that collapses to the singleton law 2, but all known proofs are surprisingly lengthy.
4512 x ◇ (y ◇ z) = (x ◇ y) ◇ z
: the associative law
Equation One of the most famous laws in all of algebra.
3588 x ◇ y = z ◇ ((x ◇ y) ◇ z)
, 3994 x ◇ y = (z ◇ (x ◇ y)) ◇ z
: An Austin pair
Equations It was shown as part of this project that 3944 and 3588 form an "Austin pair": Equation 3944 implies Equation 3588 for finite magmas, but not for infinite magmas.
x = y ◇ (y ◇ (y ◇ (x ◇ (z ◇ y))))
: A conjectural Austin law
Equation 5093 An Austin law is a law which has infinite models, but no non-trivial finite models (equivalently, this law and the trivial law (Equation 2) form an Austin pair). Kisielewicz showed that this law has no non-trivial finite models, but it remains open whether there is an infinite model.
x = (y ◇ ((z ◇ x) ◇ w)) ◇ (x ◇ w)
: the natural central groupoid law
Equation 26302 It was shown by Knuth that this law characterizes "natural central groupoids", which, up to isomorphisms, are Cartesian squares S × S
with magma operation (a,b) ∘ (c,d) = (b,c)
. These are special cases of central groupoids (Equation 168).
x = (((y ◇ y) ◇ y) ◇ x) ◇ (y ◇ z)
: An Austin law
Equation 28770 Kisielewicz showed that this law is an Austin law: it has no non-trivial finite models, but it has an infinite model. He also showed there is no shorter Austin law.
x ◇ (y ◇ z) = (x ◇ y) ◇ (x ◇ z)
, 60491 (x ◇ y) ◇ z = (x ◇ z) ◇ (y ◇ z)
: Self-distributive laws
Equations 56085 These self-distributive laws arise in the theory of racks and quandles. Magmas obeying these laws are known as shelves, and their multiplication tables are known as Laver tables.
x = (y ◇ ((x ◇ y) ◇ y)) ◇ (x ◇ (z ◇ y))
: the Sheffer stroke law
Equation 345169 It was shown by McCune, Veroff, Fitelson, Harris, Feist, and Wos that this law defines the Sheffer stroke.
x = (((y ◇ y) ◇ y) ◇ x) ◇ ((y ◇ y) ◇ z)
: An Austin law
Equation 374794 It was shown by Kisielewicz that this law is an Austin law: it has no non-trivial finite models, but it has an infinite model.
x ◇ (y ◇ (x ◇ x)) = (x ◇ y) ◇ (x ◇ x)
: The second Jordan law
Equation 906021: The second law of a Jordan algebras. (The first is the commutative law, Equation 43.)
x ◇ (y ◇ (x ◇ z)) = (x ◇ (y ◇ x)) ◇ z
, 930594 x ◇ ((y ◇ z) ◇ y) = ((x ◇ y) ◇ z) ◇ y
, 914612 x ◇ (y ◇ (x ◇ z)) = ((x ◇ y) ◇ x) ◇ z
, 916037 x ◇ (y ◇ (z ◇ y)) = ((x ◇ y) ◇ z) ◇ y
, 936498 (x ◇ y) ◇ (z ◇ x) = (x ◇ (y ◇ z)) ◇ x
, 921941 x ◇ ((y ◇ z) ◇ x) = (x ◇ y) ◇ (z ◇ x)
: the Bol-Moufang axioms
Equations 910472 The first two equations 910472, 930594 are the axioms for left and right Bol loops (if one also assumes the loop axiom that an identity element exists). A Moufang loop is a loop that is both left Bol and right Bol; this is equivalent (for loops) to any one of the other four equations 914612, 916037, 936498, 921941 holding.
x = y ◇ ((((y ◇ y) ◇ x) ◇ z) ◇ (((y ◇ y) ◇ y) ◇ z))
: the Higman-Neumann axiom
Equation 42323216 This axiom characterizes division in a (not necessarily abelian) group, as was worked out by Higman and Neumannin in 1956. It is one of the shortest such axioms.