On the Two Short Axiomatizations of Ortholattices
Wioletta Truszkowska, Adam Grabowski · 2003
Summary. In the paper, two short axiom systems for Boolean algebras are introduced. In the first section we show that the single axiom (DN1) proposed in [2] in terms of disjunction and negation characterizes Boolean algebras. To prove that (DN1) 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 (Meredith1), (Meredith2) proposed by Meredith [3] may also serve as a basis for Boolean algebras. The results will be used to characterize ortholattices. MML Identifier:ROBBINS2. WWW:http://mizar.org/JFM/Vol15/robbins2.html The articles [4] and [1] provide the notation and terminology for this paper. 1. SINGLE AXIOM FOR BOOLEAN ALGEBRAS Let L be a non empty complemented lattice structure. We say that L satisfies (DN1) if and only if: (Def. 1) For all elements x, y, z, u of L holds (((x+y) c + z) c +(x+(z c +(z+u) c) c) c) c = z. Let us mention that TrivComplLat satisfies (DN1) and TrivOrtLat satisfies (DN1). One can verify that there exists a non empty complemented lattice structure which is joincommutative and join-associative and satisfies (DN1). Next we state a number of propositions: (1) Let L be a non empty complemented lattice structure satisfying (DN1) and x, y, z, u, v be elements of L. Then ((x+y) c +(((z+u) c + x) c +(y c +(y+v) c) c) c) c = y. (2) Let L be a non empty complemented lattice structure satisfying (DN1) and x, y, z, u be elements of L. Then ((x+y) c +((z+x) c +(y c +(y+u) c) c) c) c = y. (3) Let L be a non empty complemented lattice structure satisfying (DN1) and x be an element of L. Then ((x+x c) c + x) c = x c. (4) Let L be a non empty complemented lattice structure satisfying (DN1) and x, y, z, u be