<abstract xmlns="http://www.w3.org/1999/xhtml">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
<disp-formula><alternatives><inline-graphic xmlns:xlink="http://www.w3.org/1999/xlink" xlink:href="graphic/forma-2015-0031_i1.jpg"></inline-graphic><math xmlns:mml="http://www.w3.org/1998/Math/MathML" display="block"><mrow><msup><mi>a</mi><mo>*</mo></msup><mo>⊔</mo><msup><mi>a</mi><mrow><mo>*</mo><mo>*</mo></mrow></msup><mo>=</mo><mtext>T</mtext><mo>,</mo></mrow></math><tex-math>$$a^* \sqcup a^{**} = {\rm{T}},$$</tex-math></alternatives></disp-formula>
which is fundamental for us: Stone lattices are those lattices <italic>L</italic>, which are distributive, bounded, and satisfy Stone identity for all elements <italic>a ∈ L.</italic> 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 <italic>a
*
</italic> 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 <italic>p</italic>
2 for arbitrary prime number <italic>p</italic> (Section 6). At the end we formalize the notion of the Stone lattice <italic>B</italic>
[2] (of pairs of elements <italic>a, b</italic> of <italic>B</italic> such that <italic>a</italic> ⩽ <italic>b</italic>) constructed as a sublattice of <italic>B</italic>
2, where <italic>B</italic> 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 <italic>Lattice theory for rough sets</italic> [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].</abstract>

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

Stone Lattices

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

Formalized Mathematics

This work is licensed under the Creative Commons Attribution-ShareAlike 3.0 License.

{"article-title":"Stone Lattices"}

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

Stone Lattices

Published Online: Mar 25, 2016

Page range: 387 - 396

Received: Oct 22, 2015

DOI: https://doi.org/10.1515/forma-2015-0031

Keywords
pseudocomplemented lattices, Stone lattices, Boolean lattices, lattice of natural divisors

© 2015 Adam Grabowski, published by De Gruyter Open

This work is licensed under the Creative Commons Attribution-ShareAlike 3.0 License.

Stone Lattices

Published Online: Mar 25, 2016

Page range: 387 - 396

Received: Oct 22, 2015

DOI: https://doi.org/10.1515/forma-2015-0031

Keywordspseudocomplemented lattices, Stone lattices, Boolean lattices, lattice of natural divisors

© 2015 Adam Grabowski, published by De Gruyter Open

This work is licensed under the Creative Commons Attribution-ShareAlike 3.0 License.

Keywords
pseudocomplemented lattices, Stone lattices, Boolean lattices, lattice of natural divisors