Boolean algebra

:For a basic intro to sets, Boolean operations, Venn diagrams, truth tables, and Boolean applications, see Boolean logic.

Axiomatic Bases for Boolean algebras

Of particular interest to algebraists and logicians working with Boolean algebras is the discovery and subsequent proof of additional axiomatic bases for BA. Intuitively, one may understand an axiomatic basis B of a theory T as a set of equations whose deductive closure is the set C of all derivable proofs from B such that C=T. Thus, if a given theory has a known axiomatization (as Boolean algebras do as described earlier in this treatise), it is of central mathematical interest to then find a shorter axiomatization which characterizes the same theory. This is of both aesthetic and practical interest: A shorter axiomatization may be very beautiful, may (in few cases) help with finding shorter proofs, and most importantly, it may shed new light upon the fundamental truths of the theory, delivering new, profound intuitions. A nice example is that of both Huntington and Robbins Algebras.

Related Topics:
Axiomatic - Proofs

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

In 1933, E.V. Huntington showed the following axiomatization to be a basis for Boolean algebra:

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

• commutativity: x+y = y+x.
• associativity: (x+y)+z = x+(y+z).
• Huntington equation: n(n(x)+y) + n(n(x)+n(y)) = x.

The unary functional symbol n may be read as complement.

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

Herbert Robbins then posed the following question: Can the Huntington equation be shortened as follows, and is this new equation, together with associativity and commutativity, a basis for Boolean algebra? With this collection of axioms called a Robbins algebra, the question then becomes: Is every Robbins algebra a Boolean algebra?

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

Axiomatization for Robbins algebra:

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

• commutativity: x+y = y+x.
• associativity: (x+y)+z = x+(y+z).
• Robbins Equation: n(n(x+y)+n(x+n(y))) = x.

This question remained open since the 1930s, and became a favorite question of Alfred Tarski and his students. In 1996, William McCune at Argonne National Laboratory, building upon the work of Larry Wos, Steve Winker, and Bob Veroff, answered this long-standing question in the affirmative: Every Robbins algebra is a Boolean algebra! This work was done using McCune's automated reasoning program EQP and is a remarkable achievement.

~ ~ ~ ~ ~ ~ ~ ~ ~ ~