Journal of Formalized Mathematics
Volume 13, 2001
University of Bialystok
Copyright (c) 2001 Association of Mizar Users

## Robbins Algebras vs. Boolean Algebras

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

The terminology and notation used in this paper have been introduced in the following articles [11] [12] [10] [1] [2] [3] [9]

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

Received June 12, 2001