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
University of Bialystok
This work has been partially supported by CALCULEMUS grant HPRN-CT-2000-00102.

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

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

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