:: Robbins Algebras vs. Boolean Algebras :: by Adam Grabowski :: :: Received June 12, 2001 :: Copyright (c) 2001-2018 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 STRUCT_0, BINOP_1, LATTICES, FUNCT_5, XBOOLE_0, SUBSET_1, FUNCT_1, ARYTM_3, EQREL_1, XXREAL_2, ARYTM_1, ROBBINS1, CARD_1; notations TARSKI, ORDINAL1, CARD_1, STRUCT_0, LATTICES, BINOP_1, FUNCT_2, FUNCT_5; constructors BINOP_1, LATTICES, FUNCT_5; registrations RELSET_1, STRUCT_0, LATTICES, LATTICE2, CARD_1; requirements SUBSET, NUMERALS; begin :: Preliminaries definition struct (1-sorted) ComplStr (# carrier -> set, Compl -> UnOp of the carrier #); end; definition struct(\/-SemiLattStr, ComplStr) ComplLLattStr (# carrier -> set, L_join -> BinOp of the carrier, Compl -> UnOp of the carrier #); end; definition struct(/\-SemiLattStr, ComplStr) ComplULattStr (# carrier -> set, L_meet -> BinOp of the carrier, Compl -> UnOp of the carrier #); end; definition struct (ComplLLattStr, LattStr) OrthoLattStr (# carrier -> set, L_join, L_meet -> BinOp of the carrier, Compl -> UnOp of the carrier #); end; definition func TrivComplLat -> strict ComplLLattStr equals :: ROBBINS1:def 1 ComplLLattStr (#{0}, op2, op1 #); end; definition func TrivOrtLat -> strict OrthoLattStr equals :: ROBBINS1:def 2 OrthoLattStr (#{0}, op2, op2, op1 #); end; registration cluster TrivComplLat -> 1-element; cluster TrivOrtLat -> 1-element; end; registration cluster strict 1-element for OrthoLattStr; cluster strict 1-element for ComplLLattStr; end; registration let L be 1-element ComplLLattStr; cluster the ComplStr of L -> 1-element; end; registration cluster strict 1-element for ComplStr; end; definition let L be non empty ComplStr; let x be Element of L; func x -> Element of L equals :: ROBBINS1:def 3 (the Compl of L).x; end; notation let L be non empty ComplLLattStr, x,y be Element of L; synonym x + y for x "\/" y; end; definition let L be non empty ComplLLattStr; let x,y be Element of L; func x *' y -> Element of L equals :: ROBBINS1:def 4 (x "\/" y); end; definition let L be non empty ComplLLattStr; attr L is Robbins means :: ROBBINS1:def 5 for x, y being Element of L holds ((x + y) + (x + y)) = x; attr L is Huntington means :: ROBBINS1:def 6 for x, y being Element of L holds (x + y ) + (x + y) = x; end; definition let G be non empty \/-SemiLattStr; attr G is join-idempotent means :: ROBBINS1:def 7 for x being Element of G holds x "\/" x = x; end; registration cluster TrivComplLat -> join-commutative join-associative Robbins Huntington join-idempotent; cluster TrivOrtLat -> join-commutative join-associative Huntington Robbins; end; registration cluster TrivOrtLat -> meet-commutative meet-associative meet-absorbing join-absorbing; end; registration cluster strict join-associative join-commutative Robbins join-idempotent Huntington for non empty ComplLLattStr; end; registration cluster strict Lattice-like Robbins Huntington for non empty OrthoLattStr; end; definition let L be join-commutative non empty ComplLLattStr, x,y be Element of L; redefine func x + y; commutativity; end; theorem :: ROBBINS1:1 :: 4.8 for L being Huntington join-commutative join-associative non empty ComplLLattStr, a, b being Element of L holds (a *' b) + (a *' b) = a; theorem :: ROBBINS1:2 :: 4.9 for L being Huntington join-commutative join-associative non empty ComplLLattStr, a being Element of L holds a + a = a + a; theorem :: ROBBINS1:3 :: 4.10 for L being join-commutative join-associative Huntington non empty ComplLLattStr, x being Element of L holds x = x; theorem :: ROBBINS1:4 :: 4.11 revised p. 557 without idempotency for L being join-commutative join-associative Huntington non empty ComplLLattStr, a, b being Element of L holds a + a = b + b; theorem :: ROBBINS1:5 :: 4.12 for L being join-commutative join-associative join-idempotent Huntington non empty ComplLLattStr ex c being Element of L st for a being Element of L holds c + a = c & a + a = c; theorem :: ROBBINS1:6 :: 4.12 for L being join-commutative join-associative join-idempotent Huntington non empty ComplLLattStr holds L is upper-bounded; registration cluster join-commutative join-associative join-idempotent Huntington -> upper-bounded for non empty ComplLLattStr; end; definition let L be join-commutative join-associative join-idempotent Huntington non empty ComplLLattStr; redefine func Top L means :: ROBBINS1:def 8 ex a being Element of L st it = a + a; end; theorem :: ROBBINS1:7 :: 4.13 for L being join-commutative join-associative join-idempotent Huntington non empty ComplLLattStr ex c being Element of L st for a being Element of L holds c *' a = c & (a + a) = c; definition let L be join-commutative join-associative non empty ComplLLattStr; let x,y be Element of L; redefine func x *' y; commutativity; end; definition let L be join-commutative join-associative join-idempotent Huntington non empty ComplLLattStr; func Bot L -> Element of L means :: ROBBINS1:def 9 for a being Element of L holds it *' a = it; end; theorem :: ROBBINS1:8 for L being join-commutative join-associative join-idempotent Huntington non empty ComplLLattStr, a being Element of L holds Bot L = (a + a); theorem :: ROBBINS1:9 for L being join-commutative join-associative join-idempotent Huntington non empty ComplLLattStr holds (Top L) = Bot L & Top L = (Bot L); theorem :: ROBBINS1:10 :: 4.14 for L being join-commutative join-associative Huntington non empty ComplLLattStr, a, b being Element of L st a = b holds a = b; theorem :: ROBBINS1:11 :: 4.15 proof without join-idempotency, no top at all for L being join-commutative join-associative Huntington non empty ComplLLattStr, a, b being Element of L holds a + (b + b) = a; theorem :: ROBBINS1:12 :: 4.5 for L being join-commutative join-associative Huntington non empty ComplLLattStr, a being Element of L holds a + a = a; registration cluster join-commutative join-associative Huntington -> join-idempotent for non empty ComplLLattStr; end; theorem :: ROBBINS1:13 :: 4.15 for L being join-commutative join-associative Huntington non empty ComplLLattStr, a being Element of L holds a + Bot L = a; theorem :: ROBBINS1:14 :: 4.16 for L being join-commutative join-associative Huntington non empty ComplLLattStr, a being Element of L holds a *' Top L = a; theorem :: ROBBINS1:15 :: 4.17 for L being join-commutative join-associative Huntington non empty ComplLLattStr, a being Element of L holds a *' a = Bot L; theorem :: ROBBINS1:16 :: 4.19 for L being join-commutative join-associative Huntington non empty ComplLLattStr, a, b, c being Element of L holds a *' (b *' c) = a *' b *' c; theorem :: ROBBINS1:17 :: 4.20 for L being join-commutative join-associative Huntington non empty ComplLLattStr, a, b being Element of L holds a + b = (a *' b); theorem :: ROBBINS1:18 :: 4.21 for L being join-commutative join-associative Huntington non empty ComplLLattStr, a being Element of L holds a *' a = a; theorem :: ROBBINS1:19 :: 4.22 for L being join-commutative join-associative Huntington non empty ComplLLattStr, a being Element of L holds a + Top L = Top L; theorem :: ROBBINS1:20 :: 4.24 for L being join-commutative join-associative Huntington non empty ComplLLattStr, a, b being Element of L holds a + (a *' b) = a; theorem :: ROBBINS1:21 :: 4.25 for L being join-commutative join-associative Huntington non empty ComplLLattStr, a, b being Element of L holds a *' (a + b) = a; theorem :: ROBBINS1:22 :: 4.26 for L being join-commutative join-associative Huntington non empty ComplLLattStr, a, b being Element of L st a + b = Top L & b + a = Top L holds a = b; theorem :: ROBBINS1:23 :: 4.27 for L being join-commutative join-associative Huntington non empty ComplLLattStr, a, b being Element of L st a + b = Top L & a *' b = Bot L holds a = b; theorem :: ROBBINS1:24 :: 4.28 for L being join-commutative join-associative Huntington non empty ComplLLattStr, a, b, c being Element of L holds (a *' b *' c) + (a *' b *' c) + (a *' b *' c) + (a *' b *' c) + (a *' b *' c) + (a *' b *' c) + (a *' b *' c) + (a *' b *' c) = Top L; theorem :: ROBBINS1:25 :: 4.29 for L being join-commutative join-associative Huntington non empty ComplLLattStr, a, b, c being Element of L holds (a *' c) *' (b *' c) = Bot L & (a *' b *' c) *' (a *' b *' c) = Bot L & (a *' b *' c) *' (a *' b *' c) = Bot L & (a *' b *' c) *' (a *' b *' c) = Bot L & (a *' b *' c) *' (a *' b *' c) = Bot L; theorem :: ROBBINS1:26 :: 4.30 for L being join-commutative join-associative Huntington non empty ComplLLattStr, a, b, c being Element of L holds (a *' b) + (a *' c) = (a *' b *' c) + (a *' b *' c) + (a *' b *' c); theorem :: ROBBINS1:27 :: 4.31 for L being join-commutative join-associative Huntington non empty ComplLLattStr, a, b, c being Element of L holds (a *' (b + c)) = (a *' b  *' c) + (a *' b *' c) + (a *' b *' c) + (a *' b *' c) + (a *' b *' c ); theorem :: ROBBINS1:28 :: 4.32 for L being join-commutative join-associative Huntington non empty ComplLLattStr, a, b, c being Element of L holds ((a *' b) + (a *' c)) + (a *' (b + c)) = Top L; theorem :: ROBBINS1:29 :: 4.33 for L being join-commutative join-associative Huntington non empty ComplLLattStr, a, b, c being Element of L holds ((a *' b) + (a *' c)) *' (a *' (b + c)) = Bot L; theorem :: ROBBINS1:30 :: 4.34 for L being join-commutative join-associative Huntington non empty ComplLLattStr, a, b, c being Element of L holds a *' (b + c) = (a *' b) + (a *' c); theorem :: ROBBINS1:31 :: 4.35 for L being join-commutative join-associative Huntington non empty ComplLLattStr, a, b, c being Element of L holds a + (b *' c) = (a + b) *' (a + c); begin :: Pre-Ortholattices definition let L be non empty OrthoLattStr; attr L is well-complemented means :: ROBBINS1:def 10 for a being Element of L holds a is_a_complement_of a; end; registration cluster TrivOrtLat -> Boolean well-complemented; end; definition mode preOrthoLattice is Lattice-like non empty OrthoLattStr; end; registration cluster strict Boolean well-complemented for preOrthoLattice; end; theorem :: ROBBINS1:32 for L being distributive well-complemented preOrthoLattice, x being Element of L holds x = x; theorem :: ROBBINS1:33 for L being bounded distributive well-complemented preOrthoLattice, x, y being Element of L holds x "/\" y = (x "\/" y); begin :: Correspondence between boolean preOrthoLattice and boolean lattice :: according to the definition given in \cite{LATTICES.ABS} definition let L be non empty ComplLLattStr; func CLatt L -> strict OrthoLattStr means :: ROBBINS1:def 11 the carrier of it = the carrier of L & the L_join of it = the L_join of L & the Compl of it = the Compl of L & for a, b being Element of L holds (the L_meet of it).(a,b) = a *' b; end; registration let L be non empty ComplLLattStr; cluster CLatt L -> non empty; end; registration let L be join-commutative non empty ComplLLattStr; cluster CLatt L -> join-commutative; end; registration let L be join-associative non empty ComplLLattStr; cluster CLatt L -> join-associative; end; registration let L be join-commutative join-associative non empty ComplLLattStr; cluster CLatt L -> meet-commutative; end; theorem :: ROBBINS1:34 for L being non empty ComplLLattStr, a, b being Element of L, a9, b9 being Element of CLatt L st a = a9 & b = b9 holds a *' b = a9 "/\" b9 & a + b = a9 "\/" b9 & a = a9; registration let L be join-commutative join-associative Huntington non empty ComplLLattStr; cluster CLatt L -> meet-associative join-absorbing meet-absorbing; end; registration let L be Huntington non empty ComplLLattStr; cluster CLatt L -> Huntington; end; registration let L be join-commutative join-associative Huntington non empty ComplLLattStr; cluster CLatt L -> lower-bounded; end; theorem :: ROBBINS1:35 for L being join-commutative join-associative Huntington non empty ComplLLattStr holds Bot L = Bottom CLatt L; registration let L be join-commutative join-associative Huntington non empty ComplLLattStr; cluster CLatt L -> complemented distributive bounded; end; begin :: Proofs according to Bernd Ingo Dahn notation let G be non empty ComplLLattStr, x be Element of G; synonym -x for x; end; definition let G be join-commutative non empty ComplLLattStr; redefine attr G is Huntington means :: ROBBINS1:def 12 for x, y being Element of G holds -(-x + -y) + -(x + -y) = y; end; definition let G be non empty ComplLLattStr; attr G is with_idempotent_element means :: ROBBINS1:def 13 ex x being Element of G st x + x = x; end; reserve G for Robbins join-associative join-commutative non empty ComplLLattStr; reserve x, y, z, u, v for Element of G; definition let G be non empty ComplLLattStr, x, y be Element of G; func \delta (x, y) -> Element of G equals :: ROBBINS1:def 14 -(-x + y); end; definition let G be non empty ComplLLattStr, x, y be Element of G; func Expand (x, y) -> Element of G equals :: ROBBINS1:def 15 \delta (x + y, \delta(x, y)); end; definition let G be non empty ComplLLattStr, x be Element of G; func x _0 -> Element of G equals :: ROBBINS1:def 16 -(-x + x); func Double x -> Element of G equals :: ROBBINS1:def 17 x + x; end; definition let G be non empty ComplLLattStr, x be Element of G; func x _1 -> Element of G equals :: ROBBINS1:def 18 x _0 + x; func x _2 -> Element of G equals :: ROBBINS1:def 19 x _0 + Double x; func x _3 -> Element of G equals :: ROBBINS1:def 20 x _0 + (Double x + x); func x _4 -> Element of G equals :: ROBBINS1:def 21 x _0 + (Double x + Double x); end; theorem :: ROBBINS1:36 \delta ((x + y), (\delta (x, y))) = y; theorem :: ROBBINS1:37 Expand (x, y) = y; theorem :: ROBBINS1:38 \delta (-x + y, z) = -(\delta (x, y) + z); theorem :: ROBBINS1:39 \delta (x, x) = x _0; theorem :: ROBBINS1:40 \delta (Double x, x _0) = x; theorem :: ROBBINS1:41 :: Lemma 1 \delta (x _2, x) = x _0; theorem :: ROBBINS1:42 x _4 + x _0 = x _3 + x _1; theorem :: ROBBINS1:43 x _3 + x _0 = x _2 + x _1; theorem :: ROBBINS1:44 x _3 + x = x _4; theorem :: ROBBINS1:45 :: Lemma 2 \delta (x _3, x _0) = x; theorem :: ROBBINS1:46 :: Left Argument Substitution -x = -y implies \delta (x, z) = \delta (y,z); theorem :: ROBBINS1:47 :: Exchange \delta (x, -y) = \delta (y, -x); theorem :: ROBBINS1:48 :: Lemma 3 \delta (x _3, x) = x _0; theorem :: ROBBINS1:49 :: Lemma 4 \delta (x _1 + x _3, x) = x _0; theorem :: ROBBINS1:50 :: Lemma 5 \delta (x _1 + x _2, x) = x _0; theorem :: ROBBINS1:51 :: Lemma 6 \delta (x _1 + x _3, x _0) = x; definition let G, x; func \beta x -> Element of G equals :: ROBBINS1:def 22 -(x _1 + x _3) + x + -(x _3); end; theorem :: ROBBINS1:52 :: Lemma 7 \delta (\beta x, x) = -x _3; theorem :: ROBBINS1:53 :: Lemma 8 \delta (\beta x, x) = -(x _1 + x _3); theorem :: ROBBINS1:54 :: Winker Second Condition ex y, z st -(y + z) = -z; begin :: Proofs according to Bill McCune theorem :: ROBBINS1:55 (for z holds --z = z) implies G is Huntington; theorem :: ROBBINS1:56 G is with_idempotent_element implies G is Huntington; registration cluster TrivComplLat -> with_idempotent_element; end; registration cluster with_idempotent_element -> Huntington for Robbins join-associative join-commutative non empty ComplLLattStr; end; theorem :: ROBBINS1:57 (ex c, d being Element of G st c + d = c) implies G is Huntington; theorem :: ROBBINS1:58 ex y, z st y + z = z; registration cluster Robbins -> Huntington for join-associative join-commutative non empty ComplLLattStr; end; definition let L be non empty OrthoLattStr; attr L is de_Morgan means :: ROBBINS1:def 23 for x, y being Element of L holds x "/\" y = (x "\/" y); end; registration let L be non empty ComplLLattStr; cluster CLatt L -> de_Morgan; end; theorem :: ROBBINS1:59 for L being well-complemented join-commutative meet-commutative non empty OrthoLattStr, x being Element of L holds x + x = Top L & x "/\" x = Bottom L; theorem :: ROBBINS1:60 for L being bounded distributive well-complemented preOrthoLattice holds (Top L)` = Bottom L; registration cluster TrivOrtLat -> de_Morgan; end; registration cluster strict de_Morgan Boolean Robbins Huntington for preOrthoLattice; end; registration cluster join-associative join-commutative de_Morgan -> meet-commutative for non empty OrthoLattStr; end; theorem :: ROBBINS1:61 for L being Huntington de_Morgan preOrthoLattice holds Bot L = Bottom L; registration cluster Boolean -> Huntington for well-complemented preOrthoLattice; end; registration cluster Huntington -> Boolean for de_Morgan preOrthoLattice; end; registration cluster Robbins de_Morgan -> Boolean for preOrthoLattice; cluster Boolean -> Robbins for well-complemented preOrthoLattice; end;