Implications between selected laws
We collect here some notable implications between the selected laws in Selected laws. By Birkhoff's completeness theorem, every implication can basically be established by a finite number of rewrites. In most cases, the sequence of rewrites is quite straightforward, and the implication is very easy, but we record some less obvious examples.
Theorem387 implies 43#
E387 \(({x \diamond y = (y \diamond y) \diamond x})\) implies E43 \(({x \diamond y = y \diamond x})\).
Proof
(From MathOverflow). By E387, one has the law
Specializing to \(y=x \diamond x\), we conclude
and hence by another application of E387 we see that \(x \diamond x\) is idempotent:
Now, replacing \(x\) by \(x \diamond x\) in (1) and then using (2) we see that
so in particular \(x \diamond x\) commutes with \(y \diamond y\):
Also, from two applications of (1) one has
Thus (3) simplifies to \(x \diamond y = y \diamond x\), which is E43.
Lean
Formalized as Subgraph.Equation387_implies_Equation43.
Sources
Uses 2
Theorem29 equivalent to 14#
E29 \(({x = (y \diamond x) \diamond y)})\) is equivalent to E14 \(({x = y \diamond (x \diamond y))})\).
Proof
By Duality of laws it suffices to show that E29 implies E14. From E29 one has
and also
giving \(x = y \diamond (x \diamond y)\), which is E14.
Lean
Formalized as Subgraph.Equation29_implies_Equation14.
Sources
Uses 3
This result was posed as Problem A1 from Putnam 2001.
The proof of 29 equivalent to 14 is shown with its statement.
Theorem14 implies 29#
Uses 2
This result was posed as Problem A1 from Putnam 2001.
The proof of 14 implies 29 is shown with its statement.
The following result was Problem A4 on Putnam 1978.
Theorem3744 implies 3722, 381#
E3744 \(({x \diamond y = (x \diamond z) \diamond (w \diamond y)})\) implies E3722 \(({x \diamond y = (x \diamond y) \diamond (x \diamond y)})\) and E381 \(({x \diamond y = (x \diamond z) \diamond y})\).
Proof
By hypothesis, one has
for all \(x,y,z,w\). Various specializations of this give
(5) gives E3722, while (4), (5), (6) gives
which is E381.
Lean
Formalized as Subgraph.Equation3744_implies_Equation3722, Subgraph.Equation3744_implies_Equation381.
Sources
Uses 3
Theorem1689 is equivalent to 2#
Proof
The implication of E1689 from E2 is trivial. The converse is a surprisingly long chain of implications; see pages 326–327 of (Kisielewicz 1997). With some computer assistance, we found the following human-readable proof. We denote \(y^1=y\) and \(y^{n+1}=y^n\diamond y\) for \(n\geq 1\). We also introduce the notation
The initial equation states \(x = (y \diamond x) \diamond f(x,z)\). Our main step will be to prove that for all \(t\in M\) there exists \(w\in M\) such that \(f(t,w) = t\). The rest of the proof is then straightforward. Indeed, the initial equation gives \(t = (y \diamond t) \diamond f(t,w) = (y \diamond t) \diamond t = f(y,t)\) for any \(t,y\in M\). With such a simple expression of \(f\) the initial equation becomes \(x = (y \diamond x) \diamond z\), which easily implies the singleton law, for instance by writing \(x = ((y \diamond w) \diamond x) \diamond z = w \diamond z\) for any \(w,x,y,z \in M\).
There remains to prove \(f(t,w) = t\) for a well-chosen \(w \in M\), explicitly, \(w=g(t,t^5)=t\diamond t^7\). For any \(t,u,v \in M\), the combinations \(x = f(t,u)\) and \(y = v \diamond t\) satisfy \(y \diamond x = t\). Inserting these values into the initial equation yields the identity
Specialize to \(z=f(u,v)\) and note that \(f(t,u) \diamond z = (\cdots \diamond u) \diamond f(u,v) = u\) by the initial equation so that \(f(f(t,u),z) = (f(t,u) \diamond z) \diamond z = u \diamond z = g(u,v)\). Inserting this into (7) yields
On the one hand, (7) with \(z=u=t\) states that \(t^3 = t \diamond t^5\), so (using \(f(t^n,t)=t^{n+2}\))
and (8) with \((u,v)=(t^3,t)\) then implies \(f(t,t^3) = t \diamond g(t^3,t) = t \diamond f(t,t^5) = g(t,t^5)\). On the other hand, (8) with \((u,v)=(t,t^5)\) implies \(t^3 = t \diamond g(t,t^5)\). We deduce
Lean
Formalized as Subgraph.Equation1689_implies_Equation2, Subgraph.Equation2_implies_Equation1689.
Sources
Uses 2
The following result was established in (Mendelsohn and Padmanabhan 1975).
TheoremConsequences of 1571#
Magmas satisfying E1571 \(({x = (y \diamond z) \diamond (y \diamond (x \diamond z))})\) also satisfy E2662, E40, E23, E8, E16, E14, E43, and E4512, and are in fact abelian groups of exponent two. Conversely, all abelian groups of exponent two satisfy E1571.
Proof
Suppose that a magma \(G\) satisfies E1571, thus
and
whence
which is E2662. This gives
while from (9) one has
whence
This implies that \((x \diamond y) \diamond (x \diamond y)\) does not depend on \(x\), or on \(y\), hence is equal to some constant \(e\):
From (9) the magma operation is surjective, hence
which gives E40. Applying (9) with \(x=y=z\) we conclude
while if we instead take \(y=z=e\) we have
hence
and then also
from which we readily conclude E23, E8; thus \(e\) is an identity element. From (9) with \(z=e\) we now have
which is E16. If instead we take \(y=e\) we have
which is E14. So if we substitute \(z = x \diamond y\) and use (11) we obtain
and hence
thanks to (12). This gives E43, thus \(G\) is now commutative. From (9) once more one has
which one can simplify using commutativity and (11) (or (12)) to eventually obtain
which is E4512. \(G\) is now commutative and associative, and every element is its own inverse and of exponent \(2\), hence is an abelian group thanks to (10), so \(G\) is an abelian group of exponent \(2\) as claimed. The converse is easily verified.
Lean
Formalized as Subgraph.Equation1571_implies_Equation2662, Subgraph.Equation1571_implies_Equation40, Subgraph.Equation1571_implies_Equation23, Subgraph.Equation1571_implies_Equation8, Subgraph.Equation1571_implies_Equation16, Subgraph.Equation1571_implies_Equation43, Subgraph.Equation1571_implies_Equation4512.
Sources
Uses 9
Theorem953 is equivalent to 2#
Proof
It suffices to show that E953 implies E2. Pick an element \(0\) of \(G\) and define \(1 = 0 \diamond 0\) and \(2 = 1 \diamond 1\) (we do not require \(0,1,2\) to be distinct). From E953 with \(x=z=0\) we have
If we then apply E953 with \(z=1\) we conclude that
for all \(x,y\), from which one concludes \(x=x'\) for any \(x,x' \in G\), giving E2.
Lean
Formalized as Subgraph.Equation953_implies_Equation2.
Sources
Uses 2
TheoremSheffer stroke axiom#
Definition E345169 \(({x = (y \diamond ((x \diamond y) \diamond y)) \diamond (x \diamond (z \diamond y))})\) axiomatizes the Sheffer stroke operation \(x \diamond y = \overline{xy}\) in a Boolean algebra.
Proof
See (McCune et al. 2002). In fact this is the shortest law with this property.
A sketch of proof follows. One can easily verify that the Sheffer stroke operation satisfies this law. Conversely, if this law holds, then automated theorem provers can show that the three Sheffer axioms
are satisfied. A classical result of Sheffer (Sheffer 1913) then allows one to conclude.
Lean
Formalized as Sheffer.Equation345169_is_Boolean.
Sources
A natural central groupoid is, up to isomorphism, a magma with carrier \(S \times S\) for some set \(S\) and operation
These are examples of central groupoids, E168 \(({x = (y \diamond x) \diamond (x \diamond z)})\).
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.