Robbins algebra

A Robbins algebra is an algebracontaining the binary operation $\lor$ and the unary operation $\neg$. These operations satisfy the following axioms:

For all elements a, b and c

• Associativity: $a\lor (b\lor c)=(a\lor b)\lor c$
• Commutativity: $a\lor b=b\lor a$
• Robbins' axiom: $\neg (\neg (a\lor b)\lor \neg (a\lor \neg b))=a$

The Robbins conjecture, posed by Herbert Robbins, is that a Robbins algebra is a Boolean algebra, after adding the other binary operation and the constants, with $\lor$ playing the role of joinand $\neg$ the role of complement. The conjecture was proved in 1996 by William McCune, using an automated theorem prover.

History

In 1933, Edward Huntington proposed an alternative set of axioms for Boolean algebras, consisting of the aforementioned axioms of associativity and commutativity plus Huntington's axiom:

• $\neg (\neg a\lor b)\lor \neg (\neg a\lor \neg b)=a.$

Huntington showed the three axioms together imply the axioms of Boolean algebra.

Some time after, Robbins conjectured that his (slightly simpler) axiom implies that of Huntington, so that Robbins algebras are essentially Boolean algebras. Huntington, Robbins and Alfred Tarski worked on the problem, but failed to find a proof or counterexample. The proof was finally delivered in 1996 by William McCune, using his theorem prover EQP.

External links

• [1] William McCune's page on the conjecture with links to proofs
• [2] A Complete Proof of the Robbins Conjecture, by Allen Mann