Stone Lattices

• Autorzy: Adam Grabowski
• Języki publikacji: EN

Abstrakty

EN

The article continues the formalization of the lattice theory (as structures with two binary operations, not in terms of ordering relations). In the paper, the notion of a pseudocomplement in a lattice is formally introduced in Mizar, and based on this we define the notion of the skeleton and the set of dense elements in a pseudocomplemented lattice, giving the meet-decomposition of arbitrary element of a lattice as the infimum of two elements: one belonging to the skeleton, and the other which is dense. The core of the paper is of course the idea of Stone identity [...] a*⊔a**=T, $$a^* \sqcup a^{**} = {\rm{T}},$$ which is fundamental for us: Stone lattices are those lattices L, which are distributive, bounded, and satisfy Stone identity for all elements a ∈ L. Stone algebras were introduced by Grätzer and Schmidt in [18]. Of course, the pseudocomplement is unique (if exists), so in a pseudcomplemented lattice we defined a * as the Mizar functor (unary operation mapping every element to its pseudocomplement). In Section 2 we prove formally a collection of ordinary properties of pseudocomplemented lattices. All Boolean lattices are Stone, and a natural example of the lattice which is Stone, but not Boolean, is the lattice of all natural divisors of p 2 for arbitrary prime number p (Section 6). At the end we formalize the notion of the Stone lattice B [2] (of pairs of elements a, b of B such that a ⩽ b) constructed as a sublattice of B 2, where B is arbitrary Boolean algebra (and we describe skeleton and the set of dense elements in such lattices). In a natural way, we deal with Cartesian product of pseudocomplemented lattices. Our formalization was inspired by [17], and is an important step in formalizing Jouni Järvinen Lattice theory for rough sets [19], so it follows rather the latter paper. We deal essentially with Section 4.3, pages 423–426. The description of handling complemented structures in Mizar [6] can be found in [12]. The current article together with [15] establishes the formal background for algebraic structures which are important for [10], [16] by means of mechanisms of merging theories as described in [11].

Słowa kluczowe

EN

pseudocomplemented lattices; Stone lattices; Boolean lattices; lattice of natural divisors

Kategorie tematyczne

• 03B35: Mechanization of proofs and logical operations
• 06D15: Pseudocomplemented lattices
• 06E75: Generalizations of Boolean algebras

• Wydawca: De Gruyter Open
• Czasopismo: Formalized Mathematics
• Rocznik: 2015
• Tom: 23
• Numer: 4
• Strony: 387-396

Daty

wydano

2015-12-01

otrzymano

2015-10-22

online

2016-03-25

Twórcy

autor

Adam Grabowski

• Institute of Informatics, University of Białystok, Ciołkowskiego 1M, 15-245 Białystok, Poland

Bibliografia

