A single axiom for Boolean algebra

Stream: Equational

[Stanley Burris]

Stephen Wolfram posted a lengthy article on January 9, 2025 stating that on January 29, 2000 he was the first to discover a single magma axiom for Boolean algebra, namely
((a•b)•c)•(a•((a•c)•a)) = c
and proved it is the shortest possible.

There are lots of diagrams and statistics in the paper, and a discussion of implications for the philosophy and future of mathematics at the end. He used what is now the software FindEquationalProof (in Wolfram Language) to find the axiom.

[David Michael Roberts]

Perhaps of interest for Equational is that if one assumes that the magma operation is commutative (p•q=q•p) then there is a four-operation axiom (p•q)•(p•(q•r))=p that gives Boolean algebra.

[David Michael Roberts]

(Search for "Not long after, I found two 2-axiom systems, also with 6" here)

[Bruno Le Floch]

Thanks! It's a bit hard to disentangle references. The technical report by McCune, Veroff from June 2000 states (where I've inserted our equation number for reference).

Stephen Wolfram recently brought to our attention [6] a set of 25 Sheffer identities, all of length 15 with 3 variables, that he was investigating as being possible single axioms. [...] [Equation 329857] is a member of Wolfram's set of 25 Sheffer identities.

This suggests that Wolfram had identified this as a candidate (in particular as holding for the Sheffer stroke I suppose), but not necessarily that he had proven the equivalence.

[Bruno Le Floch]

In his notes about Chapter 12 section 9 of his book A New Kind of Science, Wolfram gives a list of 25 identities which I suppose coincide with the set given to McCune and Veroff. In these notes he mentions being able to prove equivalence for two of the identities "given as (g) and (h) in the main text", but I don't have access to the main text to determine which two equations it is.

• Law 329857 is proven to work by McCune and Veroff June 2000.

• Law 321577 is stated to work in Wolfram's recent blog post.

• Quick experiments with Mace4 provide non-commutative models of 321594, 321638, 321672, 329874, 333912, 334066, so that these laws are too weak.

• For the remaining 17 (317437, 317438, 317531, 317532, 321560, 321564, 321568, 321642, 321646, 321655, 329952, 333907, 333924, 333929, 333946, 333984, 334061), I don't know, I'll let my code run longer.

[Bruno Le Floch]

Regarding the commutative case, I noticed that the law (x*y)*(x*(y*z))=x is equivalent to the weak central groupoid law 1485 x=(y*x)*(x*(z*y)). I'll add that to my next batch of commentary updates once the bibliographic situation is clarified for the Sheffer stroke laws.

[David Michael Roberts]

Bruno Le Floch said:

This suggests that Wolfram had identified this as a candidate (in particular as holding for the Sheffer stroke I suppose), but not necessarily that he had proven the equivalence.

From what Wolfram writes in this post he claims he got the result in Jan 2000:

But at 8:31pm on Saturday, January 29, 2000, out on my computer screen popped a single axiom. I had already shown there couldn’t be anything simpler, but I soon established that this one little axiom was enough to generate all of logic

in the intro paragraph. The text starting "But just how simple can the axioms be? Well, that was what I wanted to discover in 1999." down to the end of the section fills in the story, in Wolfram's inimitable style :-)

[Bruno Le Floch]

Ok, thanks for the link to the 2018 blog post. See the pull request #1232 where I've updated the commentary and pointed here for a discussion of the credit to give to Wolfram and to McCune-Veroff.

EDIT: I forgot to mention here for reference that Wolfram's 2018 blog post states that the two laws 321577 and 329857 (in our numbering) are the only three-variable order 6 laws that characterize the Sheffer stroke.

[Notification Bot]

Bruno Le Floch has marked this topic as resolved.

[Notification Bot]

Alex Meiburg has marked this topic as unresolved.

[Alex Meiburg]

Are you sure about those numbers? The equations he lists are

((p*q)*r)*(p*((p*r)*p)) = r
(p*((r*p)*p))*(r*(q*p))=r

while currently in the repo we have

/-- The Sheffer stroke law. -/
equation 345169  :=  x = (y ◇ ((x ◇ y) ◇ y)) ◇ (x ◇ (z ◇ y))

which looks like it is exactly the latter of those two.

[Alex Meiburg]

I ask because it would be good to have both (the McCune law and the Wolfram law) in Basic.lean and the commentary, ideally. But those appear to be 329857 and 321577 and we have 345169 in repository atm

[Bruno Le Floch]

That's because of duality (and that the Sheffer stroke is commutative): you have duality pairs (329857, 345169) and (321577, 361729). McCune and Veroff published in June 2000 that 345169 (and its dual) are correct. With further coauthors [1] they proved in 2002 that the other pair is also a characterization of the Sheffer stroke. Wolfram had sent them a list of 25 candidates, possibly with claims or proofs of equivalence for these two pairs. In his 2018 blog post he claims to have reduced the list two only the two pairs "before many days had gone by", so early 2000. Nothing published of course (except possibly in his book). The McCune reference [1] from 2002 is very clear about the methods used to reduce to 18 candidates (see their Theorem 4), whereas we have nothing reproducible from Wolfram. About duality, note that my find_equation_id.py script can deal with it:

