Robbins Algebras vs. Boolean Algebras

Adam Grabowski

University of Bialystok

Summary.

In the early 1930s, Huntington proposed several axiom systems for Boolean algebras. Robbins slightly changed one of them and asked if the resulted system is still a basis for variety of Boolean algebras. The solution (afirmative answer) was given in 1996 by McCune with the help of automated theorem prover EQP/{\sc Otter}. Some simplified and restucturized versions of this proof are known. In our version of proof that all Robbins algebras are Boolean we use the results of McCune [8], Huntington [5], [7], [6] and Dahn [4].

This work has been partially supported by TYPES grant IST-1999-29001.

MML Identifier: ROBBINS1

Contents (PDF format)

1. Preliminaries
2. Pre-Ortholattices
3. Correspondence between Boolean Pre-OrthoLattices and Boolean Lattices
4. Proofs according to Bernd Ingo Dahn
5. Proofs according to William McCune

Bibliography

[1] Czeslaw Bylinski. Binary operations. Journal of Formalized Mathematics, 1, 1989.

[2] Czeslaw Bylinski. Functions and their basic properties. Journal of Formalized Mathematics, 1, 1989.

[3] Czeslaw Bylinski. Functions from a set to a set. Journal of Formalized Mathematics, 1, 1989.

[4] B. I. Dahn. Robbins algebras are Boolean: A revision of McCune's computer-generated solution of Robbins problem. \em Journal of Algebra, 208:526--532, 1998.

[5] E. V. Huntington. Sets of independent postulates for the algebra of logic. \em Trans. AMS, 5:288--309, 1904.

[6] E. V. Huntington. Boolean algebra. A correction. \em Trans. AMS, 35:557--558, 1933.

[7] E. V. Huntington. New sets of independent postulates for the algebra of logic, with special reference to Whitehead and Russell's Principia Mathematica. \em Trans. AMS, 35:274--304, 1933.

[8] W. McCune. Solution of the Robbins problem. \em Journal of Automated Reasoning, 19:263--276, 1997.

[9] Michal Muzalewski. Midpoint algebras. Journal of Formalized Mathematics, 1, 1989.

[10] Michal Muzalewski. Construction of rings and left-, right-, and bi-modules over a ring. Journal of Formalized Mathematics, 2, 1990.

[11] Andrzej Trybulec. Tarski Grothendieck set theory. Journal of Formalized Mathematics, Axiomatics, 1989.

[12] Stanislaw Zukowski. Introduction to lattice theory. Journal of Formalized Mathematics, 1, 1989.