Wikipedia

Robbins algebra#History

In abstract algebra, a Robbins algebra is an algebra containing a single binary operation and a single unary operation that satisfy the following axioms:[1]

For all elements a, b, and c:

  1. Associativity:
  2. Commutativity:
  3. Robbins equation:

For many years, it was conjectured, but unproven, that all Robbins algebras are Boolean algebras. This was proved by William McCune in 1997,[1][2][3] so the term "Robbins algebra" is now simply a synonym for "Boolean algebra".

History

[edit]

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

  • Huntington's equation:

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

Very soon thereafter, Herbert Robbins posed the Robbins conjecture, namely that the Huntington equation could be replaced with what came to be called the Robbins equation, and the result would still be Boolean algebra. would interpret Boolean join and 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 equation, or some other axiomatization of a Boolean algebra, as theorems of a Robbins algebra. Huntington, Robbins, Alfred Tarski, and others worked on the problem, but failed to find a proof or counterexample.

McCune's proof

[edit]

In 1996, William McCune proved the conjecture using the automated theorem prover EQP (equational prover).[6] EQP was developed by McCune while working at the Mathematics and Computer Science Division of the Argonne National Laboratory.[7] McCune considered EQP a prototype which he developed specifically to prove the Robbins conjecture, unlike OTTER, another theorem prover which he developed for general use.[8] The proof took eight days to be completed by EQP. McCune later called Robbins, then 81 years old, to tell him that the conjecture had been proved.[7]

McCune's proof built on prior work on the conjecture by Steve Winker, also a researcher at Argonne.[6][9]

For a complete proof of the Robbins conjecture in one consistent notation and following McCune closely, see Mann (2003).[10] Dahn (1998) simplified McCune's machine proof.[3]

See also

[edit]

References

[edit]
  1. ^ a b Weisstein, Eric W. "Robbins Algebra". Retrieved 2025-09-09.
  2. ^ McCune, William (1997). "Solution of the Robbins Problem". Journal of Automated Reasoning. 19 (3): 263–276. doi:10.1023/A:1005843212881.
  3. ^ a b Dahn, Bernd I (1998-10-15). "Robbins Algebras Are Boolean: A Revision of McCune's Computer-Generated Solution of Robbins Problem". Journal of Algebra. 208 (2): 526–532. doi:10.1006/jabr.1998.7467. ISSN 0021-8693.
  4. ^ Huntington, Edward V. (1933). "New sets of independent postulates for the algebra of logic, with special reference to Whitehead and Russell's Principia mathematica". Transactions of the American Mathematical Society. 35: 274–304. doi:10.1090/S0002-9947-1933-1501684-X. JSTOR 1989325.
  5. ^ Huntington, Edward V. (1933). "Boolean algebra. A correction". Transactions of the American Mathematical Society. 35 (2): 557–558. doi:10.1090/S0002-9947-1933-1501702-9. JSTOR 1989783.
  6. ^ a b McCune, William (1996). "Robbins algebras are boolean". Association for Automated Reasoning Newsletter. 35: 1–3.
  7. ^ a b Kolata, Gina (December 10, 1996). "Computer Math Proof Shows Reasoning Power". The New York Times. Retrieved 10 December 2025.
  8. ^ Bonacina, Maria Paola; Stickel, Mark E., eds. (2013). Automated Reasoning and Mathematics: Essays in Memory of William W. McCune. Berlin, Heidelberg: Springer. p. IX. ISBN 3642366740. Retrieved 10 December 2025.
  9. ^ Wos, Larry (2013). "The Legacy of a Great Researcher". In Bonacina, Maria Paola; Stickel, Mark E. (eds.). Automated Reasoning and Mathematics: Essays in Memory of William W. McCune (PDF). Berlin, Heidelberg: Springer. p. 6. ISBN 3642366740. Retrieved 10 December 2025.
  10. ^ Wampler-Doty, Matthew (2010). "A complete proof of the Robbins conjecture". The Archive of Formal Proofs.
[edit]

McCune's website on EQP