$ python find_equation_id.py 321577 329857 *329857 *321577
Equation 321577: x = ((y ◇ z) ◇ x) ◇ (y ◇ ((y ◇ x) ◇ y))
Equation 329857: x = ((y ◇ z) ◇ x) ◇ ((y ◇ (y ◇ x)) ◇ y)
The dual of Equation 329857 is Equation 345169: x = (y ◇ ((x ◇ y) ◇ y)) ◇ (x ◇ (z ◇ y))
The dual of Equation 321577 is Equation 361729: x = ((y ◇ (x ◇ y)) ◇ y) ◇ (x ◇ (z ◇ y))

Most likely there are indeed just two correct pairs so both should appear in Basic.lean, maybe even all four equations (but a single entry in the Tour). I'm hesitant to give names like McCune or Wolfram to them, as there is a good chance that Wolfram actually found both of them before McCune et al whereas they published it much before. Maybe Sheffer stroke law A, B, C, D, or first, second etc (unfortunately our ordering of laws puts what [1] call Sh1 and Sh2 in the opposite order or not depending on whether you take the smallest in a dual pair).

[1]: William McCune, Robert Veroff, Branden Fitelson, Kenneth Harris, Andrew Feist, and Larry Wos. Short single axioms for Boolean algebra. J. Automat. Reason., 29(1):1–16, 2002.

[Alex Meiburg]

Ah ok, thanks!

[Bruno Le Floch]

Minor update: a footnote of a 2002 paper by McCune et al states

Wolfram’s 25 candidates are precisely the set of Sheffer identities of length ≤ 15 (excluding mirror images) that have no noncommutative models of size ≤ 4.

[Stanley Burris]

Perhaps it is worth mentioning that almost all finite magmas have the property that their equational theory is axiomatizable by a single equation.
This is a consequence of almost all finite magmas being quasiprimal (Murskii) and all quasiprimals having an equational theory that is axiomatizable by a single equation (Padmanabhan and Quackenbush 1973).

Reference:
R. Padmanabhan and R.W. Quackenbush. Equational theories of algebras with distributive congruences. Proc. of AMS, 41(2):373–377, 1973.

Of the 16 magmas on {0,1} only two are quasiprimal, namely NAND and NOR, but on 3 elements {0,1,2} there are 8,851 quasiprimal magmas (1,485 if counting up to isomorphism). Given the effort expended to find a short axiom for Boolean algebra (see the above link to McCune from Bruno Le Floch) one can expect that finding short single axioms for the 3-element quasiprimal magmas will require very substantial computing power.

[Cody Roux]

That's remarkable! Do you have a reference for that "almost all finite magmas are quasiprimal" bit?

[Stanley Burris]

Here is an outline of the proof.

1. A finite algebra A is quasiprimal provided there is a ternary term t(x,y,z) such that A satisfies t(x,y,z) = z if x = y and t(x,y,z) = x if x \neq y.
2. t(x,y,z) is called a (ternary) discriminator term for A.
3. Such a discriminator term is idempotent on A, that is, t(x,x,x) = x.
4. A finite algebra A is idemprimal if every idempotent function f : A^n \rightarrow A can be realized by a term p(x_1,...,x_n).
5. Since the ternary function f(x,y,z) = z if x = y and f(x,y,z) = x if x \neq y is idempotent, it can be realized by a term t(x,y,z) on each idemprimal.
6. Murskii proved that almost all finite magmas are idemprimal. (This is the really difficult part.)
7. "Almost all" means the percentage of magmas on {0,...,n} that are idemprimal tends to 100% as n goes to infinity.
8. Thus almost all finite magmas are quasiprimal.

For which steps of this proof would you like to see references? I think I have covered most of them in various previous postings

Added Comment: The best reference is
Clifford Bergman. Universal algebra, volume 301 of Pure and Applied
Mathematics (Boca Raton). CRC Press, Boca Raton, FL, 2012.
Fundamentals and selected topics.

[Cody Roux]

Well the book is 400+ pages so maybe you can mention the section :) the Padmanabhan & Quackenbush paper (what great names by the way!) is quite terse but easy to find. A bit surprised they don't take that last step, though maybe that was discovered later.

[Stanley Burris]

Probability in universal algebra.pdf

I think Chapter 2 of this Master's Thesis by Florian Aichinger will answer your questions. Section 2.3 is essentially Murskii's result as presented in Bergman's book. Theorem 2.3.4 says almost all finite magmas (= binars = groupoids) are idemprimal, which is Theorem 6.23 in Bergman's book.

The last paragraph of P&Q says all quasiprimals are 1-based---this was in 1973. Murskii's result that almost all finite magmas are idemprimal (hence quasiprimal) was in 1975.

My colleague Joel Berman says that Murskii's result is one of the greatest accomplishments in universal algebra!

[Bruno Le Floch]

If I understand correctly the question for a given finite magma is to consider all equations that it satisfies, and find a minimal subset of equations that implies all of them? And you call it 1-based if a single equation satisfied by the magma implies all others?

