Journal of Formalized Mathematics
Volume 13, 2001
University of Bialystok
Copyright (c) 2001
Association of Mizar Users
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 IST199929001.
The terminology and notation used in this paper have been
introduced in the following articles
[11]
[12]
[10]
[1]
[2]
[3]
[9]

Preliminaries

PreOrtholattices

Correspondence between Boolean PreOrthoLattices and Boolean Lattices

Proofs according to Bernd Ingo Dahn

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
computergenerated solution of Robbins problem.
\em Journal of Algebra, 208:526532, 1998.
 [5]
E. V. Huntington.
Sets of independent postulates for the algebra of logic.
\em Trans. AMS, 5:288309, 1904.
 [6]
E. V. Huntington.
Boolean algebra. A correction.
\em Trans. AMS, 35:557558, 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:274304, 1933.
 [8]
W. McCune.
Solution of the Robbins problem.
\em Journal of Automated Reasoning, 19:263276, 1997.
 [9]
Michal Muzalewski.
Midpoint algebras.
Journal of Formalized Mathematics,
1, 1989.
 [10]
Michal Muzalewski.
Construction of rings and left, right, and bimodules 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
[
Download a postscript version,
MML identifier index,
Mizar home page]