:: SHEFFER1 semantic presentation

theorem Th1: :: SHEFFER1:1

for b₁ being non empty join-commutative join-associative Huntington ComplLattStr
for b₂, b₃ being Element of b₁ holds (b₂ + b₃) ` = (b₂ ` ) *' (b₃ ` )

proof end;

theorem Th2: :: SHEFFER1:2

for b₁ being non empty join-commutative join-associative Huntington ComplLattStr
for b₂, b₃ being Element of b₁ holds (b₂ *' b₃) ` = (b₂ ` ) + (b₃ ` ) by ROBBINS1:3;

definition

let c₁ be non empty LattStr ;
attr a₁ is upper-bounded' means :Def1: :: SHEFFER1:def 1
ex b₁ being Element of a₁ st
for b₂ being Element of a₁ holds
( b₁ "/\" b₂ = b₂ & b₂ "/\" b₁ = b₂ );

end;

:: deftheorem Def1 defines upper-bounded' SHEFFER1:def 1 :

definition

let c₁ be non empty LattStr ;
assume E3: c₁ is upper-bounded' ;
func Top' c₁ -> Element of a₁ means :Def2: :: SHEFFER1:def 2
for b₁ being Element of a₁ holds
( a₂ "/\" b₁ = b₁ & b₁ "/\" a₂ = b₁ );
existence by E3, Def1;
uniqueness

proof end;

end;

:: deftheorem Def2 defines Top' SHEFFER1:def 2 :

definition

let c₁ be non empty LattStr ;
attr a₁ is lower-bounded' means :Def3: :: SHEFFER1:def 3
ex b₁ being Element of a₁ st
for b₂ being Element of a₁ holds
( b₁ "\/" b₂ = b₂ & b₂ "\/" b₁ = b₂ );

end;

:: deftheorem Def3 defines lower-bounded' SHEFFER1:def 3 :

definition

let c₁ be non empty LattStr ;
assume E5: c₁ is lower-bounded' ;
func Bot' c₁ -> Element of a₁ means :Def4: :: SHEFFER1:def 4
for b₁ being Element of a₁ holds
( a₂ "\/" b₁ = b₁ & b₁ "\/" a₂ = b₁ );
existence by E5, Def3;
uniqueness

proof end;

end;

:: deftheorem Def4 defines Bot' SHEFFER1:def 4 :

definition

let c₁ be non empty LattStr ;
attr a₁ is distributive' means :Def5: :: SHEFFER1:def 5
for b₁, b₂, b₃ being Element of a₁ holds b₁ "\/" (b₂ "/\" b₃) = (b₁ "\/" b₂) "/\" (b₁ "\/" b₃);

end;

:: deftheorem Def5 defines distributive' SHEFFER1:def 5 :

definition

let c₁ be non empty LattStr ;
let c₂, c₃ be Element of c₁;
pred c₂ is_a_complement'_of c₃ means :Def6: :: SHEFFER1:def 6
( a₃ "\/" a₂ = Top' a₁ & a₂ "\/" a₃ = Top' a₁ & a₃ "/\" a₂ = Bot' a₁ & a₂ "/\" a₃ = Bot' a₁ );

end;

:: deftheorem Def6 defines is_a_complement'_of SHEFFER1:def 6 :

definition

let c₁ be non empty LattStr ;
attr a₁ is complemented' means :Def7: :: SHEFFER1:def 7
for b₁ being Element of a₁ ex b₂ being Element of a₁ st b₂ is_a_complement'_of b₁;

end;

:: deftheorem Def7 defines complemented' SHEFFER1:def 7 :

definition

let c₁ be non empty LattStr ;
let c₂ be Element of c₁;
assume E9: ( c₁ is complemented' & c₁ is distributive & c₁ is upper-bounded' & c₁ is meet-commutative ) ;
func c₂ `# -> Element of a₁ means :Def8: :: SHEFFER1:def 8
a₃ is_a_complement'_of a₂;
existence by E9, Def7;
uniqueness

proof end;

end;

:: deftheorem Def8 defines `# SHEFFER1:def 8 :

registration

cluster non empty Lattice-like Boolean join-idempotent upper-bounded' lower-bounded' distributive' complemented' LattStr ;
existence

proof end;

end;

theorem Th3: :: SHEFFER1:3

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

proof end;

theorem Th4: :: SHEFFER1:4

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

proof end;

theorem Th5: :: SHEFFER1:5

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

proof end;

theorem Th6: :: SHEFFER1:6

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

proof end;

theorem Th7: :: SHEFFER1:7

for b₁ being non empty join-commutative meet-commutative meet-absorbing join-absorbing distributive join-idempotent LattStr
for b₂, b₃, b₄ being Element of b₁ holds ((b₂ "\/" b₃) "\/" b₄) "/\" b₂ = b₂

proof end;

theorem Th8: :: SHEFFER1:8

for b₁ being non empty join-commutative meet-commutative meet-absorbing join-absorbing join-idempotent distributive' LattStr
for b₂, b₃, b₄ being Element of b₁ holds ((b₂ "/\" b₃) "/\" b₄) "\/" b₂ = b₂

proof end;

definition

let c₁ be non empty /\-SemiLattStr ;
attr a₁ is meet-idempotent means :Def9: :: SHEFFER1:def 9
for b₁ being Element of a₁ holds b₁ "/\" b₁ = b₁;

end;

:: deftheorem Def9 defines meet-idempotent SHEFFER1:def 9 :

theorem Th9: :: SHEFFER1:9

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

proof end;

theorem Th10: :: SHEFFER1:10

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

proof end;

theorem Th11: :: SHEFFER1:11

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

proof end;

theorem Th12: :: SHEFFER1:12

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

proof end;

theorem Th13: :: SHEFFER1:13

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

proof end;

theorem Th14: :: SHEFFER1:14

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

proof end;

theorem Th15: :: SHEFFER1:15

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

proof end;

theorem Th16: :: SHEFFER1:16

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

proof end;

theorem Th17: :: SHEFFER1:17

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

proof end;

theorem Th18: :: SHEFFER1:18

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

proof end;

theorem Th19: :: SHEFFER1:19

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

proof end;

theorem Th20: :: SHEFFER1:20

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

proof end;

theorem Th21: :: SHEFFER1:21

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

proof end;

theorem Th22: :: SHEFFER1:22

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

proof end;

theorem Th23: :: SHEFFER1:23

for b₁ being non empty join-commutative meet-commutative distributive join-idempotent upper-bounded' lower-bounded' distributive' complemented' LattStr
for b₂, b₃ being Element of b₁ holds
( b₂ is_a_complement'_of b₃ iff b₂ is_a_complement_of b₃ )

proof end;

theorem Th24: :: SHEFFER1:24

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

proof end;

theorem Th25: :: SHEFFER1:25

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

proof end;

theorem Th26: :: SHEFFER1:26

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

proof end;

registration

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

end;

definition

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

end;

definition

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

end;

definition

attr a₁ 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(# {{} },op2 ,op2 ,op1 ,op2 #);
coherence ;

end;

:: deftheorem Def10 defines TrivShefferOrthoLattStr SHEFFER1:def 10 :

registration

cluster non empty ShefferStr ;
existence

proof end;

cluster non empty ShefferLattStr ;
existence

proof end;

cluster non empty ShefferOrthoLattStr ;
existence

proof end;

end;

definition

let c₁ be non empty ShefferStr ;
let c₂, c₃ be Element of c₁;
func c₂ | c₃ -> Element of a₁ equals :: SHEFFER1:def 11
the stroke of a₁ . a₂,a₃;
coherence ;

end;

:: deftheorem Def11 defines | SHEFFER1:def 11 :

definition

let c₁ be non empty ShefferOrthoLattStr ;
attr a₁ is properly_defined means :Def12: :: SHEFFER1:def 12
( ( for b₁ being Element of a₁ holds b₁ | b₁ = b₁ ` ) & ( for b₁, b₂ being Element of a₁ holds b₁ "\/" b₂ = (b₁ | b₁) | (b₂ | b₂) ) & ( for b₁, b₂ being Element of a₁ holds b₁ "/\" b₂ = (b₁ | b₂) | (b₁ | b₂) ) & ( for b₁, b₂ being Element of a₁ holds b₁ | b₂ = (b₁ ` ) + (b₂ ` ) ) );

end;

:: deftheorem Def12 defines properly_defined SHEFFER1:def 12 :

definition

let c₁ be non empty ShefferStr ;
attr a₁ is satisfying_Sheffer_1 means :Def13: :: SHEFFER1:def 13
for b₁ being Element of a₁ holds (b₁ | b₁) | (b₁ | b₁) = b₁;
attr a₁ is satisfying_Sheffer_2 means :Def14: :: SHEFFER1:def 14
for b₁, b₂ being Element of a₁ holds b₁ | (b₂ | (b₂ | b₂)) = b₁ | b₁;
attr a₁ is satisfying_Sheffer_3 means :Def15: :: SHEFFER1:def 15
for b₁, b₂, b₃ being Element of a₁ holds (b₁ | (b₂ | b₃)) | (b₁ | (b₂ | b₃)) = ((b₂ | b₂) | b₁) | ((b₃ | b₃) | b₁);

end;

:: deftheorem Def13 defines satisfying_Sheffer_1 SHEFFER1:def 13 :

:: deftheorem Def14 defines satisfying_Sheffer_2 SHEFFER1:def 14 :

:: deftheorem Def15 defines satisfying_Sheffer_3 SHEFFER1:def 15 :

registration

cluster non empty trivial -> non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr ;
coherence

proof end;

end;

registration

cluster non empty trivial -> non empty join-commutative join-associative \/-SemiLattStr ;
coherence

proof end;

cluster non empty trivial -> non empty meet-commutative meet-associative /\-SemiLattStr ;
coherence

proof end;

end;

registration

cluster non empty trivial -> non empty meet-absorbing join-absorbing Boolean LattStr ;
coherence

proof end;

end;

registration end;

registration

cluster non empty join-commutative meet-commutative Lattice-like distributive Boolean well-complemented upper-bounded' lower-bounded' distributive' complemented' properly_defined satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferOrthoLattStr ;
existence

proof end;

end;

theorem Th27: :: SHEFFER1:27

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

proof end;

theorem Th28: :: SHEFFER1:28

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

proof end;

theorem Th29: :: SHEFFER1:29

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

proof end;

definition

let c₁ be non empty ShefferStr ;
let c₂ be Element of c₁;
func c₂ " -> Element of a₁ equals :: SHEFFER1:def 16
a₂ | a₂;
coherence ;

end;

:: deftheorem Def16 defines " SHEFFER1:def 16 :

theorem Th30: :: SHEFFER1:30

for b₁ being non empty satisfying_Sheffer_3 ShefferOrthoLattStr
for b₂, b₃, b₄ being Element of b₁ holds (b₂ | (b₃ | b₄)) " = ((b₃ " ) | b₂) | ((b₄ " ) | b₂) by Def15;

theorem Th31: :: SHEFFER1:31