I don't think we have the complete answer even for 2-element magmas. Let me write magmas on {0,1} in terms of their multiplication table, so 0011 denotes the left projection magma. Then the variety of 0000 (or isomorphically 1111) is given by the constant law 41 x◇x=y◇z. I think the variety of 0001 or 0111 (the "minimum" or "maximum" operations) is not 1-based, and is at most 3-based, given by law 3 x=x◇x, law 43 x◇y=y◇x, and law 4512 x◇(y◇z)=(x◇y)◇z. Those of 0011 and 0101 are given by the left/right projection laws x=x◇y and x=y◇x respectively. That of 0110 or 1001 is the Boolean group law 895 x=y◇((x◇z)◇(y◇z)). That of 1000 or 1110 is given by the Sheffer stroke law discussed in this thread. I think those of 1010 or 1100 are given by laws 24 x=(x◇x)◇y and 13 x=y◇(x◇x) respectively. That of 0010 (equivalently 0100, 1011, 1101) is unclear.

Asymptotically most finite magmas are idemprimal, but for small magma sizes they are not the majority. At least in your 3-element groupoid catalog only 1485 of the 3330 isomorphism classes are quasiprimal (idemprimality is not studied). Do you know how to determine if a finite magma is 1-based? Maybe restricting to these would keep the question under control?

[Stanley Burris]

The equational theory of a magma (or class of magmas) is indeed the set of all equations that hold in the magma (or class). It is n-based if it can be axiomatized by n equations, that is, there are n equations in the equational theory from which one can derive all the equational theory using Birkhoff's rules for equational logic. (One could also use first-order logic.)

I never thought of being n-based as implying that one cannot have fewer equations in a base. At the end of the 1973 paper by P&Q one finds the statement "there are finitely based equational theories ... which are n-based but not n — 1 based" indicating that for them being n-based did not imply there was no smaller base. The terminology in universal algebra was largely developed after WWII, and is still being developed and stabilized. For example, I first heard the word idemprimal in the last few months. Perhaps that is because I have not followed the terminology so closely since my retirement in the mid 1990s. I will forward your comments/questions to a few universal algebra colleagues for further insights.

One notion of a minimal equational base is one that is irredundant.
An equational base is irredundant if it fails to be a base after removing any equation. Tarski proved a beautiful result (see p. 33 of the B&S book) that implies the sizes of the finite irredundant bases of an equational theory of magmas is a convex set of integers.

I have nothing to add to your analysis of minimal sized bases for 2-element magmas except some additional terminology. Since the two element Boolean algebra is primal, any finitary function on {0,1} can be expressed by a term in Boolean algebra. The minimum operation is xy, the max x+y, generating the varieties of meet-semilattices and of join-semilattices. The operation 0110 is the symmetric difference xy' + x'y. The last four in your list are interesting but not familiar---the operation 0100 is simply x'y.

I have no idea of how to determine if a randomly chosen finite magma has a 1-based equational theory. Once we move away from traditional areas of algebra like groups, rings, lattices, and more recent areas like congruence distributive varieties, like varieties generated by quasiprimals, one has left the civilized world and entered the jungle. For example I have little hope of being able to determine the spectrum of a variety generated by a randomly chosen magma.

