Robbins algebra
Encyclopedia
In abstract algebra
, a Robbins algebra is an algebra containing a single binary operation
, usually denoted by
, and a single unary operation
usually denoted by
. These operations satisfy the following axioms:
For all elements a, b, and c:
From these axioms, Huntington derived the usual axioms of Boolean algebra. Specifically, what Huntington proved was that if we take
to interpret
Boolean join,
to interpret Boolean complement and use 
and 
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 (also called the Robbins problem), 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 a "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.
Abstract algebra
Abstract algebra is the subject area of mathematics that studies algebraic structures, such as groups, rings, fields, modules, vector spaces, and algebras...
, a Robbins algebra is an algebra containing a single binary operation
Binary operation
In mathematics, a binary operation is a calculation involving two operands, in other words, an operation whose arity is two. Examples include the familiar arithmetic operations of addition, subtraction, multiplication and division....
, usually denoted by
, and a single unary operationUnary operation
In mathematics, a unary operation is an operation with only one operand, i.e. a single input. Specifically, it is a functionf:\ A\to Awhere A is a set. In this case f is called a unary operation on A....
usually denoted by
. These operations satisfy the following axioms:For all elements a, b, and c:
- AssociativityAssociativityIn mathematics, associativity is a property of some binary operations. It means that, within an expression containing two or more occurrences in a row of the same associative operator, the order in which the operations are performed does not matter as long as the sequence of the operands is not...
:
- CommutativityCommutativityIn mathematics an operation is commutative if changing the order of the operands does not change the end result. It is a fundamental property of many binary operations, and many mathematical proofs depend on it...
:
- Robbins's axiom:
History
In 1933, Edward Huntington proposed a new set of axioms for Boolean algebras, consisting of (1) and (2) above, plus:- Huntington's axiom:
From these axioms, Huntington derived the usual axioms of Boolean algebra. Specifically, what Huntington proved was that if we take
to interpretBoolean join,
to interpret Boolean complement and use and to define Boolean meet and the constants 0 and 1, then the axioms for a Boolean algebra are satisfied.Very soon thereafter, Herbert Robbins
Herbert Robbins
Herbert Ellis Robbins was an American mathematician and statistician who did research in topology, measure theory, statistics, and a variety of other fields. He was the co-author, with Richard Courant, of What is Mathematics?, a popularization that is still in print. The Robbins lemma, used in...
posed the Robbins conjecture (also called the Robbins problem), 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 a "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
Alfred Tarski
Alfred Tarski was a Polish logician and mathematician. Educated at the University of Warsaw and a member of the Lwow-Warsaw School of Logic and the Warsaw School of Mathematics and philosophy, he emigrated to the USA in 1939, and taught and carried out research in mathematics at the University of...
, and others worked on the problem, but failed to find a proof or counterexample.
William McCune
William McCune
William McCune was an American computer scientist working in the fields of Automated reasoning, Algebra, Logic, and Formal Methods. He was best known for the development of the Otter, Prover9, and Mace4 automated reasoning systems, and the automated proof of the Robbins conjecture using the EQP...
proved the conjecture in 1996, using the automated theorem prover
Automated theorem proving
Automated theorem proving or automated deduction, currently the most well-developed subfield of automated reasoning , is the proving of mathematical theorems by a computer program.- Decidability of the problem :...
EQP
EQP
EQP, an abbreviation for equational prover, is an automated theorem proving program for equational logic, developed by the Mathematics and Computer Science Division of the Argonne National Laboratory. It was one of the provers used for solving a longstanding problem posed by Herbert Robbins,...
. 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.