Robbins algebra

In abstract algebra, a Robbins algebra is an algebra containing the a single binary operation, denoted by infix $\lor$, and a single unary operation $\neg$. These operations satisfy the following axioms:

For all elements a, b, and c:

1. Associativity: $a\lor (b\lor c)=(a\lor b)\lor c$
2. Commutativity: $a\lor b=b\lor a$
3. Robbins axiom: $\neg (\neg (a\lor b)\lor \neg (a\lor \neg b))=a$

History

In 1933, Edward Huntington proposed a new set of axioms for Boolean algebras, consisting of (1) and (2) above, plus:

• Huntington's axiom: $\neg (\neg a\lor b)\lor \neg (\neg a\lor \neg b)=a.$

From these these axioms, Huntington derived the usual axioms of Boolean algebra.

Very soon thereafter, Herbert Robbins posed the Robbins conjecture, namely that the Huntington axiom could be replaced with its dual, which came to be called the Robbins axiom, and the result would still be Boolean algebra. $\lor$ would interpret Boolean join and $\neg$ Boolean complement. Boolean meet and the constants 0 and 1 are easily defined from the Robbins algebra primitives. Pending verification of the conjecture, the system of Robbins was called "Robbins algebra."

Verifying the Robbins conjecture required proving Huntington's axiom, or some other axiomatization of Boolean algebra, as theorems of Robbins algebra. Huntington, Robbins, Alfred Tarski, and others worked on the problem, but failed to find a proof or counterexample.

William McCune proved the conjecture in 1996, using the automated theorem prover EQP. For a complete proof of the Robbins conjecture in one consistent notation and following McCune closely, see Mann (2003). Dahn (1998) simplified McCune's machine proof.

References

• Dahn, B. I. (1998) Abstract to "Robbins Algebras Are Boolean: A Revision of McCune's Computer-Generated Solution of Robbins Problem," Journal of Algebra 208(2): 526-32.
• Mann, Allen (2003) "A Complete Proof of the Robbins Conjecture."
• William McCune, "Robbins Algebras Are Boolean," With links to proofs and other papers.