Journal of Formalized Mathematics
Volume 15, 2003
University of Bialystok
Copyright (c) 2003
Association of Mizar Users
On the Two Short Axiomatizations of Ortholattices

Wioletta Truszkowska

University of Bialystok

Adam Grabowski

University of Bialystok

This work has been partially supported by CALCULEMUS grant HPRNCT200000102.
Summary.

In the paper, two short axiom systems for Boolean algebras are introduced.
In the first section we show that the single axiom (DN${}_1$) proposed
in [2] in terms of disjunction and negation
characterizes Boolean algebras. To prove that (DN${}_1$) is a single
axiom for Robbins algebras (that is, Boolean algebras as well), we
use the Otter theorem prover.
The second section contains proof that the two classical axioms
(Meredith${}_1$), (Meredith${}_2$)
proposed by Meredith [3] may also serve as a basis for
Boolean algebras.
The results will be used to characterize ortholattices.
The terminology and notation used in this paper have been
introduced in the following articles
[4]
[1]

Single Axiom for Boolean Algebras

Meredith Two Axioms for Boolean Algebras
Bibliography
 [1]
Adam Grabowski.
Robbins algebras vs. Boolean algebras.
Journal of Formalized Mathematics,
13, 2001.
 [2]
W. McCune, R. Veroff, B. Fitelson, K. Harris, A. Feist, and L. Wos.
Short single axioms for Boolean algebra.
\em Journal of Automated Reasoning, 29(1):116, 2002.
 [3]
C. A. Meredith and A. N. Prior.
Equational logic.
\em Notre Dame Journal of Formal Logic, 9:212226, 1968.
 [4]
Stanislaw Zukowski.
Introduction to lattice theory.
Journal of Formalized Mathematics,
1, 1989.
Received June 28, 2003
[
Download a postscript version,
MML identifier index,
Mizar home page]