:: On Two Alternative Axiomatizations of Lattices by McKenzie and Sholander :: by Adam Grabowski and Damian Sawicki :: :: Received June 29, 2018 :: Copyright (c) 2018-2019 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies LATTICES, EQREL_1, ROBBINS5, XBOOLE_0, SUBSET_1; notations TARSKI, STRUCT_0, LATTICES, BINOP_1, FUNCT_2; constructors BINOP_1, LATTICES; registrations RELSET_1, STRUCT_0, LATTICES, LATTICE2; requirements SUBSET, NUMERALS; begin :: Preliminaries: Sholander axiomatization reserve L for non empty LattStr; reserve v64,v65,v66,v67,v103,v3,v102,v101,v100,v2,v1,v0 for Element of L; definition let L; attr L is satisfying_Sholander_1 means :: ROBBINS5:def 1 for v0,v1,v2 holds v0 "/\" (v1 "\/" v2) = (v2 "/\" v0) "\/" (v1 "/\" v0); end; theorem :: ROBBINS5:1 L is join-absorbing & (for v0,v2,v1 holds (v0"/\"(v1"\/"v2))=((v2"/\"v0)"\/"(v1"/\"v0))) implies for v0 holds (v0"/\"v0)=v0; theorem :: ROBBINS5:2 L is join-absorbing & (for v0,v2,v1 holds (v0"/\"(v1"\/"v2))=((v2"/\"v0)"\/"(v1"/\"v0))) implies for v0 holds v0"\/"v0 = v0; :: Proofs theorem :: ROBBINS5:3 :: meet-commutative L is join-absorbing & (for v0,v2,v1 holds (v0"/\"(v1"\/"v2))=((v2"/\"v0)"\/"(v1"/\"v0))) implies for v0,v1 holds v0"/\"v1 = v1"/\"v0; :: Join-commutativity theorem :: ROBBINS5:4 L is join-absorbing & (for v0,v2,v1 holds (v0"/\"(v1"\/"v2))=((v2"/\"v0)"\/"(v1"/\"v0))) implies for v0,v1 holds v0"\/"v1=v1"\/"v0; :: Meet-associativity theorem :: ROBBINS5:5 L is join-absorbing & (for v0,v2,v1 holds (v0"/\"(v1"\/"v2))=((v2"/\"v0)"\/"(v1"/\"v0))) implies for v0,v1,v2 holds ((v0"/\"v1)"/\"v2)=(v0"/\"(v1"/\"v2)); :: Third theorem :: ROBBINS5:6 ::: trivial (for v1,v0 holds (v0"/\"(v0"\/"v1))=v0) implies for v0,v1 holds v0"/\"(v0"\/"v1)=v0; :: Sixth theorem :: ROBBINS5:7 L is join-absorbing & (for v0,v2,v1 holds (v0"/\"(v1"\/"v2))=((v2"/\"v0)"\/"(v1"/\"v0))) implies for v1,v0 holds (v0"\/"(v0"/\"v1))=v0; :: Join-associativity theorem :: ROBBINS5:8 L is join-absorbing & (for v0,v2,v1 holds (v0"/\"(v1"\/"v2))=((v2"/\"v0)"\/"(v1"/\"v0))) implies for v0,v1,v2 holds (v0"\/"v1)"\/"v2=v0"\/"(v1"\/"v2); :: Seventh file theorem :: ROBBINS5:9 L is join-absorbing & (for v0,v2,v1 holds (v0"/\"(v1"\/"v2))=((v2"/\"v0)"\/"(v1"/\"v0))) implies for v0,v1,v2 holds v0"/\"(v1"\/"v2)=(v0"/\"v1)"\/"(v0"/\"v2); :: Eighth File theorem :: ROBBINS5:10 L is join-absorbing & (for v0,v2,v1 holds (v0"/\"(v1"\/"v2))=((v2"/\"v0)"\/"(v1"/\"v0))) implies for v0,v1,v2 holds (v0"\/"(v1"/\"v2))=((v0"\/"v1)"/\"(v0"\/"v2)); :: Ordinary Eight Axioms for Distributive Lattices Imply Sholander reserve L for distributive join-commutative meet-commutative non empty LattStr; reserve v0,v1,v2 for Element of L; theorem :: ROBBINS5:11 for v0,v1,v2 holds v0 "/\" (v1 "\/" v2) = (v2 "/\" v0) "\/" (v1 "/\" v0); theorem :: ROBBINS5:12 for L being non empty LattStr holds L is distributive Lattice iff L is join-absorbing satisfying_Sholander_1; registration cluster join-absorbing satisfying_Sholander_1 -> distributive Lattice-like for non empty LattStr; cluster distributive join-commutative meet-commutative -> satisfying_Sholander_1 for non empty LattStr; end; begin :: McKenzie axiomatization of lattices reserve L for non empty LattStr; reserve v103,v3,v102,v101,v100,v2,v1,v0 for Element of L; definition let L; attr L is satisfying_McKenzie_1 means :: ROBBINS5:def 2 for v1,v2,v0 holds v0 "\/" (v1 "/\" (v0 "/\" v2)) = v0; attr L is satisfying_McKenzie_2 means :: ROBBINS5:def 3 for v1,v2,v0 holds v0 "/\" (v1 "\/" (v0 "\/" v2)) = v0; attr L is satisfying_McKenzie_3 means :: ROBBINS5:def 4 for v2,v1,v0 holds ((v0 "/\" v1) "\/" (v1 "/\" v2)) "\/" v1 = v1; attr L is satisfying_McKenzie_4 means :: ROBBINS5:def 5 for v2,v1,v0 holds ((v0 "\/" v1) "/\" (v1 "\/" v2)) "/\" v1 = v1; end; theorem :: ROBBINS5:13 (L is satisfying_McKenzie_1 satisfying_McKenzie_2 & (for v2,v1,v0 holds ((v0"/\"v1)"\/"(v1"/\"v2))"\/"v1 = v1) & (for v2,v1,v0 holds ((v0"\/"v1)"/\"(v1"\/"v2))"/\"v1 = v1)) implies ((for v1,v0 holds (v0"/\"(v0"\/"v1))=v0) & (for v1,v0 holds (v0"\/"(v0"/\"v1))=v0) & L is join-commutative meet-commutative meet-associative join-associative); theorem :: ROBBINS5:14 L is join-commutative join-associative meet-commutative meet-associative & (for v1,v0 holds (v0"/\"(v0"\/"v1))=v0) & (for v1,v0 holds (v0"\/"(v0"/\"v1))=v0) implies (for v1,v2,v0 holds (v0"\/"(v1"/\"(v0"/\"v2)))=v0) & (for v1,v2,v0 holds (v0"/\"(v1"\/"(v0"\/"v2)))=v0) & (for v2,v1,v0 holds (((v0"/\"v1)"\/"(v1"/\"v2))"\/"v1)=v1) & (for v2,v1,v0 holds (((v0"\/"v1)"/\"(v1"\/"v2))"/\"v1)=v1); definition let L be non empty LattStr; attr L is satisfying_4_McKenzie_axioms means :: ROBBINS5:def 6 L is satisfying_McKenzie_1 & L is satisfying_McKenzie_2 & L is satisfying_McKenzie_3 & L is satisfying_McKenzie_4; end; registration cluster satisfying_4_McKenzie_axioms -> satisfying_McKenzie_1 satisfying_McKenzie_2 satisfying_McKenzie_3 satisfying_McKenzie_4 for non empty LattStr; cluster satisfying_McKenzie_1 satisfying_McKenzie_2 satisfying_McKenzie_3 satisfying_McKenzie_4 -> satisfying_4_McKenzie_axioms for non empty LattStr; end; reserve L for non empty LattStr; theorem :: ROBBINS5:15 L is Lattice iff L is satisfying_4_McKenzie_axioms; registration cluster Lattice-like -> satisfying_4_McKenzie_axioms for non empty LattStr; cluster satisfying_4_McKenzie_axioms -> Lattice-like for non empty LattStr; end;