:: Axiomatization of {B}oolean Algebras Based on Sheffer Stroke
:: by Violetta Kozarkiewicz and Adam Grabowski
::
:: Received May 31, 2004
:: Copyright (c) 2004-2017 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, ROBBINS1, XBOOLE_0, SUBSET_1, ARYTM_3, EQREL_1,
STRUCT_0, BINOP_1, FUNCT_5, RELAT_1, FUNCT_1, SHEFFER1, CARD_1;
notations TARSKI, XBOOLE_0, FUNCT_5, ORDINAL1, CARD_1, STRUCT_0, LATTICES,
BINOP_1, ROBBINS1;
constructors BINOP_1, ROBBINS1, FUNCT_5;
registrations LATTICES, LATTICE6, ROBBINS1, CARD_1, STRUCT_0;
requirements BOOLE, SUBSET, NUMERALS;
definitions LATTICES, ROBBINS1, STRUCT_0;
equalities ROBBINS1;
expansions LATTICES, ROBBINS1, STRUCT_0;
theorems STRUCT_0, ROBBINS1, LATTICES;
begin :: Preliminaries
theorem Th1:
for L being join-commutative join-associative Huntington non
empty ComplLLattStr, a, b being Element of L holds (a + b)` = a` *' b`
proof
let L be join-commutative join-associative Huntington non empty
ComplLLattStr;
let a, b be Element of L;
a + b = (a` *' b`)` by ROBBINS1:17;
hence thesis by ROBBINS1:3;
end;
begin :: Huntington's First Axiomatization of Boolean Algebras
definition
let IT be non empty LattStr;
attr IT is upper-bounded' means
ex c being Element of IT st for a
being Element of IT holds c "/\" a = a & a "/\" c = a;
end;
definition
let L be non empty LattStr;
assume
A1: L is upper-bounded';
func Top' L -> Element of L means
:Def2:
for a being Element of L holds it "/\" a = a & a "/\" it = a;
existence by A1;
uniqueness
proof
let c1,c2 be Element of L such that
A2: for a being Element of L holds c1"/\"a = a & a"/\"c1 = a and
A3: for a being Element of L holds c2"/\"a = a & a"/\"c2 = a;
thus c1 = c2"/\"c1 by A3
.= c2 by A2;
end;
end;
definition
let IT be non empty LattStr;
attr IT is lower-bounded' means
ex c being Element of IT st for a
being Element of IT holds c "\/" a = a & a "\/" c = a;
end;
definition
let L be non empty LattStr;
assume
A1: L is lower-bounded';
func Bot' L -> Element of L means
:Def4:
for a being Element of L holds it "\/" a = a & a "\/" it = a;
existence by A1;
uniqueness
proof
let c1,c2 be Element of L such that
A2: for a being Element of L holds c1"\/"a = a & a"\/"c1 = a and
A3: for a being Element of L holds c2"\/"a = a & a"\/"c2 = a;
thus c1 = c2"\/"c1 by A3
.= c2 by A2;
end;
end;
definition
let IT be non empty LattStr;
attr IT is distributive' means
:Def5:
for a, b, c being Element of IT holds
a "\/" (b "/\" c) = (a "\/" b) "/\" (a "\/" c);
end;
definition
let L be non empty LattStr, a, b be Element of L;
pred a is_a_complement'_of b means
b "\/" a = Top' L & a "\/" b = Top' L &
b "/\" a = Bot' L & a "/\" b = Bot' L;
end;
definition
let IT be non empty LattStr;
attr IT is complemented' means
:Def7:
for b being Element of IT ex a being
Element of IT st a is_a_complement'_of b;
end;
definition
let L be non empty LattStr, x be Element of L;
assume
A1: L is complemented' distributive upper-bounded' meet-commutative;
func x `# -> Element of L means
:Def8:
it is_a_complement'_of x;
existence by A1;
uniqueness
proof
let a,b be Element of L such that
A2: a is_a_complement'_of x and
A3: b is_a_complement'_of x;
b = b "/\" Top' L by A1,Def2
.= b "/\" (x "\/" a) by A2
.= (b "/\" x) "\/" (b "/\" a) by A1
.= (x "/\" b) "\/" (b "/\" a) by A1
.= (x "/\" b) "\/" (a "/\" b) by A1
.= (Bot' L) "\/" (a "/\" b) by A3
.= (a "/\" x) "\/" (a "/\" b) by A2
.= a "/\" (x "\/" b) by A1
.= a "/\" Top' L by A3
.= a by A1,Def2;
hence thesis;
end;
end;
registration
cluster Boolean join-idempotent upper-bounded' complemented' distributive'
lower-bounded' Lattice-like for 1-element LattStr;
existence
proof
set L = the 1-element Lattice;
A1: L is lower-bounded
proof
set x = the Element of L;
for y be Element of L holds x "/\" y = x & y "/\" x = x by
STRUCT_0:def 10;
hence thesis;
end;
A2: L is upper-bounded
proof
set x = the Element of L;
for y be Element of L holds x "\/" y = x & y "\/" x = x by
STRUCT_0:def 10;
hence thesis;
end;
for b being Element of L ex a being Element of L st a is_a_complement_of b
proof
let b be Element of L;
take a = b;
b "\/" a = Top L & b "/\" a = Bottom L by STRUCT_0:def 10;
hence thesis;
end;
then
A3: L is complemented;
A4: L is join-idempotent;
for b being Element of L ex a being Element of L st a is_a_complement'_of b
proof
let b be Element of L;
take a = b;
b "\/" a = Top' L & b "/\" a = Bot' L by STRUCT_0:def 10;
hence thesis;
end;
then
A5: L is complemented';
for a, b, c being Element of L holds a "/\" (b "\/" c) = (a "/\" b)
"\/" (a "/\" c) by STRUCT_0:def 10;
then
A6: L is distributive;
A7: L is lower-bounded'
proof
set x = the Element of L;
for y be Element of L holds x "\/" y = y & y "\/" x = y by
STRUCT_0:def 10;
hence thesis;
end;
A8: L is upper-bounded'
proof
set x = the Element of L;
for y be Element of L holds x "/\" y = y & y "/\" x = y by
STRUCT_0:def 10;
hence thesis;
end;
for a, b, c being Element of L holds a "\/" (b "/\" c) = (a "\/" b)
"/\" (a "\/" c) by STRUCT_0:def 10;
then L is distributive';
hence thesis by A3,A6,A1,A2,A4,A8,A5,A7;
end;
end;
theorem Th2:
for L being complemented' join-commutative meet-commutative
distributive upper-bounded' distributive' non empty LattStr for x be Element
of L holds x "\/" x `# = Top' L
proof
let L be complemented' join-commutative meet-commutative distributive
upper-bounded' distributive' non empty LattStr;
let x be Element of L;
x `# is_a_complement'_of x by Def8;
hence thesis;
end;
theorem Th3:
for L being complemented' join-commutative meet-commutative
distributive upper-bounded' distributive' non empty LattStr for x being
Element of L holds x "/\" x `# = Bot' L
proof
let L be complemented' join-commutative meet-commutative distributive
upper-bounded' distributive' non empty LattStr;
let x be Element of L;
x `# is_a_complement'_of x by Def8;
hence thesis;
end;
theorem Th4:
for L being complemented' join-commutative meet-commutative
join-idempotent distributive upper-bounded' distributive' non empty LattStr
for x being Element of L holds x "\/" Top' L = Top' L
proof
let L be complemented' join-commutative meet-commutative join-idempotent
distributive upper-bounded' distributive' non empty LattStr;
let x be Element of L;
x "\/" Top' L = (x "\/" Top' L) "/\" Top' L by Def2
.= (x "\/" Top' L) "/\" (x "\/" (x `# )) by Th2
.= x "\/" (Top' L "/\" x`# ) by Def5
.= x "\/" x `# by Def2
.= Top' L by Th2;
hence thesis;
end;
theorem Th5:
for L being complemented' join-commutative meet-commutative
join-idempotent distributive upper-bounded' lower-bounded' distributive' non
empty LattStr for x being Element of L holds x "/\" Bot' L = Bot' L
proof
let L be complemented' join-commutative meet-commutative join-idempotent
distributive upper-bounded' lower-bounded' distributive' non empty LattStr;
let x be Element of L;
x "/\" Bot' L = (x "/\" Bot' L) "\/" Bot' L by Def4
.= (x "/\" Bot' L) "\/" (x "/\" x`# ) by Th3
.= x "/\" (Bot' L "\/" x`# ) by LATTICES:def 11
.= x "/\" x`# by Def4
.= Bot' L by Th3;
hence thesis;
end;
theorem Th6:
for L being join-commutative meet-absorbing meet-commutative
join-absorbing join-idempotent distributive non empty LattStr for x, y, z
being Element of L holds ((x "\/" y) "\/" z) "/\" x = x
proof
let L be join-commutative meet-absorbing meet-commutative join-absorbing
join-idempotent distributive non empty LattStr;
let x, y, z be Element of L;
((x "\/" y) "\/" z) "/\" x = (x "/\" (x "\/" y)) "\/" (x "/\" z) by
LATTICES:def 11
.= (x "/\" x) "\/" (x "/\" y) "\/" (x "/\" z) by LATTICES:def 11
.= x "\/" (x "/\" y) "\/" (x "/\" z)
.= x "\/" (x "/\" z) by LATTICES:def 8
.= x by LATTICES:def 8;
hence thesis;
end;
theorem Th7:
for L being join-commutative meet-absorbing meet-commutative
join-absorbing join-idempotent distributive' non empty LattStr for x, y, z
being Element of L holds ((x "/\" y) "/\" z) "\/" x = x
proof
let L be join-commutative meet-absorbing meet-commutative join-absorbing
join-idempotent distributive' non empty LattStr;
let x, y, z be Element of L;
((x "/\" y) "/\" z) "\/" x = (x "\/" (x "/\" y)) "/\" (x "\/" z) by Def5
.= (x "\/" x) "/\" (x "\/" y) "/\" (x "\/" z) by Def5
.= x "/\" (x "\/" y) "/\" (x "\/" z)
.= x "/\" (x "\/" z) by LATTICES:def 9
.= x by LATTICES:def 9;
hence thesis;
end;
definition
let G be non empty /\-SemiLattStr;
attr G is meet-idempotent means
for x being Element of G holds x "/\" x = x;
end;
theorem Th8:
for L being complemented' join-commutative meet-commutative
distributive upper-bounded' lower-bounded' distributive' non empty LattStr
holds L is meet-idempotent
proof
let L be complemented' join-commutative meet-commutative distributive
upper-bounded' lower-bounded' distributive' non empty LattStr;
now
let x be Element of L;
thus x "/\" x = (x "/\" x) "\/" Bot' L by Def4
.= (x "/\" x) "\/" (x "/\" x`# ) by Th3
.= x "/\" (x "\/" x`# ) by LATTICES:def 11
.= x "/\" Top' L by Th2
.= x by Def2;
end;
hence thesis;
end;
theorem Th9:
for L being complemented' join-commutative meet-commutative
distributive upper-bounded' lower-bounded' distributive' non empty LattStr
holds L is join-idempotent
proof
let L be complemented' join-commutative meet-commutative distributive
upper-bounded' lower-bounded' distributive' non empty LattStr;
let x be Element of L;
thus x "\/" x = (x "\/" x) "/\" Top' L by Def2
.= (x "\/" x) "/\" (x "\/" x`# ) by Th2
.= x "\/" (x "/\" x`# ) by Def5
.= x "\/" Bot' L by Th3
.= x by Def4;
end;
theorem Th10:
for L being complemented' join-commutative meet-commutative
join-idempotent distributive upper-bounded' distributive' non empty LattStr
holds L is meet-absorbing
proof
let L be complemented' join-commutative meet-commutative join-idempotent
distributive upper-bounded' distributive' non empty LattStr;
let y, x be Element of L;
x "\/" (x "/\" y) = (Top' L "/\" x) "\/" (x "/\" y) by Def2
.= x "/\" (Top' L "\/" y) by LATTICES:def 11
.= x "/\" Top' L by Th4
.= x by Def2;
hence thesis;
end;
theorem Th11:
for L being complemented' join-commutative upper-bounded'
meet-commutative join-idempotent distributive distributive' lower-bounded' non
empty LattStr holds L is join-absorbing
proof
let L be complemented' join-commutative upper-bounded' meet-commutative
join-idempotent distributive distributive' lower-bounded' non empty LattStr;
let x, y be Element of L;
A1: L is meet-idempotent by Th8;
A2: L is meet-absorbing by Th10;
x "/\" (x "\/" y) = (x "/\" x) "\/" (x "/\" y) by LATTICES:def 11
.= x "\/" (x "/\" y) by A1
.= x by A2;
hence thesis;
end;
theorem Th12:
for L being complemented' join-commutative meet-commutative
upper-bounded' lower-bounded' join-idempotent distributive distributive' non
empty LattStr holds L is upper-bounded
proof
let L be complemented' join-commutative meet-commutative upper-bounded'
lower-bounded' join-idempotent distributive distributive' non empty LattStr;
ex c being Element of L st for a being Element of L holds c"\/"a = c & a
"\/"c = c
proof
take Top' L;
let a be Element of L;
thus thesis by Th4;
end;
hence thesis;
end;
theorem Th13:
for L being Boolean Lattice-like non empty LattStr holds L is
upper-bounded'
proof
let L be Boolean Lattice-like non empty LattStr;
ex c being Element of L st for a being Element of L holds c "/\" a = a &
a "/\" c = a
proof
take c = Top L;
let a be Element of L;
thus thesis;
end;
hence thesis;
end;
theorem Th14:
for L being complemented' join-commutative meet-commutative
upper-bounded' lower-bounded' join-idempotent distributive distributive' non
empty LattStr holds L is lower-bounded
proof
let L be complemented' join-commutative meet-commutative upper-bounded'
lower-bounded' join-idempotent distributive distributive' non empty LattStr;
ex c being Element of L st for a being Element of L holds c"/\"a = c & a
"/\"c = c
proof
take Bot' L;
let a be Element of L;
thus thesis by Th5;
end;
hence thesis;
end;
theorem Th15:
for L being Boolean Lattice-like non empty LattStr holds L is
lower-bounded'
proof
let L be Boolean Lattice-like non empty LattStr;
ex c being Element of L st for a being Element of L holds c "\/" a = a &
a "\/" c = a
proof
take c = Bottom L;
let a be Element of L;
thus thesis;
end;
hence thesis;
end;
theorem Th16:
for L being join-commutative meet-commutative meet-absorbing
join-absorbing join-idempotent distributive non empty LattStr holds L is
join-associative
proof
let L be join-commutative meet-commutative meet-absorbing join-absorbing
join-idempotent distributive non empty LattStr;
let x, y, z be Element of L;
A1: ((y "\/" z) "\/" x) "/\" y = (y "/\" (y "\/" z)) "\/" (y "/\" x) by
LATTICES:def 11
.= (y "/\" y) "\/" (y "/\" z) "\/" (y "/\" x) by LATTICES:def 11
.= y "\/" (y "/\" z) "\/" (y "/\" x)
.= y "\/" (y "/\" x) by LATTICES:def 8
.= y by LATTICES:def 8;
A2: ((x "\/" y) "\/" z) "/\" x = x by Th6;
x "\/" (y "\/" z) = (x "\/" y) "\/" z
proof
set A = ((x "\/" y) "\/" z) "/\" (x "\/" (y "\/" z));
A3: A = ((x "\/" y) "/\" (x "\/" (y "\/" z))) "\/" (z "/\" (x "\/" (y "\/"
z))) by LATTICES:def 11
.= ((x "\/" y) "/\" (x "\/" (y "\/" z))) "\/" z by Th6
.= ((x "/\" (x "\/" (y "\/" z))) "\/" (y "/\" (x "\/" (y "\/" z))))
"\/" z by LATTICES:def 11
.= (x "\/" y) "\/" z by A1,LATTICES:def 9;
A = (((x "\/" y) "\/" z) "/\" x) "\/" (((x "\/" y) "\/" z) "/\" (y
"\/" z)) by LATTICES:def 11
.= x "\/" ((((x "\/" y) "\/" z) "/\" y) "\/" (((x "\/" y) "\/" z) "/\"
z)) by A2,LATTICES:def 11
.= x "\/" (y "\/" (((x "\/" y) "\/" z) "/\" z)) by Th6
.= x "\/" (y "\/" (((x "\/" y ) "/\" z) "\/" (z "/\" z))) by
LATTICES:def 11
.= x "\/" (y "\/" (((x "\/" y ) "/\" z) "\/" z))
.= x "\/" (y "\/" z) by LATTICES:def 8;
hence thesis by A3;
end;
hence thesis;
end;
theorem Th17:
for L being join-commutative meet-commutative meet-absorbing
join-absorbing join-idempotent distributive' non empty LattStr holds L is
meet-associative
proof
let L be join-commutative meet-commutative meet-absorbing join-absorbing
join-idempotent distributive' non empty LattStr;
let x, y, z be Element of L;
A1: ((x "/\" y) "/\" z) "\/" x = x by Th7;
A2: ((y "/\" z) "/\" x) "\/" y = (y "\/" (y "/\" z)) "/\" (y "\/" x) by Def5
.= (y "\/" y) "/\" (y "\/" z) "/\" (y "\/" x) by Def5
.= y "/\" (y "\/" z) "/\" (y "\/" x)
.= y "/\" (y "\/" x) by LATTICES:def 9
.= y by LATTICES:def 9;
x "/\" (y "/\" z) = (x "/\" y) "/\" z
proof
set A = ((x "/\" y) "/\" z) "\/" (x "/\" (y "/\" z));
A3: A = ((x "/\" y) "\/" (x "/\" (y "/\" z))) "/\" (z "\/" (x "/\" (y "/\"
z))) by Def5
.= ((x "/\" y) "\/" (x "/\" (y "/\" z))) "/\" z by Th7
.= ((x "\/" (x "/\" (y "/\" z))) "/\" (y "\/" (x "/\" (y "/\" z))))
"/\" z by Def5
.= (x "/\" y) "/\" z by A2,LATTICES:def 8;
A = (((x "/\" y) "/\" z) "\/" x) "/\" (((x "/\" y) "/\" z) "\/" (y
"/\" z)) by Def5
.= x "/\" ((((x "/\" y) "/\" z) "\/" y) "/\" (((x "/\" y) "/\" z) "\/"
z)) by A1,Def5
.= x "/\" (y "/\" (((x "/\" y) "/\" z) "\/" z)) by Th7
.= x "/\" (y "/\" (((x "/\" y ) "\/" z) "/\" (z "\/" z))) by Def5
.= x "/\" (y "/\" (((x "/\" y ) "\/" z) "/\" z))
.= x "/\" (y "/\" z) by LATTICES:def 9;
hence thesis by A3;
end;
hence thesis;
end;
theorem Th18:
for L being complemented' join-commutative meet-commutative
lower-bounded' upper-bounded' join-idempotent distributive distributive' non
empty LattStr holds Top L = Top' L
proof
let L be complemented' join-commutative meet-commutative lower-bounded'
upper-bounded' join-idempotent distributive distributive' non empty LattStr;
set Y = Top' L;
L is upper-bounded & for a being Element of L holds Y "\/" a = Y & a
"\/" Y = Y by Th4,Th12;
hence thesis by LATTICES:def 17;
end;
theorem Th19:
for L being complemented' join-commutative meet-commutative
lower-bounded' upper-bounded' join-idempotent distributive distributive' non
empty LattStr holds Bottom L = Bot' L
proof
let L be complemented' join-commutative meet-commutative lower-bounded'
upper-bounded' join-idempotent distributive distributive' non empty LattStr;
set Y = Bot' L;
L is lower-bounded & for a being Element of L holds Y "/\" a = Y & a
"/\" Y = Y by Th5,Th14;
hence thesis by LATTICES:def 16;
end;
theorem Th20:
for L being Boolean distributive' Lattice-like non empty
LattStr holds Top L = Top' L
proof
let L be Boolean distributive' Lattice-like non empty LattStr;
set Y = Top L;
L is upper-bounded' & for a being Element of L holds Y "/\" a = a & a
"/\" Y = a by Th13;
hence thesis by Def2;
end;
theorem Th21:
for L being Boolean complemented lower-bounded upper-bounded
distributive distributive' Lattice-like non empty LattStr holds Bottom L =
Bot' L
proof
let L be Boolean complemented lower-bounded upper-bounded distributive
distributive' Lattice-like non empty LattStr;
set Y = Bottom L;
L is lower-bounded' & for a being Element of L holds Y "\/" a = a & a
"\/" Y = a by Th15;
hence thesis by Def4;
end;
theorem
for L being complemented' lower-bounded' upper-bounded'
join-commutative meet-commutative join-idempotent distributive distributive'
non empty LattStr, x, y being Element of L holds
x is_a_complement'_of y iff x is_a_complement_of y
by Th19,Th18;
theorem Th23:
for L being complemented' join-commutative meet-commutative
lower-bounded' upper-bounded' join-idempotent distributive distributive' non
empty LattStr holds L is complemented
proof
let L be complemented' join-commutative meet-commutative lower-bounded'
upper-bounded' join-idempotent distributive distributive' non empty LattStr;
for b being Element of L ex a being Element of L st a is_a_complement_of b
proof
let b be Element of L;
consider a being Element of L such that
A1: a is_a_complement'_of b by Def7;
take a;
A2: b "/\" a = Bot' L by A1;
b "\/" a = Top' L by A1;
hence a"\/"b = Top L & b"\/"a = Top L &
a"/\"b = Bottom L & b"/\"a = Bottom L by A2,Th18,Th19;
end;
hence thesis;
end;
theorem Th24:
for L being Boolean lower-bounded' upper-bounded' distributive'
Lattice-like non empty LattStr holds L is complemented'
proof
let L be Boolean lower-bounded' upper-bounded' distributive' Lattice-like
non empty LattStr;
for b being Element of L ex a being Element of L st a is_a_complement'_of b
proof
let b be Element of L;
consider a being Element of L such that
A1: a is_a_complement_of b by LATTICES:def 19;
take a;
A2: b "/\" a = Bottom L by A1;
b "\/" a = Top L by A1;
hence b "\/" a = Top' L & a "\/" b = Top' L &
b "/\" a = Bot' L & a "/\" b = Bot' L by A2,Th20,Th21;
end;
hence thesis;
end;
theorem Th25:
for L being non empty LattStr holds L is Boolean Lattice iff L
is lower-bounded' upper-bounded' join-commutative meet-commutative distributive
distributive' complemented'
proof
let L be non empty LattStr;
thus L is Boolean Lattice implies L is lower-bounded' upper-bounded'
join-commutative meet-commutative distributive distributive' complemented'
proof
assume
A1: L is Boolean Lattice;
then reconsider L9 = L as Boolean Lattice;
ex c being Element of L9 st for a being Element of L9 holds c "\/" a =
a & a "\/" c = a
proof
take Bottom L9;
thus thesis;
end;
hence
A2: L is lower-bounded';
ex c being Element of L9 st for a being Element of L9 holds c "/\" a =
a & a "/\" c = a
proof
take Top L9;
thus thesis;
end;
hence
A3: L is upper-bounded';
thus L is join-commutative meet-commutative by A1;
for a,b,c being Element of L9 holds a "/\" (b "\/" c) = (a "/\" b)
"\/" (a "/\" c) by LATTICES:def 11;
then for a, b, c being Element of L9 holds a "\/" (b "/\" c) = (a "\/" b)
"/\" (a "\/" c) by LATTICES:3;
hence L is distributive distributive';
hence thesis by A1,A2,A3,Th24;
end;
thus L is lower-bounded' upper-bounded' join-commutative meet-commutative
distributive distributive' complemented' implies L is Boolean Lattice
proof
assume L is lower-bounded' upper-bounded' join-commutative
meet-commutative distributive distributive' complemented';
then reconsider L9 = L as lower-bounded' upper-bounded' complemented'
join-commutative meet-commutative join-idempotent distributive distributive'
non empty LattStr by Th9;
A4: L9 is complemented by Th23;
A5: L9 is lower-bounded & L9 is upper-bounded by Th12,Th14;
A6: L9 is meet-absorbing join-absorbing by Th10,Th11;
then L9 is join-associative & L9 is meet-associative by Th16,Th17;
hence thesis by A5,A4,A6;
end;
end;
registration
cluster Boolean Lattice-like -> lower-bounded' upper-bounded' complemented'
join-commutative meet-commutative distributive distributive' for
non empty LattStr;
coherence by Th25;
cluster lower-bounded' upper-bounded' complemented' join-commutative
meet-commutative distributive distributive' -> Boolean Lattice-like for
non empty
LattStr;
coherence by Th25;
end;
begin :: Axiomatization Based on Sheffer Stroke
definition
struct (1-sorted) ShefferStr (# carrier -> set, stroke -> BinOp of the
carrier #);
end;
definition
struct (ShefferStr,LattStr) ShefferLattStr (# carrier -> set, L_join ->
BinOp of the carrier, L_meet -> BinOp of the carrier, stroke -> BinOp of the
carrier #);
end;
definition
struct (ShefferStr,OrthoLattStr) ShefferOrthoLattStr (# carrier -> set,
L_join -> BinOp of the carrier, L_meet -> BinOp of the carrier, Compl -> UnOp
of the carrier, stroke -> BinOp of the carrier #);
end;
definition
func TrivShefferOrthoLattStr -> ShefferOrthoLattStr equals
ShefferOrthoLattStr (# {0}, op2, op2, op1, op2 #);
coherence;
end;
registration
cluster 1-element for ShefferStr;
existence
proof
set S = {{}};
set B = the BinOp of S;
take ShefferStr (#S, B#);
thus the carrier of ShefferStr (#S, B#) is 1-element;
end;
cluster 1-element for ShefferLattStr;
existence
proof
set S = {{}};
set B = the BinOp of S;
take ShefferLattStr (#S, B, B, B#);
thus the carrier of ShefferLattStr (#S, B, B, B#) is 1-element;
end;
cluster 1-element for ShefferOrthoLattStr;
existence
proof
set S = {{}};
set B = the BinOp of S;
set A = the UnOp of S;
take ShefferOrthoLattStr (#S, B, B, A, B#);
thus the carrier of ShefferOrthoLattStr (#S, B, B, A, B#) is 1-element;
end;
end;
definition
let L be non empty ShefferStr;
let x, y be Element of L;
func x | y -> Element of L equals
(the stroke of L).(x,y);
coherence;
end;
definition
let L be non empty ShefferOrthoLattStr;
attr L is properly_defined means
:Def12:
(for x being Element of L holds x |
x = x`) & (for x, y being Element of L holds x "\/" y = (x | x) | (y | y)) & (
for x, y being Element of L holds x "/\" y = (x | y) | (x | y)) & for x, y
being Element of L holds x | y = x` + y`;
end;
definition
let L be non empty ShefferStr;
attr L is satisfying_Sheffer_1 means
:Def13:
for x being Element of L holds (x | x) | (x | x) = x;
attr L is satisfying_Sheffer_2 means
:Def14:
for x, y being Element of L holds x | (y | (y | y)) = x | x;
attr L is satisfying_Sheffer_3 means
:Def15:
for x, y, z being Element of L
holds (x | (y | z)) | (x | (y | z)) = ((y | y) | x) | ((z | z) | x);
end;
registration
cluster -> satisfying_Sheffer_1 satisfying_Sheffer_2
satisfying_Sheffer_3 for 1-element ShefferStr;
coherence
by STRUCT_0:def 10;
end;
registration
cluster -> join-commutative join-associative
for 1-element \/-SemiLattStr;
coherence
by STRUCT_0:def 10;
cluster -> meet-commutative meet-associative
for 1-element /\-SemiLattStr;
coherence
by STRUCT_0:def 10;
end;
registration
cluster -> join-absorbing meet-absorbing Boolean for 1-element LattStr;
coherence
proof
let L be 1-element LattStr;
thus L is join-absorbing
by STRUCT_0:def 10;
A1: L is upper-bounded
proof
set c = the Element of L;
take c;
let a be Element of L;
thus thesis by STRUCT_0:def 10;
end;
thus L is meet-absorbing
by STRUCT_0:def 10;
A2: L is lower-bounded
proof
set c = the Element of L;
take c;
let a be Element of L;
thus thesis by STRUCT_0:def 10;
end;
A3: L is complemented
proof
set a = the Element of L;
let b be Element of L;
take a;
A4: a "/\" b = Bottom L & b "/\" a = Bottom L by STRUCT_0:def 10;
a "\/" b = Top L & b "\/" a = Top L by STRUCT_0:def 10;
hence thesis by A4;
end;
L is distributive
by STRUCT_0:def 10;
hence thesis by A2,A1,A3;
end;
end;
registration
cluster TrivShefferOrthoLattStr -> 1-element;
coherence;
cluster TrivShefferOrthoLattStr -> properly_defined well-complemented;
coherence
proof
set L = TrivShefferOrthoLattStr;
A1: ( for x, y being Element of L holds x "/\" y = (x | y) | (x | y))& for
x, y being Element of L holds x | y = x` + y` by STRUCT_0:def 10;
( for x being Element of L holds x | x = x`)& for x, y being Element
of L holds x "\/" y = (x | x) | (y | y) by STRUCT_0:def 10;
hence L is properly_defined by A1;
L is well-complemented
proof
let a be Element of L;
thus a` "\/" a = Top L & a "\/" a` = Top L &
a` "/\" a = Bottom L & a "/\" a` = Bottom L by STRUCT_0:def 10;
end;
hence thesis;
end;
end;
registration
cluster properly_defined Boolean well-complemented Lattice-like
satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 for
non empty ShefferOrthoLattStr;
existence
proof
take TrivShefferOrthoLattStr;
thus thesis;
end;
end;
theorem
for L being properly_defined Boolean well-complemented Lattice-like
non empty ShefferOrthoLattStr holds L is satisfying_Sheffer_1
proof
let L be properly_defined Boolean well-complemented Lattice-like non empty
ShefferOrthoLattStr;
let x be Element of L;
x`` = x by ROBBINS1:3;
then (x | x)` = x by Def12;
hence thesis by Def12;
end;
theorem
for L being properly_defined Boolean well-complemented Lattice-like
non empty ShefferOrthoLattStr holds L is satisfying_Sheffer_2
proof
let L be properly_defined Boolean well-complemented Lattice-like non empty
ShefferOrthoLattStr;
let x, y be Element of L;
x` + Bot L = x` by ROBBINS1:13;
then x` + (y`` *' y`) = x` by ROBBINS1:15;
then x` + (y` + y)` = x` by Th1;
then x | (y` + y) = x` by Def12;
then x | (y` + y``) = x` by ROBBINS1:3;
then x | (y | (y`)) = x` by Def12;
then x | (y | (y | y)) = x` by Def12
.= x | x by Def12;
hence thesis;
end;
theorem
for L being properly_defined Boolean well-complemented Lattice-like
non empty ShefferOrthoLattStr holds L is satisfying_Sheffer_3
proof
let L be properly_defined Boolean well-complemented Lattice-like non empty
ShefferOrthoLattStr;
let x, y, z be Element of L;
x *' (y` + z`) = (y` *' x) + (z` *' x) by ROBBINS1:30;
then (x` + (y | z)`)` = (y` *' x) + (z` *' x) by Def12;
then (x | (y | z))` = (y` *' x) + (z` *' x) by Def12;
then (x | (y | z)) | (x | (y | z)) = (y` *' x) + (z` *' x) by Def12
.= (y` *' x``) + (z` *' x) by ROBBINS1:3
.= (y` *' x``) + (z` *' x``) by ROBBINS1:3
.= (y + x`)` + (z` *' x``) by Th1
.= (y + x`)` + (z + x`)` by Th1
.= (y + x`) | (z + x`) by Def12
.= (y`` + x`) | (z + x`) by ROBBINS1:3
.= (y`` + x`) | (z`` + x`) by ROBBINS1:3
.= (y` | x) | (z`` + x`) by Def12
.= (y` | x) | (z` | x) by Def12
.= ((y | y) | x) | (z` | x) by Def12
.= ((y | y) | x) | ((z | z) | x) by Def12;
hence thesis;
end;
definition
let L be non empty ShefferStr;
let a be Element of L;
func a" -> Element of L equals
a | a;
coherence;
end;
theorem
for L being satisfying_Sheffer_3 non empty ShefferOrthoLattStr, x, y
, z being Element of L holds (x | (y | z))" = (y" | x) | (z" | x) by Def15;
theorem
for L being satisfying_Sheffer_1 non empty ShefferOrthoLattStr, x
being Element of L holds x = (x")" by Def13;
theorem Th31:
for L being satisfying_Sheffer_1 satisfying_Sheffer_2
satisfying_Sheffer_3 properly_defined non empty ShefferOrthoLattStr, x, y
being Element of L holds x | y = y | x
proof
let L be satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3
properly_defined non empty ShefferOrthoLattStr;
let x, y be Element of L;
x | y = ((x | y)")" by Def13
.= ((x | (y")")")" by Def13
.= (((y")" |x)")" by Def15
.= ((y | x)")" by Def13
.= y | x by Def13;
hence thesis;
end;
theorem Th32:
for L being satisfying_Sheffer_1 satisfying_Sheffer_2
satisfying_Sheffer_3 properly_defined non empty ShefferOrthoLattStr, x, y
being Element of L holds x | (x | x) = y | (y | y)
proof
let L be satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3
properly_defined non empty ShefferOrthoLattStr;
let x, y be Element of L;
x | (x | x) = ((x | x") | (x | x"))" by Def13
.= ((x | x") | (y | y"))" by Def14
.= ((y | y") | (x | (x | x)))" by Th31
.= ((y | y")")" by Def14
.= y | (y | y) by Def13;
hence thesis;
end;
theorem Th33:
for L being satisfying_Sheffer_1 satisfying_Sheffer_2
satisfying_Sheffer_3 properly_defined non empty ShefferOrthoLattStr holds L
is join-commutative
proof
let L be satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3
properly_defined non empty ShefferOrthoLattStr;
let x, y be Element of L;
x "\/" y = x" | (y | y) by Def12
.= (y | y) | (x | x) by Th31
.= y "\/" x by Def12;
hence thesis;
end;
theorem Th34:
for L being satisfying_Sheffer_1 satisfying_Sheffer_2
satisfying_Sheffer_3 properly_defined non empty ShefferOrthoLattStr holds L
is meet-commutative
proof
let L be satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3
properly_defined non empty ShefferOrthoLattStr;
let x, y be Element of L;
x "/\" y = (x | y) | (x | y) by Def12
.= (y | x) | (x | y) by Th31
.= (y | x) | (y | x) by Th31
.= y "/\" x by Def12;
hence thesis;
end;
theorem Th35:
for L being satisfying_Sheffer_1 satisfying_Sheffer_2
satisfying_Sheffer_3 properly_defined non empty ShefferOrthoLattStr holds L
is distributive
proof
let L be satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3
properly_defined non empty ShefferOrthoLattStr;
let x, y, z be Element of L;
set Y = y";
set Z = z";
x "/\" (y "\/" z) = x "/\" ((y | y) | (z | z)) by Def12
.= (x | (Y | Z))" by Def12
.= (Y" | x) | (Z" | x) by Def15
.= (y | x) | (Z" | x) by Def13
.= (y | x) | (z | x) by Def13
.= (x | y) | (z | x) by Th31
.= (x | y) | (x | z) by Th31
.= ((x | y)")" | (x | z) by Def13
.= ((x | y) | (x | y))" | ((x | z)")" by Def13
.= ((x "/\" y) | ((x | y) | (x | y))) | (((x | z) | (x | z)) | ((x | z)
| (x | z))) by Def12
.= ((x "/\" y) | (x "/\" y)) | (((x | z) | (x | z)) | ((x | z) | (x | z)
)) by Def12
.= ((x "/\" y) | (x "/\" y)) | ((x "/\" z) | ((x | z) | (x | z))) by Def12
.= ((x "/\" y) | (x "/\" y)) | ((x "/\" z) | (x "/\" z)) by Def12
.= (x "/\" y) "\/" (x "/\" z) by Def12;
hence thesis;
end;
theorem Th36:
for L being satisfying_Sheffer_1 satisfying_Sheffer_2
satisfying_Sheffer_3 properly_defined non empty ShefferOrthoLattStr holds L
is distributive'
proof
let L be satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3
properly_defined non empty ShefferOrthoLattStr;
let x, y, z be Element of L;
set X = (x | x);
x "\/" (y "/\" z) = x "\/" ((y | z) | (y | z)) by Def12
.= X | ((y | z)")" by Def12
.= X | (y | z) by Def13
.= ((X |(y | z))")" by Def13
.= ((y" | X) | (z" | X))" by Def15
.= ((X | y") | (z" | X))" by Th31
.= ((X | (y | y)) | (X | z"))" by Th31
.= (((x "\/" y) | (X | (z | z))) | ((X | (y | y)) | (X | (z | z)))) by
Def12
.= (((x "\/" y) | (x "\/" z)) | ((X | (y | y)) | (X | (z | z)))) by Def12
.= (((x "\/" y) | (x "\/" z)) | ((x "\/" y) | (X | (z | z)))) by Def12
.= (((x "\/" y) | (x "\/" z)) | ((x "\/" y) | (x "\/" z))) by Def12
.= (x "\/" y) "/\" (x "\/" z) by Def12;
hence thesis;
end;
theorem
for L being satisfying_Sheffer_1 satisfying_Sheffer_2
satisfying_Sheffer_3 properly_defined non empty ShefferOrthoLattStr holds L
is Boolean Lattice
proof
let L be satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3
properly_defined non empty ShefferOrthoLattStr;
A1: L is distributive & L is distributive' by Th35,Th36;
ex c being Element of L st for a being Element of L holds c "/\" a = a &
a "/\" c = a
proof
set b = the Element of L;
take c = (b|b) | ((b|b)|(b|b));
let a be Element of L;
thus c "/\" a = a
proof
set X = b";
c "/\" a = (((b | b) | (X | X)) | a)" by Def12
.= (a | (X | (X | X)))" by Th31
.= (a | a)" by Def14
.= a by Def13;
hence thesis;
end;
thus a "/\" c = a
proof
set X = b";
a "/\" c = (a | ((b | b) | (X | X)))" by Def12
.= (a | a)" by Def14
.= a by Def13;
hence thesis;
end;
end;
then
A2: L is upper-bounded';
ex c being Element of L st for a being Element of L holds c "\/" a = a &
a "\/" c = a
proof
set b = the Element of L;
take c = (b | (b | b)) | (b | (b | b));
let a be Element of L;
c "\/" a = ((b | (b | b))")" | (a | a) by Def12
.= ((a | (a | a))")" | (a | a) by Th32
.= (a | (a | a)) | (a | a) by Def13
.= (a | a) | (a | (a | a)) by Th31
.= (a | a) | (a | a) by Def14
.= a by Def13;
hence c "\/" a = a;
a "\/" c = (a | a) | ((b | (b | b))")" by Def12
.= (a | a) | ((a | (a | a))")" by Th32
.= (a | a) | (a | (a | a)) by Def13
.= (a | a) | (a | a) by Def14
.= a by Def13;
hence a "\/" c = a;
end;
then
A3: L is lower-bounded';
for b being Element of L ex a being Element of L st a is_a_complement'_of b
proof
let b be Element of L;
set a = b | b;
take a;
A4: Top' L = (b | b) | ((b | b)|(b | b))
proof
set X = (b | b) | ((b | b)|(b | b));
for a being Element of L holds X "/\" a = a & a "/\" X = a
proof
let a be Element of L;
set Y = b";
thus X "/\" a = (((b | b) | (Y | Y)) | a)" by Def12
.= (a | (Y | (Y | Y)))" by Th31
.= (a | a)" by Def14
.= a by Def13;
thus a "/\" X = (a | ((b | b) | (Y | Y)))" by Def12
.= (a | a)" by Def14
.= a by Def13;
end;
hence thesis by A2,Def2;
end;
then
A5: b "\/" a = Top' L by Def12;
A6: Bot' L = (b | (b | b)) | (b | (b | b))
proof
set X = (b | (b | b)) | (b | (b | b));
for a being Element of L holds X "\/" a = a & a "\/" X = a
proof
let a be Element of L;
thus X "\/" a = ((b | (b | b))")" | (a | a) by Def12
.= ((a | (a | a))")" | (a | a) by Th32
.= (a | (a | a)) | (a | a) by Def13
.= (a | a) | (a | (a | a)) by Th31
.= (a | a) | (a | a) by Def14
.= a by Def13;
thus a "\/" X = (a | a) | ((b | (b | b))")" by Def12
.= (a | a) | ((a | (a | a))")" by Th32
.= (a | a) | (a | (a | a)) by Def13
.= (a | a) | (a | a) by Def14
.= a by Def13;
end;
hence thesis by A3,Def4;
end;
then
A7: b "/\" a = Bot' L by Def12;
A8: a "\/" b = ((b | b) | (b | b)) | (b | b) by Def12
.= Top' L by A4,Th31;
a "/\" b = ((b | b) | b) | ((b | b) | b) by Def12
.= (b | (b | b)) | ((b | b) | b) by Th31
.= Bot' L by A6,Th31;
hence thesis by A8,A5,A7;
end;
then
A9: L is complemented';
L is join-commutative & L is meet-commutative by Th33,Th34;
hence thesis by A3,A2,A9,A1;
end;