Robbins algebra

A Robbins algebra is an algebra consisting of the set {0,1} and the logical operations $lor$ (disjunction, "or") and $eg$ (negation, "not"), with the following axioms:

* Associativity: $a\; lor\; (b\; lor\; c)\; =\; (a\; lor\; b)\; lor\; c$
* Commutativity: $a\; lor\; b\; =\; b\; lor\; a$
* Robbins' axiom: $eg(\; eg(a\; lor\; b)\; lor\; eg(a\; lor\; eg\; b))\; =\; a$

The Robbins conjecture, posed by Herbert Robbins, is that these axioms are equivalent to those of Boolean algebras. The conjecture was proven 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":
* $eg(\; eg\; a\; lor\; b)\; lor\; eg(\; eg\; a\; lor\; eg\; b)\; =\; a.$The validity of this axiom in Boolean logic can easily be proved using its truth table. Huntington also 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 equivalent to 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

* [http://www.cs.unm.edu/~mccune/papers/robbins] William McCune's page on the conjecture with links to proofs
* [http://math.colgate.edu/~amann/MA/robbins_complete.pdf] A Complete Proof of the Robbins Conjecture, by Allen Mann