:: 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;