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 HPRN-CT-2000-00102.


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.

MML Identifier: ROBBINS2

The terminology and notation used in this paper have been introduced in the following articles [4] [1]

Contents (PDF format)

  1. Single Axiom for Boolean Algebras
  2. Meredith Two Axioms for Boolean Algebras


[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):1--16, 2002.
[3] C. A. Meredith and A. N. Prior. Equational logic. \em Notre Dame Journal of Formal Logic, 9:212--226, 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]