:: Axiomatization of {B}oolean Algebras Based on Sheffer Stroke
:: by Violetta Kozarkiewicz and Adam Grabowski
::
:: 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 b1 being Element of L st
for a being Element of L holds
( b1 "/\" a = a & a "/\" b1 = a )
by A1;
uniqueness
for b1, b2 being Element of L st ( for a being Element of L holds
( b1 "/\" a = a & a "/\" b1 = a ) ) & ( for a being Element of L holds
( b2 "/\" a = a & a "/\" b2 = a ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines Top' SHEFFER1:def 2 :
for L being non empty LattStr st L is upper-bounded' holds
for b2 being Element of L holds
( b2 = Top' L iff for a being Element of L holds
( b2 "/\" a = a & a "/\" b2 = 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 b1 being Element of L st
for a being Element of L holds
( b1 "\/" a = a & a "\/" b1 = a )
by A1;
uniqueness
for b1, b2 being Element of L st ( for a being Element of L holds
( b1 "\/" a = a & a "\/" b1 = a ) ) & ( for a being Element of L holds
( b2 "\/" a = a & a "\/" b2 = a ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def4 defines Bot' SHEFFER1:def 4 :
for L being non empty LattStr st L is lower-bounded' holds
for b2 being Element of L holds
( b2 = Bot' L iff for a being Element of L holds
( b2 "\/" a = a & a "\/" b2 = 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 b1 being Element of L st b1 is_a_complement'_of x
by A1;
uniqueness
for b1, b2 being Element of L st b1 is_a_complement'_of x & b2 is_a_complement'_of x holds
b1 = b2
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 b3 being Element of L holds
( b3 = x # iff b3 is_a_complement'_of x );

registration
existence
ex b1 being 1 -element LattStr st
( b1 is Boolean & b1 is join-idempotent & b1 is upper-bounded' & b1 is complemented' & b1 is distributive' & b1 is lower-bounded' & b1 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
proof end;

theorem Th9: :: SHEFFER1:9
proof end;

theorem Th10: :: SHEFFER1:10
proof end;

theorem Th11: :: SHEFFER1:11
proof end;

theorem Th12: :: SHEFFER1:12
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
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
proof end;

theorem Th17: :: SHEFFER1:17
proof end;

theorem Th18: :: SHEFFER1:18
proof end;

theorem Th19: :: SHEFFER1:19
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
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 ;

theorem Th23: :: SHEFFER1:23
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
coherence
for b1 being non empty LattStr st b1 is Boolean & b1 is Lattice-like holds
( b1 is lower-bounded' & b1 is upper-bounded' & b1 is complemented' & b1 is join-commutative & b1 is meet-commutative & b1 is distributive & b1 is distributive' )
by Th25;
coherence
for b1 being non empty LattStr st b1 is lower-bounded' & b1 is upper-bounded' & b1 is complemented' & b1 is join-commutative & b1 is meet-commutative & b1 is distributive & b1 is distributive' holds
( b1 is Boolean & b1 is Lattice-like )
by Th25;
end;

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

definition end;

definition end;

definition
coherence ;
end;

:: deftheorem defines TrivShefferOrthoLattStr SHEFFER1:def 10 :

registration
existence
ex b1 being ShefferStr st b1 is 1 -element
proof end;
existence
ex b1 being ShefferLattStr st b1 is 1 -element
proof end;
existence
ex b1 being ShefferOrthoLattStr st b1 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
coherence
for b1 being 1 -element ShefferStr holds
( b1 is satisfying_Sheffer_1 & b1 is satisfying_Sheffer_2 & b1 is satisfying_Sheffer_3 )
by STRUCT_0:def 10;
end;

registration
coherence
for b1 being 1 -element \/-SemiLattStr holds
( b1 is join-commutative & b1 is join-associative )
by STRUCT_0:def 10;
coherence
for b1 being 1 -element /\-SemiLattStr holds
( b1 is meet-commutative & b1 is meet-associative )
by STRUCT_0:def 10;
end;

registration
coherence
for b1 being 1 -element LattStr holds
( b1 is join-absorbing & b1 is meet-absorbing & b1 is Boolean )
proof end;
end;

registration
coherence ;
coherence
proof end;
end;

registration
existence
ex b1 being non empty ShefferOrthoLattStr st
( b1 is properly_defined & b1 is Boolean & b1 is well-complemented & b1 is Lattice-like & b1 is satisfying_Sheffer_1 & b1 is satisfying_Sheffer_2 & b1 is satisfying_Sheffer_3 )
proof end;
end;

theorem :: SHEFFER1:26
proof end;

theorem :: SHEFFER1:27
proof end;

theorem :: SHEFFER1:28
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
proof end;

theorem Th34: :: SHEFFER1:34
proof end;

theorem Th35: :: SHEFFER1:35
proof end;

theorem Th36: :: SHEFFER1:36
proof end;

theorem :: SHEFFER1:37
proof end;