Order, lattices, ordered algebraic structures Theorem

Robbins conjecture

Builds on Huntington's axioms Boolean algebra

Statement

Let $A$ be a set with a binary operation $+$ and a unary operation $n$ such that for all $x, y, z \in A$ :

$x + y = y + x$ ;
$(x + y) + z = x + (y + z)$ ;
$n(n(x + y) + n(x + n(y))) = x$ .

Such a structure is called a Robbins algebra, and axiom 3 is Robbins' equation. Then $A$ satisfies Huntington's equation $n(n(x) + y) + n(n(x) + n(y)) = x$ , so $(A, +, n)$ is a Boolean algebra with $+$ as join and $n$ as complement.

Remarks

Every Boolean algebra satisfies Robbins' equation, so the theorem says that the Robbins algebras are exactly the Boolean algebras. The question was raised by Herbert Robbins in the 1930s and stayed open for about sixty years. William McCune settled it in 1996 with the automated theorem prover EQP, which found a derivation of a condition that earlier work had shown to be sufficient. The proof is purely equational; human-readable versions of it were written later.

Going deeper

For a student

The result is a standard example of a mathematical question solved by an automated theorem prover. It shows that the equational theory of Boolean algebras has several very short bases, and the search for the shortest single axioms for Boolean algebra builds on such results. The proof works inside equational logic: it uses only substitution and replacement of equals by equals, starting from the three axioms.

Reading path

To understand this page from the ground up, read these 3 pages in order. The foundations come first.

Show the path as a graph

Each page uses the pages above it. The colour of the bar on a box shows how strong the evidence is, and the box also gives it as text. The list has the same pages.

no evidence level

Tag	`X74S395RZD`
URI	`m2://X74S395RZD`
Kind	statement, theorem
Writing	W0 stub
MSC	06E05, 03G05, 68V15
Status	This copy of the site has no build data. Run `m2 status X74S395RZD`.
About	Boolean algebra
Uses	Huntington's axioms, Boolean algebra
Changed	2 November 2026