<abstract xmlns="http://www.w3.org/1999/xhtml"><p>The main result of the article is to prove formally that two sets of axioms, proposed by McKenzie and Sholander, axiomatize lattices and distributive lattices, respectively. In our Mizar article we used proof objects generated by Prover9. We continue the work started in <xref ref-type="bibr" rid="j_forma-2018-0017_ref_007_w2aab3b7b9b1b6b1ab1ab7Aa">[7]</xref>, <xref ref-type="bibr" rid="j_forma-2018-0017_ref_021_w2aab3b7b9b1b6b1ab1ac21Aa">[21]</xref>, and <xref ref-type="bibr" rid="j_forma-2018-0017_ref_013_w2aab3b7b9b1b6b1ab1ac13Aa">[13]</xref> of developing lattice theory as initialized in <xref ref-type="bibr" rid="j_forma-2018-0017_ref_022_w2aab3b7b9b1b6b1ab1ac22Aa">[22]</xref> as a formal counterpart of <xref ref-type="bibr" rid="j_forma-2018-0017_ref_011_w2aab3b7b9b1b6b1ab1ac11Aa">[11]</xref>. Complete formal proofs can be found in the Mizar source code of this article available in the Mizar Mathematical Library (MML).</p></abstract>

The main result of the article is to prove formally that two sets of axioms, proposed by McKenzie and Sholander, axiomatize lattices and distributive lattices, respectively. In our Mizar article we used proof objects generated by Prover9. We continue the work started in [7], [21], and [13] of developing lattice theory as initialized in [22] as a formal counterpart of [11]. Complete formal proofs can be found in the Mizar source code of this article available in the Mizar Mathematical Library (MML).

On Two Alternative Axiomatizations of Lattices by McKenzie and Sholander

Formalized Mathematics

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

{"article-title":"On Two Alternative Axiomatizations of Lattices by McKenzie and Sholander"}

The main result of the article is to prove formally that two sets of axioms, proposed by McKenzie and Sholander, axiomatize lattices and distributive lattices,...

On Two Alternative Axiomatizations of Lattices by McKenzie and Sholander

Publicado en línea: 24 dic 2018

Páginas: 193 - 198

Aceptado: 29 jun 2018

DOI: https://doi.org/10.2478/forma-2018-0017

Palabras clave
lattice, distributive lattice, lattice axioms

© 2018 Adam Grabowski et al., published by Sciendo

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

On Two Alternative Axiomatizations of Lattices by McKenzie and Sholander

Publicado en línea: 24 dic 2018

Páginas: 193 - 198

Aceptado: 29 jun 2018

DOI: https://doi.org/10.2478/forma-2018-0017

Palabras clavelattice, distributive lattice, lattice axioms

© 2018 Adam Grabowski et al., published by Sciendo

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

Palabras clave
lattice, distributive lattice, lattice axioms