abstract algebra In mathematics, more specifically algebra, abstract algebra or modern algebra is the study of algebraic structures. Algebraic structures include groups, rings, fields, modules, vector spaces, lattices, and algebras over a field. The ter ...

, a Robbins algebra is an

algebra Algebra () is one of the broad areas of mathematics. Roughly speaking, algebra is the study of mathematical symbols and the rules for manipulating these symbols in formulas; it is a unifying thread of almost all of mathematics. Elementary ...

containing a single

binary operation In mathematics, a binary operation or dyadic operation is a rule for combining two elements (called operands) to produce another element. More formally, a binary operation is an operation of arity two. More specifically, an internal binary op ...

, usually denoted by

\lor

, and a single

unary operation In mathematics, an unary operation is an operation with only one operand, i.e. a single input. This is in contrast to binary operations, which use two operands. An example is any function , where is a set. The function is a unary operation o ...

usually denoted by

\neg

. These operations satisfy the following

axioms An axiom, postulate, or assumption is a statement that is taken to be true, to serve as a premise or starting point for further reasoning and arguments. The word comes from the Ancient Greek word (), meaning 'that which is thought worthy or f ...

: For all elements ''a'', ''b'', and ''c'': #

Associativity In mathematics, the associative property is a property of some binary operations, which means that rearranging the parentheses in an expression will not change the result. In propositional logic, associativity is a valid rule of replacement ...

a \lor \left(b \lor c \right) = \left(a \lor b \right) \lor c

Commutativity In mathematics, a binary operation is commutative if changing the order of the operands does not change the result. It is a fundamental property of many binary operations, and many mathematical proofs depend on it. Most familiar as the name of ...

a \lor b = b \lor a

# ''Robbins equation'':

\neg \left( \neg \left(a \lor b \right) \lor \neg \left(a \lor \neg b \right) \right) = a

For many years, it was conjectured, but unproven, that all Robbins algebras are

Boolean algebra In mathematics and mathematical logic, Boolean algebra is a branch of algebra. It differs from elementary algebra in two ways. First, the values of the variables are the truth values ''true'' and ''false'', usually denoted 1 and 0, whereas i ...

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: *''Huntington's equation'':

\neg(\neg a \lor b) \lor \neg(\neg a \lor \neg b) = a.

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

Herbert Robbins Herbert Ellis Robbins (January 12, 1915 – February 12, 2001) was an American mathematician and statistician. He did research in topology, measure theory, statistics, and a variety of other fields. He was the co-author, with Richard Co ...

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

\lor

would interpret Boolean

join Join may refer to: * Join (law), to include additional counts or additional defendants on an indictment *In mathematics: ** Join (mathematics), a least upper bound of sets orders in lattice theory ** Join (topology), an operation combining two topo ...

and

\neg

Boolean

complement A complement is something that completes something else. Complement may refer specifically to: The arts * Complement (music), an interval that, when added to another, spans an octave ** Aggregate complementation, the separation of pitch-clas ...

. 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 Alfred Tarski (, born Alfred Teitelbaum;School of Mathematics and Statistics, University of St Andrews ''School of Mathematics and Statistics, University of St Andrews''. January 14, 1901 – October 26, 1983) was a Polish-American logician a ...

, 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 Automated theorem proving (also known as ATP or automated deduction) is a subfield of automated reasoning and mathematical logic dealing with proving mathematical theorems by computer programs. Automated reasoning over mathematical proof was a m ...

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
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)
A Complete Proof of the Robbins Conjecture.
* William McCune,
Robbins Algebras Are Boolean
" With links to proofs and other papers. {{DEFAULTSORT:Robbins Algebra Boolean algebra Formal methods Computer-assisted proofs

History

See also

References