I don't know how rapidly the density of quasiprimals among n-element magmas converges to 100% although one could effectively find a value of n for which it is greater than say 50% by looking at the estimates in the 10 cases in Murskii's proof (stated in Aichinger's Masters Thesis). I suspect the density is monotone increasing, but that is only a guess. We have the counts for 2-element and 3-element magmas, but not even 4-element magmas.

[Stanley Burris]

Cliff Bergman informs me that the word idemprimal appeared and was defined, perhaps for the first time in print, in Bergman's book Universal Algebra, 2012, page 177, although it was evidently in limited circulation since the 1980s in manuscripts discussing Murskii's 1975 result. My 1981 book with Sanka was too early to include this word.

[Bruno Le Floch]

It seems possible that the equational theory of the [0,0,1,0] magma is 2-based: law 1043 x=x◇((y◇(x◇z))◇z) and law 4293 x◇(x◇y) = y◇(y◇x) (commutativity of Boolean AND) imply all laws of order up to 4 satisfied by this magma. I suppose we need to prove that any magma satisfying laws 1043 and 4293 is a subdirect product of copies of [0,0,1,0], namely can be seen as a subset of some power set, with the operation X◇Y = X∖Y.

[Alex Meiburg]

What do you mean by "the [0,0,1,0] magma"?

[Alex Meiburg]

Never mind, I see you explained your notation above

[Stanley Burris]

Bruno Le Floch: It seems possible that the equational theory of the [0,0,1,0] magma is 2-based ...

Let A be the 2-element magma ({0,1}, ◇) with operation table [0,0,1,0], and let V(A) be the variety it generates.

Indeed A is the only non-trivial subdirectly irreducible member of V(A), so every member of V(A) is as you described. There is likely a shorter proof than the following:

Proof: A generates the same variety as the 3-element magma B = ({0,1,2}, ◇) with table [0,0,0,1,0,1,2,2,0] since B is isomorphic to a subalgebra of A^2 and A is a subalgebra of B. From the B&B catalog for 3-element groupoids we know that the variety V(B) is congruence distributive (B is B&B #239). By a result of Jonsson (see B&S p. 149, Corollary 6.10) all subdirectly irreducible members of V(A) are in HS(A). QED

Showing that the associative law for AND, which is of order 10 when expressed in terms of ◇, follows from 1043 and 4293 would be an encouraging step towards proving one has a 2-base for the equational theory of the 2-element [0,0,1,0] magma.

To prove that 1043 and 4293 form a 2-base for V(A) indeed it suffices to show that A is the only subdirectly irreducible model of the two equations. One could try to emulate results of Stone for Boolean algebras and Birkhoff for distributive lattices to show that for any model M of the two equations and distinct elements a, b in M, a maximal congruence separating the two elements must have only two cosets. They were able to define a partial order a \le b by a \meet b = a. This carries over to V(A). For Boolean algebra one had the fact that a congruence is determined by the coset of 0, an ideal. From the consequence x◇x = y◇y of 1043 and 4293 one has a least element, and perhaps a congruence on M is also determined by the coset of this element.

[Stanley Burris]

Bruno Le Floch: I think the variety of 0001 or 0111 (the "minimum" or "maximum" operations) is not 1-based, and is at most 3-based,...

The three equations saying ◇ is idempotent, commutative and associative can be reduced to two, namely
x◇x = x and (x◇y)◇z = (y◇z)◇x,
by a 1953 result of Słupecki (see Grätzer’s Universal Algebra, 2nd ed., 1979). Here is the proof:

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

giving the commutativity of ◇. The associativity of ◇ follows immediately from this and the second equation above.

I agree, being 1-based looks most unlikely.

Addendum: The only non-trivial subdirectly irreducible model of the three equations above which define semilattices is the 2-element semilattice which is isomorphic to the two mentioned above (min and max)---see Exercise 7 page 60 in B&S. Thus the variety generated by either of these two is the variety of semilattices.

[Bruno Le Floch]

For the 0010 magma, here is an outline of a proof that 1043+4293 is a base of $V(A)$ with $A=[0,0,1,0]$. The proof superficially uses the axiom of choice, but I think it can be eliminated.

Proof that 1043+4293 is a base of V([0,0,1,0])

1. Fix a magma $M$ satisfying 1043+4293. We will construct a large collection of magma morphisms $\varphi_I\colon M\to A$ such that any two elements $a,b\in M$ are distinguished by some $\varphi_I$. Thus, the morphism $\prod_I \varphi_I \colon M\to \prod_I A$ is injective and $M$ obeys any equation satisfied by $A$ itself.

2. Laws 1043+4293 imply (x◇y)◇z = (x◇z)◇(y◇z), namely right multiplications are magma morphisms.

3. For any reference element $z\in M$, consider the right-coset $z\diamond M$ and the map $\pi_z\colon M\to z\diamond M$ defined by $\pi_z(x) = z\diamond(z\diamond x)$. It is the identity on $z\diamond M$ and is a magma morphism (not obvious).

4. The right coset $z\diamond M$, equipped with the meet operation $x\wedge y=x\diamond(x\diamond y)$ and not operation $\neg x=z\diamond x$, can be shown to obey associativity and commutativity of $\wedge$ and Huntington's equation $\neg(\neg a\wedge b)\wedge\neg(\neg a\wedge\neg b)=a$ hence it is a Boolean algebra.

5. If two elements $a,b\in M$ have $a\diamond b=0$ and $b\diamond a=0$ then $a=a\diamond 0=a\diamond(a\diamond b)=b\diamond(b\diamond a)=b\diamond 0=b$. Thus, two distinct elements $a,b\in M$ have either $a\diamond b\neq 0$ or $b\diamond a\neq 0$. Up to swapping the two elements, let us assume $a\diamond b\neq 0$. Consider the meet $c=\pi_a(b)=a\diamond(a\diamond b)$.

6. The magma morphism $\varphi\colon M\to a\diamond M$ defined by $\varphi(x) = \pi_a(x\diamond c)$ maps $b\mapsto 0$ and $a\mapsto a\diamond b\neq 0$. The image of $\varphi$ is actually contained in the coset $(a\diamond b)\diamond M$.

7. Using the axiom of choice, pick a Boolean algebra morphism $(a\diamond b)\diamond M\to\{0,1\}$ mapping $0\mapsto 0$ and $a\diamond b\mapsto 1$. Composing $\varphi$ with that gives the desired morphism $M\to A$ that maps $b\mapsto 0$ and $a\mapsto 1$.

I'm not sure about the last step that uses the axiom of choice. Probably all equations satisfied by A are satisfied by the operation $x\diamond y = x\wedge\neg y$ in any Boolean algebra.

If I didn't mess up some quick python+mace4 code, no other pair of equations of order ≤4 are equivalent to 1043+4293 (but I didn't rule out the possibility of another pair of equations of total order ≤8).

[Bruno Le Floch]

(EDIT: I moved the first part of the message to collect the discussion of the 0001 magma in one place.)

To show that the equational theory of 0001 cannot be generated by a single equation:

• if the equation has the form x=... then it must be a single-variable equation (as the RHS simplifies to the meet of all variables it involves), which cannot imply commutativity for instance;
• if the equation has non-zero order on both sides, then it is satisfied by the constant magma, so the equation cannot imply idempotence.

Now consider a 2-basis of the equational theory of 0001. One of the two equations must be of the form x=... (otherwise the constant magma would obey the two equations), and the other must have non-zero order on both sides (otherwise any idempotent magma would obey the two equations). The lowest-order choice for the first equations is idempotence x=x◇x, then the possibilities of order up to 4 for the second law are the shift-associative laws: law 4364 x◇(y◇z) = y◇(z◇x) or its dual law 4679 (x◇y)◇z=(y◇z)◇x, or law 4541 x◇(y◇z) = (z◇x)◇y.

It turns out that x=x◇(x◇x) and (x◇y)◇z = (y◇z)◇(x◇x) form another 2-basis, so we don't necessarily have to include idempotence. I didn't explore such other low-order possibilities.

[Bruno Le Floch]

I'm a bit confused though: do these results mean that any magma satisfying idempotence and law 4364 (say) must be a subdirect power of the 0001 magma? (Or do I need a proof similar to what you used referring to the B&B catalog?)

[Stanley Burris]

Let me return to the 0010 magma later, but for now let's review some basic facts from universal algebra, stated for magmas but they apply for algebras in general, and apply them to V(0001).

Let E be a collection of magma equations, and e such an equation. Let's say "e is a consequence of E" if either of the following two equivalent conditions hold:

1) (semantic consequence) Every magma satisfying E also satisfies e.

