abstract algebra In mathematics, more specifically algebra, abstract algebra or modern algebra is the study of algebraic structures, which are set (mathematics), sets with specific operation (mathematics), operations acting on their elements. Algebraic structur ...

, a Robbins algebra is an

algebra Algebra is a branch of mathematics that deals with abstract systems, known as algebraic structures, and the manipulation of expressions within those systems. It is a generalization of arithmetic that introduces variables and algebraic ope ...

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, a binary operation ...

, usually denoted by

\lor

, and a single

unary operation In mathematics, a 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 ...

usually denoted by

\neg

satisfying 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 that rearranging the parentheses in an expression will not change the result. In propositional logic, associativity is a Validity (logic), valid rule of replaceme ...

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. Perhaps most familiar as a p ...

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 variable (mathematics), variables are the truth values ''true'' and ''false'', usually denot ...

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 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. 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 ...

, 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 ma ...

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