:: On Weakly Associative Lattices and Near Lattices :: by Damian Sawicki and Adam Grabowski :: :: Received June 30, 2021 :: Copyright (c) 2021 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 EQREL_1, LATTICES, PBOOLE, CARD_1, FUNCT_1, XXREAL_0, ZFMISC_1, SHEFFER1, LATWAL_1, ROBBINS3, XBOOLE_0, SUBSET_1, ROBBINS1, BINOP_1; notations ENUMSET1, XXREAL_0, SUBSET_1, ORDINAL1, STRUCT_0, BINOP_1, LATTICES, ROBBINS1, SHEFFER1, ROBBINS3; constructors BINOP_1, ENUMSET1, XREAL_0, SHEFFER1, ROBBINS3; registrations RELSET_1, LATTICES, XREAL_0, SUBSET_1, LATTAD_1, LATQUASI; requirements SUBSET, NUMERALS, BOOLE, REAL; begin :: Preliminaries reserve L for non empty LattStr; reserve v100,v102,v2,v1,v0,v3,v101 for Element of L; :: WAL + v0"/\"(v1"\/"(v0"\/"v2)) = v0 => LT :: WAL-1 theorem :: LATWAL_1:1 (for v0 holds v0"/\"v0 = v0) & (for v1,v0 holds v0"/\"v1 = v1"/\"v0) & (for v0 holds v0"\/"v0 = v0) & (for v1,v0 holds v0"\/"v1 = v1"\/"v0) & (for v2,v1,v0 holds ((v0"\/"v1)"/\"(v2"\/"v1))"/\"v1 = v1) & (for v2,v1,v0 holds ((v0"/\"v1)"\/"(v2"/\"v1))"\/"v1 = v1) & (for v1,v2,v0 holds v0"/\"(v1"\/"(v0"\/"v2)) = v0) implies for v0,v1,v2 holds (v0"/\"v1)"/\"v2 = v0"/\"(v1"/\"v2); :: Associativity theorem :: LATWAL_1:2 (for v0 holds v0"/\"v0 = v0) & (for v1,v0 holds v0"/\"v1 = v1"/\"v0) & (for v0 holds v0"\/"v0 = v0) & (for v1,v0 holds v0"\/"v1 = v1"\/"v0) & (for v2,v1,v0 holds ((v0"\/"v1)"/\"(v2"\/"v1))"/\"v1 = v1) & (for v2,v1,v0 holds ((v0"/\"v1)"\/"(v2"/\"v1))"\/"v1 = v1) & (for v1,v2,v0 holds v0"/\"(v1"\/"(v0"\/"v2)) = v0) implies for v0,v1,v2 holds (v0"\/"v1)"\/"v2 = v0"\/"(v1"\/"v2); :: Third theorem :: LATWAL_1:3 (for v0 holds v0"\/"v0 = v0) & (for v1,v2,v0 holds v0"/\"(v1"\/"(v0"\/"v2)) = v0) implies for v1,v2 holds v1"/\"(v1"\/"v2) = v1; :: Fourth theorem :: LATWAL_1:4 (for v1,v0 holds v0"/\"v1 = v1"/\"v0) & (for v0 holds v0"\/"v0 = v0) & (for v1,v0 holds v0"\/"v1 = v1"\/"v0) & (for v2,v1,v0 holds ((v0"/\"v1)"\/"(v2"/\"v1))"\/"v1 = v1) implies for v1,v2 holds v1"\/"(v1"/\"v2) = v1; begin :: Definition of Attributes definition let L be non empty LattStr; attr L is satisfying_W3 means :: LATWAL_1:def 1 for v2,v1,v0 being Element of L holds ((v0"\/"v1)"/\"(v2"\/"v1))"/\"v1 = v1; attr L is satisfying_W3' means :: LATWAL_1:def 2 for v2,v1,v0 being Element of L holds ((v0"/\"v1)"\/"(v2"/\"v1))"\/"v1 = v1; end; definition let L be meet-absorbing join-absorbing meet-commutative non empty LattStr; redefine attr L is satisfying_W3 means :: LATWAL_1:def 3 for v2,v1,v0 being Element of L holds v1 [= (v0"\/"v1)"/\"(v2"\/"v1); end; definition let L; redefine attr L is satisfying_W3' means :: LATWAL_1:def 4 for v2,v1,v0 holds (v0"/\"v1)"\/"(v2"/\"v1) [= v1; end; registration cluster meet-commutative join-idempotent join-commutative satisfying_W3' -> meet-Absorbing for non empty LattStr; end; registration cluster meet-commutative meet-idempotent join-commutative satisfying_W3 -> join-absorbing for non empty LattStr; end; registration cluster trivial -> satisfying_W3' for non empty LattStr; end; registration cluster satisfying_W3 satisfying_W3' join-idempotent meet-idempotent join-commutative meet-commutative for non empty LattStr; end; definition mode WeaklyAssociativeLattice is join-idempotent meet-idempotent join-commutative meet-commutative satisfying_W3 satisfying_W3' non empty LattStr; end; :: The above definition is taken from Padmanabhan and Rudeanu, Chapter 6 :: x ^ x = x x v x = x :: x ^ y = y ^ x x v y = y v x :: ((x v z) ^ (y v z)) ^ z = z ((x ^ z) v (y ^ z)) v z = z :: :: but :: :: Fried and Gratzer Some Examples of Weakly Associative Lattices states that :: x ^ x = x x v x = x :: x ^ y = y ^ x x v y = y v x :: x ^ (x v y) = x x v (x ^ y) = x :: ((x v z) ^ (y v z)) ^ z = z ((x ^ z) v (y ^ z)) v z = z :: weak-associative identities :: Absorption law can be derived from these definition mode WA_Lattice is WeaklyAssociativeLattice; end; :: Every lattice is weakly associative lattice registration cluster -> satisfying_W3' for join-associative meet-absorbing Lattice; end; definition let L be non empty LattStr; attr L is satisfying_WA means :: LATWAL_1:def 5 for x,y,z being Element of L holds x"/\"(y"\/"(x"\/"z)) = x; end; begin :: Defining WALs in terms of the ordering registration cluster meet-Absorbing meet-commutative join-commutative -> meet-absorbing for non empty LattStr; end; registration cluster -> meet-absorbing for WA_Lattice; end; begin :: On the Ordering Relation Generated by Weakly Associated Lattices reserve L for WA_Lattice; reserve x,y,z,u for Element of L; theorem :: LATWAL_1:5 x "\/" y = y iff x [= y; theorem :: LATWAL_1:6 x "/\" y = x iff x [= y; theorem :: LATWAL_1:7 x [= x; theorem :: LATWAL_1:8 x [= y & y [= x implies x = y; theorem :: LATWAL_1:9 x [= x "\/" y; :: LATTICES:5 but without associativity theorem :: LATWAL_1:10 x "/\" y [= x; :: LATTICES:5 but without associativity theorem :: LATWAL_1:11 x [= z & y [= z implies x "\/" y [= z; theorem :: LATWAL_1:12 ex z st x [= z & y [= z & for u st x [= u & y [= u holds z [= u; theorem :: LATWAL_1:13 z [= x & z [= y implies z [= x "/\" y; theorem :: LATWAL_1:14 ex z st z [= x & z [= y & for u st u [= x & u [= y holds u [= z; :: Under the assumption of (4) the following is true: theorem :: LATWAL_1:15 x [= z & y [= z implies (x "\/" y) "\/" z = x "\/" (y "\/" z); theorem :: LATWAL_1:16 z [= x & z [= y implies (x "/\" y) "/\" z = x "/\" (y "/\" z); :: WA-Lattice is a lattice iff [= is transitive theorem :: LATWAL_1:17 L is distributive & x [= y [= z implies x [= z; begin :: Distributivity Gives Associativity reserve L for non empty LattStr; reserve v0,v1,v2 for Element of L; theorem :: LATWAL_1:18 :: WAL + Distributivity -> Associativity (for v0 holds v0"/\"v0 = v0) & (for v1,v0 holds v0"/\"v1 = v1"/\"v0) & (for v0 holds v0"\/"v0 = v0) & (for v1,v0 holds v0"\/"v1 = v1"\/"v0) & (for v2,v1,v0 holds ((v0"\/"v1)"/\"(v2"\/"v1))"/\"v1 = v1) & (for v2,v1,v0 holds ((v0"/\"v1)"\/"(v2"/\"v1))"\/"v1 = v1) & (for v1,v0 holds v0"/\"(v0"\/"v1) = v0) & (for v0,v2,v1 holds v0"\/"(v1"/\"v2) = (v0"\/"v1)"/\"(v0"\/"v2)) implies for v0,v1,v2 holds (v0"\/"v1)"\/"v2 = v0"\/"(v1"\/"v2); :: If we assume distributivity (actually one of them), we get full :: lattice (via the associativity). registration cluster distributive' -> join-associative for WA_Lattice; end; begin definition let x,y be Element of {0,1,2}; func x ex123"/\" y -> Element of {0,1,2} equals :: LATWAL_1:def 6 2 if (x = 0 & y = 2) or (x = 2 & y = 0), min (x,y) if not ((x = 0 & y = 2) or (x = 2 & y = 0)); func x ex123"\/" y -> Element of {0,1,2} equals :: LATWAL_1:def 7 0 if (x = 0 & y = 2) or (x = 2 & y = 0), max (x,y) if not ((x = 0 & y = 2) or (x = 2 & y = 0)); end; definition func ex123\/ -> BinOp of {0,1,2} means :: LATWAL_1:def 8 for x,y being Element of {0,1,2} holds it.(x,y) = x ex123"\/" y; func ex123/\ -> BinOp of {0,1,2} means :: LATWAL_1:def 9 for x,y being Element of {0,1,2} holds it.(x,y) = x ex123"/\" y; end; begin :: Near Lattices :: Here the example of the near lattice. We should show :: that it breaks one of the lattice axioms definition func ExNearLattice -> non empty LattStr equals :: LATWAL_1:def 10 LattStr (#{0,1,2}, ex123\/, ex123/\ #); end; registration cluster ExNearLattice -> non join-associative non meet-associative; end; registration cluster trivial -> meet-idempotent join-commutative meet-Absorbing join-absorbing for non empty LattStr; end; definition mode NearLattice is join-idempotent meet-idempotent join-commutative meet-commutative meet-Absorbing join-absorbing non empty LattStr; end; registration cluster ExNearLattice -> join-commutative meet-commutative join-idempotent meet-idempotent join-absorbing meet-absorbing; end; registration cluster meet-absorbing -> meet-Absorbing for join-commutative meet-commutative non empty LattStr; cluster meet-Absorbing -> meet-absorbing for join-commutative meet-commutative non empty LattStr; end; theorem :: LATWAL_1:19 :: automatically accepted thanks to registrations of clusters ExNearLattice is NearLattice & not ExNearLattice is Lattice; begin :: Alternative Axioms for WAL ::: WAL-3 :: (x ^ y) v (x ^ (x v y)) = x :: (x ^ x) v (y ^ (x v x)) = x :: (x ^ y) v (y ^ (x v y)) = y :: ((x v y) ^ (z v x)) ^ x = x :: ((x ^ y) v (z ^ x)) v x = x :: implies :: x ^ x = x :: x v x = x :: x ^ y = y ^ x :: x v y = y v x reserve L for non empty LattStr; reserve v101,v100,v2,v1,v0,v102,v103,v3 for Element of L; theorem :: LATWAL_1:20 (for v1,v0 holds (v0"/\"v1)"\/"(v0"/\"(v0"\/"v1)) = v0) & (for v0,v1 holds (v0"/\"v0)"\/"(v1"/\"(v0"\/"v0)) = v0) & (for v1,v0 holds (v0"/\"v1)"\/"(v1"/\"(v0"\/"v1)) = v1) & (for v2,v1,v0 holds ((v0"\/"v1)"/\"(v2"\/"v0))"/\"v0 = v0) & (for v2,v1,v0 holds ((v0"/\"v1)"\/"(v2"/\"v0))"\/"v0 = v0) implies for v0 holds v0 "\/" v0 = v0; theorem :: LATWAL_1:21 (for v1,v0 holds (v0"/\"v1)"\/"(v0"/\"(v0"\/"v1)) = v0) & (for v0,v1 holds (v0"/\"v0)"\/"(v1"/\"(v0"\/"v0)) = v0) & (for v1,v0 holds (v0"/\"v1)"\/"(v1"/\"(v0"\/"v1)) = v1) & (for v2,v1,v0 holds ((v0"\/"v1)"/\"(v2"\/"v0))"/\"v0 = v0) & (for v2,v1,v0 holds ((v0"/\"v1)"\/"(v2"/\"v0))"\/"v0 = v0) implies for v0,v1 holds v0 "/\" v1 = v1 "/\" v0; theorem :: LATWAL_1:22 (for v1,v0 holds (v0"/\"v1)"\/"(v0"/\"(v0"\/"v1)) = v0) & (for v0,v1 holds (v0"/\"v0)"\/"(v1"/\"(v0"\/"v0)) = v0) & (for v1,v0 holds (v0"/\"v1)"\/"(v1"/\"(v0"\/"v1)) = v1) & (for v2,v1,v0 holds ((v0"\/"v1)"/\"(v2"\/"v0))"/\"v0 = v0) & (for v2,v1,v0 holds ((v0"/\"v1)"\/"(v2"/\"v0))"\/"v0 = v0) implies for v0,v1 holds v0 "\/" v1 = v1 "\/" v0; definition let L be non empty LattStr; attr L is satisfying_WAL31 means :: LATWAL_1:def 11 for v1,v0 being Element of L holds (v0"/\"v1)"\/"(v0"/\"(v0"\/"v1)) = v0; attr L is satisfying_WAL32 means :: LATWAL_1:def 12 for v0,v1 being Element of L holds (v0"/\"v0)"\/"(v1"/\"(v0"\/"v0)) = v0; attr L is satisfying_WAL33 means :: LATWAL_1:def 13 for v1,v0 being Element of L holds (v0"/\"v1)"\/"(v1"/\"(v0"\/"v1)) = v1; attr L is satisfying_WAL34 means :: LATWAL_1:def 14 for v2,v1,v0 being Element of L holds ((v0"\/"v1)"/\"(v2"\/"v0))"/\"v0 = v0; attr L is satisfying_WAL35 means :: LATWAL_1:def 15 for v2,v1,v0 being Element of L holds ((v0"/\"v1)"\/"(v2"/\"v0))"\/"v0 = v0; end; registration cluster trivial -> satisfying_WAL31 satisfying_WAL32 satisfying_WAL33 satisfying_WAL34 satisfying_WAL35 for non empty LattStr; end; registration cluster satisfying_WAL31 satisfying_WAL32 satisfying_WAL33 satisfying_WAL34 satisfying_WAL35 -> join-idempotent meet-idempotent join-commutative meet-commutative for non empty LattStr; end; begin :: Short Single Axiom for WAL: WAL-4 definition let L be non empty LattStr; attr L is satisfying_WAL4 means :: LATWAL_1:def 16 for v2,v0,v5,v4,v3,v1 being Element of L holds (((v0"/\"v1)"\/"(v1"/\"(v0"\/"v1)))"/\"v2)"\/"(((v0"/\"(((v1"/\"v3)"\/" (v4"/\"v1))"\/"v1))"\/"(((v1"/\"(((v1"\/"v3)"/\"(v4"\/"v1))"/\"v1))"\/" (v5"/\"(v1"\/"(((v1"\/"v3)"/\"(v4"\/"v1))"/\"v1))))"/\"(v0"\/" (((v1"/\"v3)"\/"(v4"/\"v1))"\/"v1))))"/\"(((v0"/\"v1)"\/" (v1"/\"(v0"\/"v1)))"\/"v2)) = v1; end; reserve L for non empty LattStr; reserve v108,v107,v106,v101,v10,v9,v8,v7,v6,v105,v102,v100, v104,v103,v5,v4,v3,v2,v1,v0 for Element of L; theorem :: LATWAL_1:23 (for v2,v0,v5,v4,v3,v1 holds ((((v0"/\"v1)"\/"(v1"/\"(v0"\/"v1)))"/\"v2)"\/"(((v0"/\"(((v1"/\"v3)"\/" (v4"/\"v1))"\/"v1))"\/"(((v1"/\"(((v1"\/"v3)"/\"(v4"\/"v1))"/\"v1))"\/"(v5"/\"( v1"\/"(( (v1"\/"v3)"/\"(v4"\/"v1))"/\"v1))))"/\"(v0"\/"(((v1"/\"v3)"\/"(v4"/\"v1))"\/"v1 ))))"/\"(( (v0"/\"v1)"\/"(v1"/\"(v0"\/"v1)))"\/"v2)))=v1) implies for v0 holds v0"/\"v0 = v0; theorem :: LATWAL_1:24 (for v2,v0,v5,v4,v3,v1 holds ((((v0"/\"v1)"\/"(v1"/\"(v0"\/"v1)))"/\"v2)"\/"(((v0"/\"(((v1"/\"v3)"\/" (v4"/\"v1))"\/"v1))"\/"(((v1"/\"(((v1"\/"v3)"/\"(v4"\/"v1))"/\"v1))"\/"(v5"/\"( v1"\/"(( (v1"\/"v3)"/\"(v4"\/"v1))"/\"v1))))"/\"(v0"\/"(((v1"/\"v3)"\/"(v4"/\"v1))"\/"v1 ))))"/\"(( (v0"/\"v1)"\/"(v1"/\"(v0"\/"v1)))"\/"v2)))=v1) implies for v0 holds v0"\/"v0 = v0; registration cluster trivial -> satisfying_WAL4 for non empty LattStr; end; registration cluster satisfying_WAL4 -> join-idempotent meet-idempotent for non empty LattStr; end;