2) (syntactic consequence) There is a formal derivation of e from E (say using Birkhoff's rules for equational logic).

Their equivalence is Birkhoff's completeness theorem. There are cases where 1) is easier to apply, and cases where 2) is a better choice.

Understanding the variety V(M) generated by a magma M has two basic components:

a) Describing the magmas in V(M)

b) Finding a set of equations (a base) for the equational theory of V(M), which is the same as the equational theory of M.

(The same setup applies to a variety V(K) generated by a class K of magmas.)

For (a) we know from Tarski that V(M) consists of all homomorphic images of subalgebras of powers of M (this is the HSP theorem). To get something more "concrete" Birkhoff showed that every magma is a subdirect product of subdirectly irreducible magmas, the subdirectly irreducibles being homomorphic images of the magma. Getting ones hands on the subdirectly irreducible members of V(M) may be difficult, but in some cases we can. If M is finite and V(M) is congruence distributive, that is every magma in V(M) has a distributive lattice of congruences, Jónsson showed that every subdirectly irreducible in V(M) is a homomorphic image of a subalgebra of M. For M small and finite this makes finding the subdirectly irreducibles rather easy. In particular if M has 2 elements then it is the only subdirectly irreducible in V(M).

But V(0001) is not congruence distributive, so we resort to a direct semantic argument just for it to determine the subdirectly irreducible members. 0001, being a 2-element magma, is subdirectly irreducible. One goal is to show there are no other non-trivial subdirectly irreducibles in V(0001). We do know that every member of V(0001) satisfies the idempotent, commutative and associative equations since 0001 does. We will show that each magma satisfying these 3 equations is in V(0001), so they form a 3-base for V(0001).

On each magma M satisfying these 3 equations define a binary relation \le by a \le b iff a = a ◇ b. Using these 3 equations one can prove that \le is a partial order on the elements of M.

For distinct a,b in M with a not-\le b define an equivalence relation R on M by
xRy iff (a \le x and a \le y) or (a not-\le x and a not-\le y).
Then a and b are not R-equivalent.
Also there are exactly two equivalence classes, namely {x : a \le x} and {x : a not-\le x}. From the three equations we know M satisfies one can prove that R is a congruence on M, that is, xRy and uRv imply xuRyv.
The quotient magma M/R is isomorphic to 0001, and a/R \neq b/R.
This means M can be embedded in the product of all such M/R, that is,
in a power of 0001.
Thus we finally have a structure theorem for V(0001), namely all members are subdirect powers of 0001, and vice-versa. This was achieved with only knowing the 3 equations above held in V(0001), and every model of them is in V(0001). So they must not only be true of V(0001), they must axiomatize it, i.e., be a base for its equational theory.

[Bruno Le Floch]

Thanks a lot for the explanation! That also clarifies some details of your proof above that V(0010) has a unique subdirectly irreducible magma. However, I notive that the proofs via the B&B catalog and congruence distributivity are useful mostly to orient us, but do not seem load-bearing in the final arguments. Indeed, to prove that some equations E are a basis of the equational theory for V(A), what we really care about is to determine subdirectly irreducible magmas satisfying E, and specifically show they belong to V(A).

For A=0001 and E=[idempotence, commutativity, associativity] that's what you did: for any magma M obeying E, and distinct elements a,b∈M, either a≰b or b≰a, and you built a morphism to A that distinguishes these two elements. But a subdirectly irreducible M would have a pair of elements a,b that could not be distinguished by any homomorphic image not isomorphic to M. So the only possible subdirectly irreducible one is M=A. (Alternatively, taking for instance the product over all pairs (a,b), we inject M into a power of A.)

For A=0010 and E=[1043,4293], I built similarly a morphism to a Boolean algebra equipped with x◇y = x∧¬y. This shows that subdirectly irreducible magmas M obeying E are such Boolean algebras that are subdirectly irreducible as Boolean algebras. With (a weak form of) the axiom of choice we have the Stone representation theorem that realizes the algebra as the set of clopen sets of some topological space, and in particular as a subalgebra of the power set of that space, which is simply a power of A.

Without the axiom of choice, a mathoverflow answer by François G. Dorais points out that H. Läuchli MR143705 built a model with an infinite-dimensional vector space whose proper subspaces are finite-dimensional. If this still works over the fields F2, then we may get a Boolean algebra whose quotients are all isomorphic to itself. Details are very unclear to me. Despite these subtleties, I would be shocked if the resulting subdirectly irreducible magma fails to belong to V(A).

[Stanley Burris]

