:: Axiomatization of {B}oolean Algebras Based on Sheffer Stroke
:: by Violetta Kozarkiewicz and Adam Grabowski
::
:: Received May 31, 2004
:: Copyright (c) 2004-2016 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;
begin :: Preliminaries
theorem :: SHEFFER1:1
for L being join-commutative join-associative Huntington non
empty ComplLLattStr, a, b being Element of L holds (a + b)` = a` *' b`;
begin :: Huntington's First Axiomatization of Boolean Algebras
definition
let IT be non empty LattStr;
attr IT is upper-bounded' means
:: SHEFFER1:def 1
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
L is upper-bounded';
func Top' L -> Element of L means
:: SHEFFER1:def 2
for a being Element of L holds it "/\" a = a & a "/\" it = a;
end;
definition
let IT be non empty LattStr;
attr IT is lower-bounded' means
:: SHEFFER1:def 3
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
L is lower-bounded';
func Bot' L -> Element of L means
:: SHEFFER1:def 4
for a being Element of L holds it "\/" a = a & a "\/" it = a;
end;
definition
let IT be non empty LattStr;
attr IT is distributive' means
:: SHEFFER1:def 5
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
:: SHEFFER1:def 6
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
:: SHEFFER1:def 7
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
L is complemented' distributive upper-bounded' meet-commutative;
func x `# -> Element of L means
:: SHEFFER1:def 8
it is_a_complement'_of x;
end;
registration
cluster Boolean join-idempotent upper-bounded' complemented' distributive'
lower-bounded' Lattice-like for 1-element LattStr;
end;
theorem :: SHEFFER1:2
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;
theorem :: SHEFFER1:3
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;
theorem :: SHEFFER1:4
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;
theorem :: SHEFFER1:5
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;
theorem :: SHEFFER1:6
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;
theorem :: SHEFFER1:7
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;
definition
let G be non empty /\-SemiLattStr;
attr G is meet-idempotent means
:: SHEFFER1:def 9
for x being Element of G holds x "/\" x = x;
end;
theorem :: SHEFFER1:8
for L being complemented' join-commutative meet-commutative
distributive upper-bounded' lower-bounded' distributive' non empty LattStr
holds L is meet-idempotent;
theorem :: SHEFFER1:9
for L being complemented' join-commutative meet-commutative
distributive upper-bounded' lower-bounded' distributive' non empty LattStr
holds L is join-idempotent;
theorem :: SHEFFER1:10
for L being complemented' join-commutative meet-commutative
join-idempotent distributive upper-bounded' distributive' non empty LattStr
holds L is meet-absorbing;
theorem :: SHEFFER1:11
for L being complemented' join-commutative upper-bounded'
meet-commutative join-idempotent distributive distributive' lower-bounded' non
empty LattStr holds L is join-absorbing;
theorem :: SHEFFER1:12
for L being complemented' join-commutative meet-commutative
upper-bounded' lower-bounded' join-idempotent distributive distributive' non
empty LattStr holds L is upper-bounded;
theorem :: SHEFFER1:13
for L being Boolean Lattice-like non empty LattStr holds L is
upper-bounded';
theorem :: SHEFFER1:14
for L being complemented' join-commutative meet-commutative
upper-bounded' lower-bounded' join-idempotent distributive distributive' non
empty LattStr holds L is lower-bounded;
theorem :: SHEFFER1:15
for L being Boolean Lattice-like non empty LattStr holds L is
lower-bounded';
theorem :: SHEFFER1:16
for L being join-commutative meet-commutative meet-absorbing
join-absorbing join-idempotent distributive non empty LattStr holds L is
join-associative;
theorem :: SHEFFER1:17
for L being join-commutative meet-commutative meet-absorbing
join-absorbing join-idempotent distributive' non empty LattStr holds L is
meet-associative;
theorem :: SHEFFER1:18
for L being complemented' join-commutative meet-commutative
lower-bounded' upper-bounded' join-idempotent distributive distributive' non
empty LattStr holds Top L = Top' L;
theorem :: SHEFFER1:19
for L being complemented' join-commutative meet-commutative
lower-bounded' upper-bounded' join-idempotent distributive distributive' non
empty LattStr holds Bottom L = Bot' L;
theorem :: SHEFFER1:20
for L being Boolean distributive' Lattice-like non empty
LattStr holds Top L = Top' L;
theorem :: SHEFFER1:21
for L being Boolean complemented lower-bounded upper-bounded
distributive distributive' Lattice-like non empty LattStr holds Bottom L =
Bot' L;
theorem :: SHEFFER1:22
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;
theorem :: SHEFFER1:23
for L being complemented' join-commutative meet-commutative
lower-bounded' upper-bounded' join-idempotent distributive distributive' non
empty LattStr holds L is complemented;
theorem :: SHEFFER1:24
for L being Boolean lower-bounded' upper-bounded' distributive'
Lattice-like non empty LattStr holds L is complemented';
theorem :: SHEFFER1:25
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';
registration
cluster Boolean Lattice-like -> lower-bounded' upper-bounded' complemented'
join-commutative meet-commutative distributive distributive' for
non empty LattStr;
cluster lower-bounded' upper-bounded' complemented' join-commutative
meet-commutative distributive distributive' -> Boolean Lattice-like for
non empty
LattStr;
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
:: SHEFFER1:def 10
ShefferOrthoLattStr (# {0}, op2, op2, op1, op2 #);
end;
registration
cluster 1-element for ShefferStr;
cluster 1-element for ShefferLattStr;
cluster 1-element for ShefferOrthoLattStr;
end;
definition
let L be non empty ShefferStr;
let x, y be Element of L;
func x | y -> Element of L equals
:: SHEFFER1:def 11
(the stroke of L).(x,y);
end;
definition
let L be non empty ShefferOrthoLattStr;
attr L is properly_defined means
:: SHEFFER1:def 12
(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
:: SHEFFER1:def 13
for x being Element of L holds (x | x) | (x | x) = x;
attr L is satisfying_Sheffer_2 means
:: SHEFFER1:def 14
for x, y being Element of L holds x | (y | (y | y)) = x | x;
attr L is satisfying_Sheffer_3 means
:: SHEFFER1:def 15
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;
end;
registration
cluster -> join-commutative join-associative
for 1-element \/-SemiLattStr;
cluster -> meet-commutative meet-associative
for 1-element /\-SemiLattStr;
end;
registration
cluster -> join-absorbing meet-absorbing Boolean for 1-element LattStr;
end;
registration
cluster TrivShefferOrthoLattStr -> 1-element;
cluster TrivShefferOrthoLattStr -> properly_defined well-complemented;
end;
registration
cluster properly_defined Boolean well-complemented Lattice-like
satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 for
non empty ShefferOrthoLattStr;
end;
theorem :: SHEFFER1:26
for L being properly_defined Boolean well-complemented Lattice-like
non empty ShefferOrthoLattStr holds L is satisfying_Sheffer_1;
theorem :: SHEFFER1:27
for L being properly_defined Boolean well-complemented Lattice-like
non empty ShefferOrthoLattStr holds L is satisfying_Sheffer_2;
theorem :: SHEFFER1:28
for L being properly_defined Boolean well-complemented Lattice-like
non empty ShefferOrthoLattStr holds L is satisfying_Sheffer_3;
definition
let L be non empty ShefferStr;
let a be Element of L;
func a" -> Element of L equals
:: SHEFFER1:def 16
a | a;
end;
theorem :: SHEFFER1:29
for L being satisfying_Sheffer_3 non empty ShefferOrthoLattStr, x, y
, z being Element of L holds (x | (y | z))" = (y" | x) | (z" | x);
theorem :: SHEFFER1:30
for L being satisfying_Sheffer_1 non empty ShefferOrthoLattStr, x
being Element of L holds x = (x")";
theorem :: SHEFFER1:31
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;
theorem :: SHEFFER1:32
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);
theorem :: SHEFFER1:33
for L being satisfying_Sheffer_1 satisfying_Sheffer_2
satisfying_Sheffer_3 properly_defined non empty ShefferOrthoLattStr holds L
is join-commutative;
theorem :: SHEFFER1:34
for L being satisfying_Sheffer_1 satisfying_Sheffer_2
satisfying_Sheffer_3 properly_defined non empty ShefferOrthoLattStr holds L
is meet-commutative;
theorem :: SHEFFER1:35
for L being satisfying_Sheffer_1 satisfying_Sheffer_2
satisfying_Sheffer_3 properly_defined non empty ShefferOrthoLattStr holds L
is distributive;
theorem :: SHEFFER1:36
for L being satisfying_Sheffer_1 satisfying_Sheffer_2
satisfying_Sheffer_3 properly_defined non empty ShefferOrthoLattStr holds L
is distributive';
theorem :: SHEFFER1:37
for L being satisfying_Sheffer_1 satisfying_Sheffer_2
satisfying_Sheffer_3 properly_defined non empty ShefferOrthoLattStr holds L
is Boolean Lattice;