:: Axiomatization of {B}oolean Algebras Based on Sheffer Stroke :: by Violetta Kozarkiewicz and Adam Grabowski :: :: Received May 31, 2004 :: Copyright (c) 2004-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 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;