You are welcome! As you noted, when it comes to looking for a basis for V(A), A finite, one finds a candidate set of equations E that holds in A and tries to prove all models of E are in V(A). Knowing info about subdirectly irreducibles can be helpful.

P&Q (1973) show that in congruence distributive V(A) they have some methods to shrink the number of equations in a basis E (for V(0010) down to 3), and for congruence distributive and congruence permutable V(A) all the way down to one equation (which applies to quasiprimals A).

I have read that this compression can lead to enormous equations, which might explain why explicit single equations for Boolean algebra did not appear until ca. 2000. For A with more than 4 elements just determining if A is quasiprimal or is congruence distributive can be computationally very challenging.

It looks like I will have little time to study your "no 1-basis" result for semilattices nor the 2-basis result for V(0010) for the next few days. But I do intend to give them a serious examination and post my comments.

[Stanley Burris]

The equational theory of semilattices, V(0001), is not 1-based :eyes:

Proof: Suppose p = q is a 1-base for semilattices.

Note that an equation holds in semilattices iff both sides have the same variables (just check out the equation on the 2-element semilattice).

An elementary deduction from p = q is, by definition, one of the form
r(... \sigma p ...) = r(...\sigma q ...) or the form r(... \sigma q ...) = r(...\sigma p ...)
where \sigma p and \sigma q are substitution instances of p and q, each using the same substitution \sigma, each having the same "location" in the term r(...).

A chain deduction from p = q has the form
p_1 = p_2 = ... = p_n
with each step p_i = p_{i+1} being elementary.

FACT: An equation s_1 = t_1 can be derived from s = t in Birkhoff's system iff there is a chain deduction of s_1 = t_1 from s = t. (See B&S page 98, Exercise 11).

To derive x = x◇x from p = q by a chain deduction the first elementary deduction in the chain must be of the form x = p_2.
This means p = q has the form x = q(x) or q(x) = x, where q(x) is a term in the single variable x.

For t a term let X_t be the set of subterms of t that are not variables.
Let P(t) be the property that if X_t is not empty then the only member of X_t of order 1 is x◇y.

(**) If e is an elementary deduction from x = q(x) such that the left side has P then so does the right side.

Now suppose p_1 = p_2 = ... = p_n is a chain derivation of the commutative law x◇y = y◇x from x = q(x).

The first elementary deduction p_1 = p_2 must be x◇y = q(x◇y), and p_n must be y◇x.

Thus P(p_n) does not hold. Since P(p_1) holds, by (**) P(p_j) holds for all j , a contradiction.

Thus p = q cannot be an equational base for V(A). QED

NOTE: I cancelled an earlier version to have time to double check the FACT, not having worked with the B&S book for more than 20 years.

If my memory is correct I learned about chain deductions from Murskii's 1965 paper showing that the equational theory of a certain 3-element magma is not finitely based.

[Stanley Burris]

