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.

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

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.