View source for Herbrandization

In [[abstract algebra]], a '''Robbins algebra''' is an [[Universal algebra#Basic idea|algebra]] containing a single [[binary operation]], usually denoted by <math>\lor</math>, and a single [[unary operation]] usually denoted by <math>\neg</math>. These operations satisfy the following [[Universal algebra#Equations|axioms]]:

For all elements ''a'', ''b'', and ''c'':
# [[Associativity]]: <math>a \lor \left(b \lor c\right) = \left(a \lor b\right) \lor c</math>
# [[Commutativity]]: <math>a \lor b = b \lor a</math>
# ''Robbins equation'': <math>\neg \left( \neg \left(a \lor b \right) \lor \neg \left(a \lor \neg b \right) \right) = a</math>

For many years, it was conjectured, but unproven, that all Robbins algebras are [[Boolean algebra (structure)|Boolean algebra]]s.  This was proved in 1996, so the term "Robbins algebra" is now simply a synonym for "Boolean algebra".

== History ==
In 1933, [[Edward Huntington]] proposed a new set of axioms for Boolean algebras, consisting of (1) and (2) above, plus: 
*''Huntingtons equation'': <math>\neg(\neg a \lor b) \lor \neg(\neg a \lor \neg b) = a.</math>
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 (structure)|Boolean algebra]]. <math>\lor</math> would interpret Boolean [[Boolean algebra (structure)#Definition|join]] and <math>\neg</math> Boolean [[Boolean algebra (structure)#Definition|complement]]. Boolean [[Boolean algebra (structure)#Definition|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 Huntingtons 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.

[[William McCune]] proved the conjecture in 1996, using the [[automated theorem proving|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 "[http://www.sciencedirect.com/science?_ob=ArticleURL&_udi=B6WH2-45S4RJV-7&_user=10&_rdoc=1&_fmt=&_orig=search&_sort=d&view=c&_acct=C000050221&_version=1&_urlVersion=0&_userid=10&md5=cafdb746bc7e14ffe040ff04ec4e42c2 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) "[http://math.colgate.edu/~amann/MA/robbins_complete.pdf A Complete Proof of the Robbins Conjecture.]"
* [[William McCune]], "[http://www.cs.unm.edu/~mccune/papers/robbins/ Robbins Algebras Are Boolean,]" With links to proofs and other papers.

{{DEFAULTSORT:Robbins Algebra}}
[[Category:Boolean algebra]]
[[Category:Formal methods]]