Now that it seems that the equational theory of V(0001) is indeed 2-based but not 1-based, I want to return to looking at V(0010), which is the same as V(B&B #239) .

SOME BACKGROUND

First some clarification. When Joel and I made the B&B catalog back in the 1990s the goal was to show how computers could be useful to assist in proving theorems in universal algebra about finitely generated varieties V(A) regarding popular topics like congruence distributivity (CD), congruence permutability (CP), congruence modularity (CM), quasiprimality, etc.

A word about why CD was much in fashion.
(1) Every finitely generated CD variety is finitely based. (Baker)
(2) For A finite and V(A) CD, the subdirectly irreducibles in V(A) are in HS(A). (Jónsson)

Example regarding (2): Given two finite magmas A and B, a simple question was how to determine if V(A) is a subclass of V(B), i.e., does A belong to V(B). If V(A) and V(B) were CD then by Jónsson's result one could sort through the finitely many quotients of subalgebras of A to find all the subdirectly irreducibles in V(A), and likewise for V(B). Then V(A) is a subclass of V(B) iff the first set of subdirectly irreducibles is a subset of the second set. With great enthusiasm this was actually used to determine portions of the lattice of varieties of lattices since every variety of lattices is CD.

To impress our colleagues we decided to computer analyze properties of A and V(A) for the thousands (3^9) of 3-element magmas. Using the same algorithms we separately wrote C-programs for the entire catalog to hopefully guarantee the accuracy of the results. The results were well received by colleagues, few of whom were proficient in computer programming at the time.

It never occurred to us to make a catalog for the sixteen 2-element magmas, so recently when considering V(0010) my first query was to see if there was a 3-element magma generating this variety so I could use the B&B catalog. To my surprise there was (B&B # 239) , and thus I learned that V(0010) is CD but not CP.

The computer proof that V = V(B&B #239) is CD used a brute force search algorithm to find two ternary Jónsson terms (Theorem 12.6, B&S, page 80)

 p_1(x,y,z) is  x◇((x◇y)◇z)        p_2(x,y,z) is  z◇(y◇x)

such that V satisfies

x = p_1(x,x,y)
p_1(x,y,y) = p_2(x,y,y)
p_2(x,x,y) = y,

that is, it satisfies

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

These equations hold in V(0010). Then P&Q (1973) Theorem 1, page 375 says this guarantees the variety is 3-based. Presumably one can effectively find the basis from the Jónsson terms...I need to study this paper to see what is going on!

[Stanley Burris]

@Bruno Le Floch The proof that 1043+4293 is a base of V([0,0,1,0]) looks good !modulo filling in the missing details for several claimed derivations from 1043+4293. If they are only accessible through an ATP then independent verifications would be reassuring. (Unfortunately I do not have such software and am not very adventuresome at my age.)

Regarding using the axiom of choice or some near relative, one does not need such to prove that the only non-trivial directly indecomposable Boolean algebra is the two-element one (B&S page 120, Cor. 1.9.), hence this is the only non-trivial subdirectly irreducible Boolean algebra. However to prove that every Boolean algebra satisfies all the identities of the two-element BA it seems one needs Zorn's Lemma to show every algebra is a subdirect product of subdirectly irreducibles (B&S page 58, Thm 8.6).

To prove that this variety is not 1-based (if true) I suspect that, much as with semilattices, one would need a property P that holds for both sides of every elementary deduction from the two axioms whenever one side has P, but holds only for one side for a suitably narrowed list of possible candidates for a single axiom. As with semilattices, one side of a single axiom would have to be a variable.

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

Stanley Burris said:

However to prove that every Boolean algebra satisfies all the identities of the two-element BA it seems one needs Zorn's Lemma to show every algebra is a subdirect product of subdirectly irreducibles

Apologies in advance: the following is a drive-by comment on something that caught my eye, and I might be missing important context or misunderstanding what you're trying to do.

One does not need Zorn's lemma to prove that every Boolean algebra satisfies the same algebraic identities as the two-element Boolean algebra. The following argument works.

Take any identity $\varphi(x_1,x_2,\dots,x_n)$ that holds in the two-element Boolean algebra. Assume that $\varphi(x_1,x_2,\dots,x_n)$ fails in some Boolean algebra $B$. Then we can find $b_1,b_2,\dots,b_n \in B$ so that $\neg \varphi(b_1,b_2,\dots,b_n)$ holds in $B$.

Consider the subalgebra $F$ of $B$ generated by $b_1,b_2,\dots,b_n$. By construction $\neg \varphi(b_1,b_2,\dots,b_n)$ still holds in $F$.

But a finitely generated Boolean algebra is finite, and every finite Boolean algebra satisfies all the identities of the two-element Boolean algebra since every finite Boolean algebra is a Cartesian power of the two-element Boolean algebra. This contradicts our assumption.

[Bruno Le Floch]

Thanks Zoltan. This proof works in our context indeed! It can also be made into an explicit algorithm to prove/disprove any given equation: write both sides in disjunctive normal form using properties of Boolean algebras and compare them.

Stanley Burris said:

Regarding using the axiom of choice or some near relative, one does not need such to prove that the only non-trivial directly indecomposable Boolean algebra is the two-element one (B&S page 120, Cor. 1.9.), hence this is the only non-trivial subdirectly irreducible Boolean algebra.

I think this is incorrect: indeed the Boolean algebra B can be written as a product, but it may be the case that one of the factors is isomorphic to B itself, so that B is not subdirectly irreducible, at least according to the Wikipedia definition of subdirect irreducibility. Zoltan's proof circumvents all that by showing that once we have a Boolean algebra we are done.

For the rest of the proof indeed there are a lot of ATP-derived steps. I could try to collect the various ATP inputs for reference, or to convert them into a Lean proof, but it would be best to determine what we plan to do with these results, to avoid wasting efforts on formalization. E.g., if the goal is simply to add commentary about equations 1043 and 4293 in the equation explorer then we don't need to be very formal.

[Stanley Burris]

@Zoltan A. Kocsis (Z.A.K.) Your claim that

One does not need Zorn's lemma to prove that every Boolean algebra satisfies the same algebraic identities as the two-element Boolean algebra.

looks plausible. We did not pay much attention to the subtleties of set theory when writing B&S so I will need to sort this out.

[Stanley Burris]

@Bruno Le Floch said:

indeed the Boolean algebra B can be written as a product, but it may be the case that one of the factors is isomorphic to B itself, so that B is not subdirectly irreducible, at least according to the Wikipedia definition of subdirect irreducibility.

I'm not sure of what is intended in this statement. If a Boolean algebra B can be written as a product of two non-trivial BAs, say B \isom B_1 x B_2, then the kernels of the projection maps are non-trivial congruences of the product, but their intersection is the trivial congruence. This means B does not have a smallest non-trivial congruence, and hence cannot be subdirectly irreducible (B&S page 57, Theorem 8.4).
Thus subdirectly irreducible implies directly indecomposable.

Perhaps a word on the Wikipedia definition is needed:

A universal algebra A is said to be subdirectly irreducible when A has more than one element, and when any subdirect representation of A includes (as a factor) an algebra isomorphic to A, with the isomorphism being given by the projection map.

The phrase "any subdirect representation" needs to be read as "every subdirect representation", not "some subdirect representation".

Regarding how much detail needs to be written up regarding the proof that the variety V(0010) is axiomatized by equations 1043 and 4293 goes to the core of the dilemma mathematicians face when there are powerful ATPs. Short of Lean verification, how much weight is to be given to announcements of new results obtained only with the help of computers, especially ATPs? And how much credit to the author when it comes to climbing the academic ladder? If you leave your work on V(0010) as it is, will your 2-basis be regarded simply as a "claim", or a "likely theorem"? I don't know the answer to these questions.

[Stanley Burris]

@Zoltan A. Kocsis (Z.A.K.)

I finally got the facts straight in my head, and indeed your proof goes through without the Axiom of Choice or its relatives (just need ZF set theory). Very nice indeed!

[Stanley Burris]

@Bruno Le Floch @Zoltan A. Kocsis (Z.A.K.)

I was so impressed by Bruno's 2 axioms for V(0010) that I sent a note to 9 of the top universal algebraists I know asking what was known about equational axioms for this variety. A prompt reply from Keith Kearnes, UColorado, Boulder, follows, discussing bases for all of the 2-element magmas.

EQUATIONAL BASES for 2-ELEMENT MAGMAS

Your magma is 2-based but not 1-based.

You mentioned that there are sixteen magmas with universe {0,1}. 

True, but there are only seven up to isomorphism or anti-isomorphism,

and that's all that matters for this problem. Of these seven, 

five are 1-based and the other two are 2-based but not 1-based.

The seven magma multiplications on the set {0,1}

(up to isomorphism/anti-isomorphism) are,

in Boolean notation:

1. (constant)  xy := 0

1-based: xy=uv

2. (projection) xy := x

1-based: xy=x

3. (projection composed with negation) xy := x' = \neg x

1-based: (xy)z = x     (Exercise!)

4. (Boolean group) xy := (x\wedge \neg y) \vee (\neg x\wedge y)

1-based: x(((xy)z)y)z = z

See Thm 1 of 
A single identity for Boolean groups and Boolean rings

N. S. Mendelsohn, R. Padmanabhan

J. Algebra 20, 78-82, (1972)

5. (Nand) xy := (x\wedge y)'  =  \neg(x\wedge y)

1-based: x((yx)x)(y(zx)) = y

See Theorem 2 of
Short Single Axioms for Boolean Algebra

W. McCune + 4 others

J. Automated Reasoning, 29, 1-16, (2002)

6. (Semilattice) xy := x\wedge y

2-based, but not 1-based.

See

Axioms for Semi-Lattices

D. H. Potts

Canadian Math Bulletin, 8 (1965), 519-519.

The two identities Potts gives to axiomatize semilattices are:

xx=x, 

and

(uv)((wx)(yz)) = ((vu)(xw))(zy)

7. (Implication algebra) xy  :=  x\to y  =  (\neg x) \vee y

2-based, but not 1-based 

See Theorems 1 & 2 of
Two Axioms for Implication Algebras

A. Gareau and R. Padmanabhan

Notre Dame J. of Formal Logic, 2006.

The two identities Gareau and Padmanabhan give 

to axiomatize implication algebras are:

(xy)x = x, 

and

x(y((zu)u)) = y(x((uz)z)) 

---

Stan, your magma   <{0,1}; x\wedge y'>    belongs

to isomorphism/antiisomorphism class #7, which means that up to a change

of notation it is the 2-element implication algebra. This makes

your magma 2-based but not 1-based.  

The fact that the 2-element implication algebra

generates a variety that is CD and not CP can be found in 
Implication algebras are 3-permutable and 3-distributive. 

Aleit Mitschke

Algebra Universalis 1, (1971), 182-186.

Here is her Theorem 2:
THEOREM 2. The equational class of all implication algebras is

(P) 3-permutable, but not 2-permutable.

(M) 3-modular, but not 2-modular.

(D) 3-distributive, but not 2-distributive.

---

Let me give a short, human-readable proof that the 2-element implication algebra

is not 1-based.

Call an identity s = t an "absorption identity" if at least one

of the terms s, t is a variable.

Lemma 1. If s = t is NOT an absorption identity, then s = t 

holds in the 2-element algebra with constant multiplication.

(Easy!)

Lemma 2. If s = t holds in the 2-element implication algebra

and s = t  IS  an absorption identity, then s = t 

also holds in the 2-element algebra whose multiplication

is right projection.

Cor. Any single identity that holds in the 2-element implication algebra

must hold in either the 2-element constant algebra or the

2-element right projection algebra (neither of which 

belong to any CD variety). Hence no single identity

axiomatizes the CD variety generated by the 2-element 

implication algebra.

Here is how I would argue for Lemma 2:

Assume that s(x,y,z,\ldots) = x is an absorption identity

in the language of implication algebra (here xy: = x\to y = (\neg x \vee y).

If the rightmost leaf of the term tree for s is labeled

by any variable other than x, then in the 2-element

implication algebra we get 

s(0,1,1,1,1,\ldots) = 1 \neq 0 = x,

so the identity s = x does not hold in the 2-element 

implication algebra. 

On the other hand, if the rightmost leaf of the term tree for s 

IS labeled by x, then the identity s = x will hold

in the 2-element right projection algebra. Altogether, any

absorption identity either fails in the 2-element

implication algebra or holds in the 2-element

right projection algebra.\\\\\\

[Bruno Le Floch]

Please thank Keith Kearnes on my behalf! What he wrote is consistent with my understanding, and knowing the name "implication algebra" will help me navigate the literature.

Regarding the academic ladder, I really don't care: being a string theorist, this whole project can at best be seen as a distraction by anyone evaluating me. That said, your point about ATP proofs being unconvincing on their own is well-taken, so I will try my hand at a Lean formalization and summarizing the whole discussion. Hopefully some time this month or the next.

[Stanley Burris]

Message of thanks sent!