Formalization of Ortholattices via Orthoposets

Abstract

There are two approaches to lattices used in the Mizar Mathematical Library: on the one hand, these structures are based on the set with two binary operations (with an equational characterization as in [17]). On the other hand, we may look at them as at relational structures (posets– see [12]). As the main result of this article we can state that the Mizar formalization enables us to use both approaches simultaneously (Section 3). This is especially useful because most of lemmas on ortholattices in the literature are stated in the poset setting, so we cannot use equational theorem provers in a straightforward way. We give also short equational characterization of lattices via four axioms (as it was done in [7] with the help of the Otter prover). Some corresponding results about ortholattices are also formalized.