:: Axiomatization of {B}oolean Algebras Based on Sheffer Stroke
:: by Violetta Kozarkiewicz and Adam Grabowski
::
:: Received May 31, 2004
:: Copyright (c) 2004-2021 Association of Mizar Users

theorem Th1: :: SHEFFER1:1

for L being non empty join-commutative join-associative Huntington ComplLLattStr
for a, b being Element of L holds (a + b) ` = (a `) *' (b `)

proof end;

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;

:: deftheorem defines upper-bounded' SHEFFER1:def 1 :
for IT being non empty LattStr holds
( IT is upper-bounded' iff ex c being Element of IT st
for a being Element of IT holds
( c "/\" a = a & a "/\" c = a ) );

definition

let L be non empty LattStr ;
assume A1: L is upper-bounded' ;

func Top' L -> Element of L means :Def2: :: SHEFFER1:def 2
for a being Element of L holds
( it "/\" a = a & a "/\" it = a );

existence
ex b₁ being Element of L st
for a being Element of L holds
( b₁ "/\" a = a & a "/\" b₁ = a ) by A1;
uniqueness
for b₁, b₂ being Element of L st ( for a being Element of L holds
( b₁ "/\" a = a & a "/\" b₁ = a ) ) & ( for a being Element of L holds
( b₂ "/\" a = a & a "/\" b₂ = a ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def2 defines Top' SHEFFER1:def 2 :
for L being non empty LattStr st L is upper-bounded' holds
for b₂ being Element of L holds
( b₂ = Top' L iff for a being Element of L holds
( b₂ "/\" a = a & a "/\" b₂ = a ) );

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;

:: deftheorem defines lower-bounded' SHEFFER1:def 3 :
for IT being non empty LattStr holds
( IT is lower-bounded' iff ex c being Element of IT st
for a being Element of IT holds
( c "\/" a = a & a "\/" c = a ) );

definition

let L be non empty LattStr ;
assume A1: L is lower-bounded' ;

func Bot' L -> Element of L means :Def4: :: SHEFFER1:def 4
for a being Element of L holds
( it "\/" a = a & a "\/" it = a );

existence
ex b₁ being Element of L st
for a being Element of L holds
( b₁ "\/" a = a & a "\/" b₁ = a ) by A1;
uniqueness
for b₁, b₂ being Element of L st ( for a being Element of L holds
( b₁ "\/" a = a & a "\/" b₁ = a ) ) & ( for a being Element of L holds
( b₂ "\/" a = a & a "\/" b₂ = a ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def4 defines Bot' SHEFFER1:def 4 :
for L being non empty LattStr st L is lower-bounded' holds
for b₂ being Element of L holds
( b₂ = Bot' L iff for a being Element of L holds
( b₂ "\/" a = a & a "\/" b₂ = a ) );

definition

let IT be non empty LattStr ;

attr IT is distributive' means :Def5: :: SHEFFER1:def 5
for a, b, c being Element of IT holds a "\/" (b "/\" c) = (a "\/" b) "/\" (a "\/" c);

end;

:: deftheorem Def5 defines distributive' SHEFFER1:def 5 :
for IT being non empty LattStr holds
( IT is distributive' iff for a, b, c being Element of IT holds a "\/" (b "/\" c) = (a "\/" b) "/\" (a "\/" c) );

definition

let L be non empty LattStr ;
let 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;

:: deftheorem defines is_a_complement'_of SHEFFER1:def 6 :
for L being non empty LattStr
for a, b being Element of L holds
( a is_a_complement'_of b iff ( b "\/" a = Top' L & a "\/" b = Top' L & b "/\" a = Bot' L & a "/\" b = Bot' L ) );

definition

let IT be non empty LattStr ;

attr IT is complemented' means :Def7: :: SHEFFER1:def 7
for b being Element of IT ex a being Element of IT st a is_a_complement'_of b;

end;

:: deftheorem Def7 defines complemented' SHEFFER1:def 7 :
for IT being non empty LattStr holds
( IT is complemented' iff for b being Element of IT ex a being Element of IT st a is_a_complement'_of b );

definition

let L be non empty LattStr ;
let x be Element of L;
assume A1: ( L is complemented' & L is distributive & L is upper-bounded' & L is meet-commutative ) ;

func x `# -> Element of L means :Def8: :: SHEFFER1:def 8
it is_a_complement'_of x;

existence
ex b₁ being Element of L st b₁ is_a_complement'_of x by A1;
uniqueness
for b₁, b₂ being Element of L st b₁ is_a_complement'_of x & b₂ is_a_complement'_of x holds
b₁ = b₂

proof end;

end;

:: deftheorem Def8 defines `# SHEFFER1:def 8 :
for L being non empty LattStr
for x being Element of L st L is complemented' & L is distributive & L is upper-bounded' & L is meet-commutative holds
for b<sub>3</sub> being Element of L holds
( b<sub>3</sub> = x `# iff b₃ is_a_complement'_of x );

registration

cluster non empty V48() V49() 1 -element Lattice-like Boolean join-idempotent upper-bounded' lower-bounded' distributive' complemented' for LattStr ;

existence
ex b₁ being 1 -element LattStr st
( b₁ is Boolean & b₁ is join-idempotent & b₁ is upper-bounded' & b₁ is complemented' & b₁ is distributive' & b₁ is lower-bounded' & b₁ is Lattice-like )

proof end;

end;

theorem Th2: :: SHEFFER1:2

for L being non empty join-commutative meet-commutative distributive upper-bounded' distributive' complemented' LattStr
for x being Element of L holds x "\/" (x `#) = Top' L

proof end;

theorem Th3: :: SHEFFER1:3

for L being non empty join-commutative meet-commutative distributive upper-bounded' distributive' complemented' LattStr
for x being Element of L holds x "/\" (x `#) = Bot' L

proof end;

theorem Th4: :: SHEFFER1:4

for L being non empty join-commutative meet-commutative distributive join-idempotent upper-bounded' distributive' complemented' LattStr
for x being Element of L holds x "\/" (Top' L) = Top' L

proof end;

theorem Th5: :: SHEFFER1:5

for L being non empty join-commutative meet-commutative distributive join-idempotent upper-bounded' lower-bounded' distributive' complemented' LattStr
for x being Element of L holds x "/\" (Bot' L) = Bot' L

proof end;

theorem Th6: :: SHEFFER1:6

for L being non empty join-commutative meet-commutative meet-absorbing join-absorbing distributive join-idempotent LattStr
for x, y, z being Element of L holds ((x "\/" y) "\/" z) "/\" x = x

proof end;

theorem Th7: :: SHEFFER1:7

for L being non empty join-commutative meet-commutative meet-absorbing join-absorbing join-idempotent distributive' LattStr
for x, y, z being Element of L holds ((x "/\" y) "/\" z) "\/" x = x

proof end;

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;

:: deftheorem defines meet-idempotent SHEFFER1:def 9 :
for G being non empty /\-SemiLattStr holds
( G is meet-idempotent iff for x being Element of G holds x "/\" x = x );

theorem Th8: :: SHEFFER1:8

for L being non empty join-commutative meet-commutative distributive upper-bounded' lower-bounded' distributive' complemented' LattStr holds L is meet-idempotent

proof end;

theorem Th9: :: SHEFFER1:9

for L being non empty join-commutative meet-commutative distributive upper-bounded' lower-bounded' distributive' complemented' LattStr holds L is join-idempotent

proof end;

theorem Th10: :: SHEFFER1:10

for L being non empty join-commutative meet-commutative distributive join-idempotent upper-bounded' distributive' complemented' LattStr holds L is meet-absorbing

proof end;

theorem Th11: :: SHEFFER1:11

for L being non empty join-commutative meet-commutative distributive join-idempotent upper-bounded' lower-bounded' distributive' complemented' LattStr holds L is join-absorbing

proof end;

theorem Th12: :: SHEFFER1:12

for L being non empty join-commutative meet-commutative distributive join-idempotent upper-bounded' lower-bounded' distributive' complemented' LattStr holds L is upper-bounded

proof end;

theorem Th13: :: SHEFFER1:13

for L being non empty Lattice-like Boolean LattStr holds L is upper-bounded'

proof end;

theorem Th14: :: SHEFFER1:14

for L being non empty join-commutative meet-commutative distributive join-idempotent upper-bounded' lower-bounded' distributive' complemented' LattStr holds L is lower-bounded

proof end;

theorem Th15: :: SHEFFER1:15

for L being non empty Lattice-like Boolean LattStr holds L is lower-bounded'

proof end;

theorem Th16: :: SHEFFER1:16

for L being non empty join-commutative meet-commutative meet-absorbing join-absorbing distributive join-idempotent LattStr holds L is join-associative

proof end;

theorem Th17: :: SHEFFER1:17

for L being non empty join-commutative meet-commutative meet-absorbing join-absorbing join-idempotent distributive' LattStr holds L is meet-associative

proof end;

theorem Th18: :: SHEFFER1:18

for L being non empty join-commutative meet-commutative distributive join-idempotent upper-bounded' lower-bounded' distributive' complemented' LattStr holds Top L = Top' L

proof end;

theorem Th19: :: SHEFFER1:19

for L being non empty join-commutative meet-commutative distributive join-idempotent upper-bounded' lower-bounded' distributive' complemented' LattStr holds Bottom L = Bot' L

proof end;

theorem Th20: :: SHEFFER1:20

for L being non empty Lattice-like Boolean distributive' LattStr holds Top L = Top' L

proof end;

theorem Th21: :: SHEFFER1:21

for L being non empty Lattice-like distributive lower-bounded upper-bounded complemented Boolean distributive' LattStr holds Bottom L = Bot' L

proof end;

theorem :: SHEFFER1:22

for L being non empty join-commutative meet-commutative distributive join-idempotent upper-bounded' lower-bounded' distributive' complemented' LattStr
for 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: :: SHEFFER1:23

for L being non empty join-commutative meet-commutative distributive join-idempotent upper-bounded' lower-bounded' distributive' complemented' LattStr holds L is complemented

proof end;

theorem Th24: :: SHEFFER1:24

for L being non empty Lattice-like Boolean upper-bounded' lower-bounded' distributive' LattStr holds L is complemented'

proof end;

theorem Th25: :: SHEFFER1:25

for L being non empty LattStr holds
( L is Boolean Lattice iff ( L is lower-bounded' & L is upper-bounded' & L is join-commutative & L is meet-commutative & L is distributive & L is distributive' & L is complemented' ) )

proof end;

registration

cluster non empty Lattice-like Boolean -> non empty join-commutative meet-commutative distributive upper-bounded' lower-bounded' distributive' complemented' for LattStr ;

coherence
for b₁ being non empty LattStr st b₁ is Boolean & b₁ is Lattice-like holds
( b₁ is lower-bounded' & b₁ is upper-bounded' & b₁ is complemented' & b₁ is join-commutative & b₁ is meet-commutative & b₁ is distributive & b₁ is distributive' ) by Th25;

cluster non empty join-commutative meet-commutative distributive upper-bounded' lower-bounded' distributive' complemented' -> non empty Lattice-like Boolean for LattStr ;

coherence
for b₁ being non empty LattStr st b₁ is lower-bounded' & b₁ is upper-bounded' & b₁ is complemented' & b₁ is join-commutative & b₁ is meet-commutative & b₁ is distributive & b₁ is distributive' holds
( b₁ is Boolean & b₁ is Lattice-like ) by Th25;

end;

definition

attr c₁ is strict ;
struct ShefferStr -> 1-sorted ;
aggr ShefferStr(# carrier, stroke #) -> ShefferStr ;
sel stroke c₁ -> BinOp of the carrier of c₁;

end;

definition

attr c₁ is strict ;
struct ShefferLattStr -> ShefferStr , LattStr ;
aggr ShefferLattStr(# carrier, L_join, L_meet, stroke #) -> ShefferLattStr ;

end;

definition

attr c₁ is strict ;
struct ShefferOrthoLattStr -> ShefferStr , OrthoLattStr ;
aggr ShefferOrthoLattStr(# carrier, L_join, L_meet, Compl, stroke #) -> ShefferOrthoLattStr ;

end;

definition

func TrivShefferOrthoLattStr -> ShefferOrthoLattStr equals :: SHEFFER1:def 10
ShefferOrthoLattStr(# {0},op2,op2,op1,op2 #);

coherence
ShefferOrthoLattStr(# {0},op2,op2,op1,op2 #) is ShefferOrthoLattStr ;

end;

:: deftheorem defines TrivShefferOrthoLattStr SHEFFER1:def 10 :
TrivShefferOrthoLattStr = ShefferOrthoLattStr(# {0},op2,op2,op1,op2 #);

registration

cluster 1 -element for ShefferStr ;

existence
ex b₁ being ShefferStr st b₁ is 1 -element

proof end;

cluster 1 -element for ShefferLattStr ;

existence
ex b₁ being ShefferLattStr st b₁ is 1 -element

proof end;

cluster 1 -element for ShefferOrthoLattStr ;

existence
ex b₁ being ShefferOrthoLattStr st b₁ is 1 -element

proof end;

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

coherence
the stroke of L . (x,y) is Element of L ;

end;

:: deftheorem defines | SHEFFER1:def 11 :
for L being non empty ShefferStr
for x, y being Element of L holds x | y = the stroke of L . (x,y);

definition

let L be non empty ShefferOrthoLattStr ;

attr L is properly_defined means :Def12: :: 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;

:: deftheorem Def12 defines properly_defined SHEFFER1:def 12 :
for L being non empty ShefferOrthoLattStr holds
( L is properly_defined iff ( ( 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 `) ) ) );

definition

let L be non empty ShefferStr ;

attr L is satisfying_Sheffer_1 means :Def13: :: SHEFFER1:def 13
for x being Element of L holds (x | x) | (x | x) = x;

attr L is satisfying_Sheffer_2 means :Def14: :: SHEFFER1:def 14
for x, y being Element of L holds x | (y | (y | y)) = x | x;

attr L is satisfying_Sheffer_3 means :Def15: :: 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;

:: deftheorem Def13 defines satisfying_Sheffer_1 SHEFFER1:def 13 :
for L being non empty ShefferStr holds
( L is satisfying_Sheffer_1 iff for x being Element of L holds (x | x) | (x | x) = x );

:: deftheorem Def14 defines satisfying_Sheffer_2 SHEFFER1:def 14 :
for L being non empty ShefferStr holds
( L is satisfying_Sheffer_2 iff for x, y being Element of L holds x | (y | (y | y)) = x | x );

:: deftheorem Def15 defines satisfying_Sheffer_3 SHEFFER1:def 15 :
for L being non empty ShefferStr holds
( L is satisfying_Sheffer_3 iff for x, y, z being Element of L holds (x | (y | z)) | (x | (y | z)) = ((y | y) | x) | ((z | z) | x) );

registration

cluster 1 -element -> 1 -element satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 for ShefferStr ;

coherence
for b₁ being 1 -element ShefferStr holds
( b₁ is satisfying_Sheffer_1 & b₁ is satisfying_Sheffer_2 & b₁ is satisfying_Sheffer_3 ) by STRUCT_0:def 10;

end;

registration

cluster 1 -element -> 1 -element join-commutative join-associative for \/-SemiLattStr ;

coherence
for b₁ being 1 -element \/-SemiLattStr holds
( b₁ is join-commutative & b₁ is join-associative ) by STRUCT_0:def 10;

cluster 1 -element -> 1 -element meet-commutative meet-associative for /\-SemiLattStr ;

coherence
for b₁ being 1 -element /\-SemiLattStr holds
( b₁ is meet-commutative & b₁ is meet-associative ) by STRUCT_0:def 10;

end;

registration

cluster 1 -element -> 1 -element meet-absorbing join-absorbing Boolean for LattStr ;

coherence
for b₁ being 1 -element LattStr holds
( b₁ is join-absorbing & b₁ is meet-absorbing & b₁ is Boolean )

proof end;

end;

registration

cluster TrivShefferOrthoLattStr -> 1 -element ;

coherence
TrivShefferOrthoLattStr is 1 -element ;

cluster TrivShefferOrthoLattStr -> well-complemented properly_defined ;

coherence
( TrivShefferOrthoLattStr is properly_defined & TrivShefferOrthoLattStr is well-complemented )

proof end;

end;

registration

cluster non empty Lattice-like Boolean well-complemented properly_defined satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 for ShefferOrthoLattStr ;

existence
ex b₁ being non empty ShefferOrthoLattStr st
( b₁ is properly_defined & b₁ is Boolean & b₁ is well-complemented & b₁ is Lattice-like & b₁ is satisfying_Sheffer_1 & b₁ is satisfying_Sheffer_2 & b₁ is satisfying_Sheffer_3 )

proof end;

end;

theorem :: SHEFFER1:26

for L being non empty Lattice-like Boolean well-complemented properly_defined ShefferOrthoLattStr holds L is satisfying_Sheffer_1

proof end;

theorem :: SHEFFER1:27

for L being non empty Lattice-like Boolean well-complemented properly_defined ShefferOrthoLattStr holds L is satisfying_Sheffer_2

proof end;

theorem :: SHEFFER1:28

for L being non empty Lattice-like Boolean well-complemented properly_defined ShefferOrthoLattStr holds L is satisfying_Sheffer_3

proof end;

definition

let L be non empty ShefferStr ;
let a be Element of L;

func a " -> Element of L equals :: SHEFFER1:def 16
a | a;

coherence
a | a is Element of L ;

end;

:: deftheorem defines " SHEFFER1:def 16 :
for L being non empty ShefferStr
for a being Element of L holds a " = a | a;

theorem :: SHEFFER1:29

for L being non empty satisfying_Sheffer_3 ShefferOrthoLattStr
for x, y, z being Element of L holds (x | (y | z)) " = ((y ") | x) | ((z ") | x) by Def15;

theorem :: SHEFFER1:30

for L being non empty satisfying_Sheffer_1 ShefferOrthoLattStr
for x being Element of L holds x = (x ") " by Def13;

theorem Th31: :: SHEFFER1:31

for L being non empty properly_defined satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferOrthoLattStr
for x, y being Element of L holds x | y = y | x

proof end;

theorem Th32: :: SHEFFER1:32

for L being non empty properly_defined satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferOrthoLattStr
for x, y being Element of L holds x | (x | x) = y | (y | y)

proof end;

theorem Th33: :: SHEFFER1:33

for L being non empty properly_defined satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferOrthoLattStr holds L is join-commutative

proof end;

theorem Th34: :: SHEFFER1:34

for L being non empty properly_defined satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferOrthoLattStr holds L is meet-commutative

proof end;

theorem Th35: :: SHEFFER1:35

for L being non empty properly_defined satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferOrthoLattStr holds L is distributive

proof end;

theorem Th36: :: SHEFFER1:36

for L being non empty properly_defined satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferOrthoLattStr holds L is distributive'

proof end;

theorem :: SHEFFER1:37

for L being non empty properly_defined satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferOrthoLattStr holds L is Boolean Lattice

proof end;