• [1] Grzegorz Bancerek. Cardinal numbers. Formalized Mathematics, 1(2):377–382, 1990.
• [2] Grzegorz Bancerek. Filters – part II. Quotient lattices modulo filters and direct product of two lattices. Formalized Mathematics, 2(3):433–438, 1991.
• [3] Grzegorz Bancerek. Ideals. Formalized Mathematics, 5(2):149–156, 1996.
• [4] Grzegorz Bancerek. Complete lattices. Formalized Mathematics, 2(5):719–725, 1991.
• [5] Grzegorz Bancerek. The ordinal numbers. Formalized Mathematics, 1(1):91–96, 1990.
• [6] Grzegorz Bancerek, Czesław Byliński, Adam Grabowski, Artur Korniłowicz, Roman Matuszewski, Adam Naumowicz, Karol Pąk, and Josef Urban. Mizar: State-of-the-art and beyond. In Manfred Kerber, Jacques Carette, Cezary Kaliszyk, Florian Rabe, and Volker Sorge, editors, Intelligent Computer Mathematics, volume 9150 of Lecture Notes in Computer Science, pages 261–279. Springer International Publishing, 2015. ISBN 978-3-319-20614-1. doi:10.1007/978-3-319-20615-8 17.[Crossref]
• [7] Czesław Byliński. Some basic properties of sets. Formalized Mathematics, 1(1):47–53, 1990.
• [8] Marek Chmur. The lattice of natural numbers and the sublattice of it. The set of prime numbers. Formalized Mathematics, 2(4):453–459, 1991.
• [9] Agata Darmochwał. Finite sets. Formalized Mathematics, 1(1):165–167, 1990.
• [10] Adam Grabowski. On the computer-assisted reasoning about rough sets. In B. Dunin-Kęplicz, A. Jankowski, A. Skowron, and M. Szczuka, editors, International Workshop on Monitoring, Security, and Rescue Techniques in Multiagent Systems Location, volume 28 of Advances in Soft Computing, pages 215–226, Berlin, Heidelberg, 2005. Springer-Verlag. doi:10.1007/3-540-32370-8 15.[Crossref]
• [11] Adam Grabowski. Efficient rough set theory merging. Fundamenta Informaticae, 135(4): 371–385, 2014. doi:10.3233/FI-2014-1129.[Crossref][WoS]
• [12] Adam Grabowski. Mechanizing complemented lattices within Mizar system. Journal of Automated Reasoning, 55:211–221, 2015. doi:10.1007/s10817-015-9333-5.[Crossref]
• [13] Adam Grabowski. Prime filters and ideals in distributive lattices. Formalized Mathematics, 21(3):213–221, 2013. doi:10.2478/forma-2013-0023.[Crossref]
• [14] Adam Grabowski. On square-free numbers. Formalized Mathematics, 21(2):153–162, 2013. doi:10.2478/forma-2013-0017.[Crossref]
• [15] Adam Grabowski. Two axiomatizations of Nelson algebras. Formalized Mathematics, 23 (2):115–125, 2015. doi:10.1515/forma-2015-0012.[Crossref]
• [16] Adam Grabowski and Magdalena Jastrzębska. Rough set theory from a math-assistant perspective. In Rough Sets and Intelligent Systems Paradigms, International Conference, RSEISP 2007, Warsaw, Poland, June 28–30, 2007, Proceedings, pages 152–161, 2007. doi:10.1007/978-3-540-73451-2 17.[Crossref]
• [17] George Grätzer. Lattice Theory: Foundation. Birkhäuser, 2011.
• [18] George Grätzer and E.T. Schmidt. On a problem of M.H. Stone. Acta Mathematica Academiae Scientarum Hungaricae, (8):455–460, 1957.
• [19] Jouni Järvinen. Lattice theory for rough sets. Transactions of Rough Sets, VI, Lecture Notes in Computer Science, 4374:400–498, 2007.
• [20] Magdalena Jastrzębska and Adam Grabowski. On the properties of the Möbius function. Formalized Mathematics, 14(1):29–36, 2006. doi:10.2478/v10037-006-0005-0.[Crossref]
• [21] Jolanta Kamieńska and Jarosław Stanisław Walijewski. Homomorphisms of lattices, finite join and finite meet. Formalized Mathematics, 4(1):35–40, 1993.
• [22] Rafał Kwiatek. Factorial and Newton coefficients. Formalized Mathematics, 1(5):887–890, 1990.
• [23] Rafał Kwiatek and Grzegorz Zwara. The divisibility of integers and integer relatively primes. Formalized Mathematics, 1(5):829–832, 1990.
• [24] Robert Milewski. More on the lattice of many sorted equivalence relations. Formalized Mathematics, 5(4):565–569, 1996.
• [25] Andrzej Trybulec. Enumerated sets. Formalized Mathematics, 1(1):25–34, 1990.
• [26] Michał J. Trybulec. Integers. Formalized Mathematics, 1(3):501–505, 1990.
• [27] Zinaida Trybulec. Properties of subsets. Formalized Mathematics, 1(1):67–71, 1990.
• [28] Stanisław Żukowski. Introduction to lattice theory. Formalized Mathematics, 1(1):215–222, 1990.

Identyfikatory

DOI

10.1515/forma-2015-0031

bwmeta1.id-class.MML

LATSTONE