The Full Wiki

More info on Robbins algebra

Robbins algebra: Wikis

Advertisements

Note: Many of our articles have direct quotes from sources you can cite, within the Wikipedia article! This article doesn't yet, but we're working on it! See more info or our list of citable articles.

Encyclopedia

From Wikipedia, the free encyclopedia

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

For all elements a, b, and c:

  1. Associativity: a \lor \left(b \lor c\right) = \left(a \lor b\right) \lor c
  2. Commutativity: a \lor b = b \lor a
  3. Robbins's axiom: \neg \left( \neg \left(a \lor b \right) \lor \neg \left(a \lor \neg b \right) \right) = 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 \left( \neg \left( a \lor b \right) \lor \neg \left( \neg a \lor \neg b \right) \right) = a.

From these axioms, Huntington derived the usual axioms of Boolean algebra. Specifically, what Huntington proved was that if we take \lor to interpret Boolean join, \neg to interpret Boolean complement and use \lor and \neg to define Boolean meet and the constants 0 and 1, then the axioms for a Boolean algebra are satisfied.

Very soon thereafter, Herbert Robbins posed the Robbins conjecture, namely that the Huntington axiom could be replaced with Robbins's axiom, and the result would still be a Boolean algebra in the sense explained in the previous paragraph. 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 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 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

Advertisements

Advertisements






Got something to say? Make a comment.
Your name
Your email address
Message