:: Two Axiomatizations of {N}elson Algebras
:: by Adam Grabowski
::
:: Received April 19, 2015
:: Copyright (c) 2015-2021 Association of Mizar Users

definition

let L be non empty OrthoLattStr ;

attr L is DeMorgan means :Def1: :: NELSON_1:def 1
for x, y being Element of L holds (x "/\" y) ` = (x `) "\/" (y `);

end;

:: deftheorem Def1 defines DeMorgan NELSON_1:def 1 :
for L being non empty OrthoLattStr holds
( L is DeMorgan iff for x, y being Element of L holds (x "/\" y) ` = (x `) "\/" (y `) );

registration

cluster non empty de_Morgan involutive -> non empty DeMorgan for OrthoLattStr ;

coherence
for b₁ being non empty OrthoLattStr st b₁ is de_Morgan & b₁ is involutive holds
b₁ is DeMorgan

proof end;

cluster non empty involutive DeMorgan -> non empty de_Morgan for OrthoLattStr ;

coherence
for b₁ being non empty OrthoLattStr st b₁ is DeMorgan & b₁ is involutive holds
b₁ is de_Morgan

proof end;

end;

registration

cluster non empty trivial -> non empty DeMorgan for OrthoLattStr ;

coherence
for b₁ being non empty OrthoLattStr st b₁ is trivial holds
b₁ is DeMorgan by STRUCT_0:def 10;

end;

registration

cluster non empty Lattice-like distributive bounded involutive DeMorgan for OrthoLattStr ;

existence
ex b₁ being non empty OrthoLattStr st
( b₁ is DeMorgan & b₁ is involutive & b₁ is bounded & b₁ is distributive & b₁ is Lattice-like )

proof end;

end;

definition

mode DeMorgan_Algebra is non empty Lattice-like distributive involutive DeMorgan OrthoLattStr ;

end;

definition

mode Quasi-Boolean_Algebra is bounded DeMorgan_Algebra;

end;

theorem Th1: :: NELSON_1:1

for L being Quasi-Boolean_Algebra
for x, y being Element of L holds (x "\/" y) ` = (x `) "/\" (y `)

proof end;

theorem Th2: :: NELSON_1:2

for L being Quasi-Boolean_Algebra holds (Top L) ` = Bottom L

proof end;

theorem :: NELSON_1:3

for L being Quasi-Boolean_Algebra holds (Bottom L) ` = Top L

proof end;

theorem :: NELSON_1:4

for L being Quasi-Boolean_Algebra
for x, y being Element of L holds x "/\" (x "/\" y) = x "/\" y

proof end;

theorem :: NELSON_1:5

for L being Quasi-Boolean_Algebra
for x, y being Element of L holds x "\/" (x "\/" y) = x "\/" y

proof end;

definition

attr c₁ is strict ;
struct NelsonStr -> OrthoLattStr ;
aggr NelsonStr(# carrier, unity, Compl, Nnegation, Iimpl, impl, L_join, L_meet #) -> NelsonStr ;
sel unity c₁ -> Element of the carrier of c₁;
sel Nnegation c₁ -> UnOp of the carrier of c₁;
sel Iimpl c₁ -> BinOp of the carrier of c₁;
sel impl c₁ -> BinOp of the carrier of c₁;

end;

registration

cluster non empty strict for NelsonStr ;

existence
ex b₁ being NelsonStr st
( b₁ is strict & not b₁ is empty )

proof end;

end;

registration

cluster non empty trivial Lattice-like distributive bounded involutive DeMorgan for NelsonStr ;

existence
ex b₁ being non empty NelsonStr st
( b₁ is trivial & b₁ is DeMorgan & b₁ is involutive & b₁ is bounded & b₁ is distributive & b₁ is Lattice-like )

proof end;

end;

definition

let L be non empty NelsonStr ;
let a, b be Element of L;

func a => b -> Element of L equals :: NELSON_1:def 2
the Iimpl of L . (a,b);

coherence
the Iimpl of L . (a,b) is Element of L ;

end;

:: deftheorem defines => NELSON_1:def 2 :
for L being non empty NelsonStr
for a, b being Element of L holds a => b = the Iimpl of L . (a,b);

definition

let L be non empty NelsonStr ;
let a, b be Element of L;

pred a < b means :: NELSON_1:def 3
a => b = Top L;

end;

:: deftheorem defines < NELSON_1:def 3 :
for L being non empty NelsonStr
for a, b being Element of L holds
( a < b iff a => b = Top L );

:: Lattice-like ordering

definition

let L be non empty NelsonStr ;
let a, b be Element of L;

pred a <= b means :: NELSON_1:def 4
a = a "/\" b;

end;

:: deftheorem defines <= NELSON_1:def 4 :
for L being non empty NelsonStr
for a, b being Element of L holds
( a <= b iff a = a "/\" b );

:: Strong negation operator

definition

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

func ! a -> Element of L equals :: NELSON_1:def 5
the Nnegation of L . a;

coherence
the Nnegation of L . a is Element of L ;

end;

:: deftheorem defines ! NELSON_1:def 5 :
for L being non empty NelsonStr
for a being Element of L holds ! a = the Nnegation of L . a;

:: Strong implication

definition

let L be non empty NelsonStr ;
let a, b be Element of L;

func a =-> b -> Element of L equals :: NELSON_1:def 6
the impl of L . (a,b);

coherence
the impl of L . (a,b) is Element of L ;

end;

:: deftheorem defines =-> NELSON_1:def 6 :
for L being non empty NelsonStr
for a, b being Element of L holds a =-> b = the impl of L . (a,b);

::NdR _A1, _A2 : quasi_ordering on A

definition

let L be non empty NelsonStr ;

::NdR _A1, _A2 : quasi_ordering on A

attr L is satisfying_A1 means :Def2: :: NELSON_1:def 7
for a being Element of L holds a < a;

attr L is satisfying_A1b means :Def3: :: NELSON_1:def 8
for a, b, c being Element of L st a < b & b < c holds
a < c;

end;

:: deftheorem Def2 defines satisfying_A1 NELSON_1:def 7 :
for L being non empty NelsonStr holds
( L is satisfying_A1 iff for a being Element of L holds a < a );

:: deftheorem Def3 defines satisfying_A1b NELSON_1:def 8 :
for L being non empty NelsonStr holds
( L is satisfying_A1b iff for a, b, c being Element of L st a < b & b < c holds
a < c );

definition

let L be non empty Lattice-like bounded NelsonStr ;

attr L is satisfying_A2 means :: NELSON_1:def 9
( L is DeMorgan & L is involutive & L is distributive );

end;

:: deftheorem defines satisfying_A2 NELSON_1:def 9 :
for L being non empty Lattice-like bounded NelsonStr holds
( L is satisfying_A2 iff ( L is DeMorgan & L is involutive & L is distributive ) );

registration

cluster non empty Lattice-like bounded satisfying_A2 -> non empty Lattice-like distributive bounded involutive DeMorgan for NelsonStr ;

coherence
for b₁ being non empty Lattice-like bounded NelsonStr st b₁ is satisfying_A2 holds
( b₁ is DeMorgan & b₁ is involutive & b₁ is distributive ) ;

cluster non empty Lattice-like distributive bounded involutive DeMorgan -> non empty Lattice-like bounded satisfying_A2 for NelsonStr ;

coherence
for b₁ being non empty Lattice-like bounded NelsonStr st b₁ is DeMorgan & b₁ is involutive & b₁ is distributive holds
b₁ is satisfying_A2 ;

end;

:: Axioms of N-algebras (according to Rasiowa)
:: These lattices are called Nelson algebras now, but Rasiowa used the name
:: either N-lattices or quasi-pseudo-boolean algebras.

definition

let L be non empty NelsonStr ;

:: Axioms of N-algebras (according to Rasiowa)
:: These lattices are called Nelson algebras now, but Rasiowa used the name
:: either N-lattices or quasi-pseudo-boolean algebras.

attr L is satisfying_N3 means :Def4: :: NELSON_1:def 10
for x, a, b being Element of L holds
( a "/\" x < b iff x < a => b );

attr L is satisfying_N4 means :Def5: :: NELSON_1:def 11
for a, b being Element of L holds a =-> b = (a => b) "/\" ((- b) => (- a));

attr L is satisfying_N5 means :Def6: :: NELSON_1:def 12
for a, b being Element of L holds
( a =-> b = Top L iff a "/\" b = a );

attr L is satisfying_N6 means :Def7: :: NELSON_1:def 13
for a, b, c being Element of L st a < c & b < c holds
a "\/" b < c;

attr L is satisfying_N7 means :Def8: :: NELSON_1:def 14
for a, b, c being Element of L st a < b & a < c holds
a < b "/\" c;

attr L is satisfying_N8 means :Def9: :: NELSON_1:def 15
for a, b being Element of L holds a "/\" (- b) < - (a => b);

attr L is satisfying_N9 means :Def10: :: NELSON_1:def 16
for a, b being Element of L holds - (a => b) < a "/\" (- b);

attr L is satisfying_N10 means :Def11: :: NELSON_1:def 17
for a being Element of L holds a < - (! a);

attr L is satisfying_N11 means :Def12: :: NELSON_1:def 18
for a being Element of L holds - (! a) < a;

attr L is satisfying_N12 means :Def13: :: NELSON_1:def 19
for a, b being Element of L holds a "/\" (- a) < b;

attr L is satisfying_N13 means :Def14: :: NELSON_1:def 20
for a being Element of L holds ! a = a => (- (Top L));

end;

:: deftheorem Def4 defines satisfying_N3 NELSON_1:def 10 :
for L being non empty NelsonStr holds
( L is satisfying_N3 iff for x, a, b being Element of L holds
( a "/\" x < b iff x < a => b ) );

:: deftheorem Def5 defines satisfying_N4 NELSON_1:def 11 :
for L being non empty NelsonStr holds
( L is satisfying_N4 iff for a, b being Element of L holds a =-> b = (a => b) "/\" ((- b) => (- a)) );

:: deftheorem Def6 defines satisfying_N5 NELSON_1:def 12 :
for L being non empty NelsonStr holds
( L is satisfying_N5 iff for a, b being Element of L holds
( a =-> b = Top L iff a "/\" b = a ) );

:: deftheorem Def7 defines satisfying_N6 NELSON_1:def 13 :
for L being non empty NelsonStr holds
( L is satisfying_N6 iff for a, b, c being Element of L st a < c & b < c holds
a "\/" b < c );

:: deftheorem Def8 defines satisfying_N7 NELSON_1:def 14 :
for L being non empty NelsonStr holds
( L is satisfying_N7 iff for a, b, c being Element of L st a < b & a < c holds
a < b "/\" c );

:: deftheorem Def9 defines satisfying_N8 NELSON_1:def 15 :
for L being non empty NelsonStr holds
( L is satisfying_N8 iff for a, b being Element of L holds a "/\" (- b) < - (a => b) );

:: deftheorem Def10 defines satisfying_N9 NELSON_1:def 16 :
for L being non empty NelsonStr holds
( L is satisfying_N9 iff for a, b being Element of L holds - (a => b) < a "/\" (- b) );

:: deftheorem Def11 defines satisfying_N10 NELSON_1:def 17 :
for L being non empty NelsonStr holds
( L is satisfying_N10 iff for a being Element of L holds a < - (! a) );

:: deftheorem Def12 defines satisfying_N11 NELSON_1:def 18 :
for L being non empty NelsonStr holds
( L is satisfying_N11 iff for a being Element of L holds - (! a) < a );

:: deftheorem Def13 defines satisfying_N12 NELSON_1:def 19 :
for L being non empty NelsonStr holds
( L is satisfying_N12 iff for a, b being Element of L holds a "/\" (- a) < b );

:: deftheorem Def14 defines satisfying_N13 NELSON_1:def 20 :
for L being non empty NelsonStr holds
( L is satisfying_N13 iff for a being Element of L holds ! a = a => (- (Top L)) );

registration

cluster non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded V124() V125() V126() satisfying_A1 satisfying_A1b satisfying_A2 satisfying_N3 satisfying_N4 satisfying_N5 satisfying_N6 satisfying_N7 satisfying_N8 satisfying_N9 satisfying_N10 satisfying_N11 satisfying_N12 satisfying_N13 for NelsonStr ;

existence
ex b₁ being non empty Lattice-like bounded NelsonStr st
( b₁ is satisfying_A1 & b₁ is satisfying_A1b & b₁ is satisfying_A2 & b₁ is satisfying_N3 & b₁ is satisfying_N4 & b₁ is satisfying_N5 & b₁ is satisfying_N6 & b₁ is satisfying_N7 & b₁ is satisfying_N8 & b₁ is satisfying_N9 & b₁ is satisfying_N10 & b₁ is satisfying_N11 & b₁ is satisfying_N12 & b₁ is satisfying_N13 )

proof end;

end;

definition

mode Nelson_Algebra is non empty Lattice-like bounded satisfying_A1 satisfying_A1b satisfying_A2 satisfying_N3 satisfying_N4 satisfying_N5 satisfying_N6 satisfying_N7 satisfying_N8 satisfying_N9 satisfying_N10 satisfying_N11 satisfying_N12 satisfying_N13 NelsonStr ;

end;

definition

let L be non empty bounded satisfying_N4 NelsonStr ;
let a, b be Element of L;

redefine func a =-> b equals :: NELSON_1:def 21
(a => b) "/\" ((- b) => (- a));

compatibility
for b₁ being Element of L holds
( b₁ = a =-> b iff b₁ = (a => b) "/\" ((- b) => (- a)) ) by Def5;

end;

:: deftheorem defines =-> NELSON_1:def 21 :
for L being non empty bounded satisfying_N4 NelsonStr
for a, b being Element of L holds a =-> b = (a => b) "/\" ((- b) => (- a));

theorem :: NELSON_1:6

for L being Nelson_Algebra
for a, b being Element of L holds
( a [= b iff a <= b ) by LATTICES:4;

theorem Th3: :: NELSON_1:7

for L being Nelson_Algebra
for a, b being Element of L holds
( ( a <= b & b <= a ) iff a = b )

proof end;

theorem Th4: :: NELSON_1:8

for L being Nelson_Algebra
for a, b being Element of L holds
( a "/\" b = Top L iff ( a = Top L & b = Top L ) )

proof end;

::NdR RasiowaNonClassical: p 69 1.1 (2) <=> (4)

theorem Th5: :: NELSON_1:9

for L being Nelson_Algebra
for a, b being Element of L holds
( a <= b iff ( a < b & - b < - a ) )

proof end;

theorem Th6: :: NELSON_1:10

for L being Nelson_Algebra
for a, b being Element of L holds a "/\" b < a

proof end;

theorem Th7: :: NELSON_1:11

for L being Nelson_Algebra
for a, b being Element of L holds a < a "\/" b

proof end;

::NdR RasiowaNonClassical: p 69 1.1 (2) <=> (3)

theorem :: NELSON_1:12

for L being Nelson_Algebra
for a, b being Element of L holds
( a <= b iff a =-> b = Top L ) by Def6;

::NdR RasiowaNonClassical: p 70 (38)

theorem Th8: :: NELSON_1:13

for L being Nelson_Algebra
for a, b being Element of L holds - (a "/\" b) = (- a) "\/" (- b)

proof end;

theorem :: NELSON_1:14

for L being Nelson_Algebra
for a, b being Element of L holds (a "/\" (- a)) "/\" (b "\/" (- b)) = a "/\" (- a)

proof end;

Lm1: for L being Nelson_Algebra
for a, b, c being Element of L st b < c holds
( a "\/" b < a "\/" c & a "/\" b < a "/\" c )

proof end;

theorem Th9: :: NELSON_1:15

for L being Nelson_Algebra
for a, b, c being Element of L st a <= b & b <= c holds
a <= c

proof end;

theorem Th10: :: NELSON_1:16

for L being Nelson_Algebra
for a, b, c being Element of L st b <= c holds
( a "\/" b <= a "\/" c & a "/\" b <= a "/\" c )

proof end;

theorem Th11: :: NELSON_1:17

for L being Nelson_Algebra
for a, b being Element of L holds (- a) "\/" b <= a => b

proof end;

theorem Th12: :: NELSON_1:18

for L being Nelson_Algebra
for a, b being Element of L holds (a => b) "/\" ((- a) "\/" b) = (- a) "\/" b

proof end;

theorem Th13: :: NELSON_1:19

for L being Nelson_Algebra
for a, b being Element of L holds (- a) "\/" b < a => b

proof end;

theorem Th14: :: NELSON_1:20

for L being Nelson_Algebra
for a, b being Element of L holds a "/\" (a => b) = a "/\" ((- a) "\/" b)

proof end;

Lm2: for L being Nelson_Algebra
for a, b, c, d being Element of L st a < b & c < d holds
( a "\/" c < b "\/" d & a "/\" c < b "/\" d )

proof end;

theorem Th15: :: NELSON_1:21

for L being Nelson_Algebra
for x, y, z being Element of L st - x < - y holds
- (z => x) < - (z => y)

proof end;

theorem Th16: :: NELSON_1:22

for L being Nelson_Algebra
for a, x, y being Element of L st x < y holds
a "/\" (a => x) < y

proof end;

theorem Th16bis: :: NELSON_1:23

for L being Nelson_Algebra
for a, x, y being Element of L st x < y holds
a => x < a => y

proof end;

theorem :: NELSON_1:24

for L being Nelson_Algebra
for a, b, c being Element of L holds a => (b "/\" c) = (a => b) "/\" (a => c)

proof end;

Lm3: for L being Nelson_Algebra
for a, b, c being Element of L holds a => (b => c) = (a "/\" b) => c

proof end;

:: Proven properties from Rasiowa's "Algebraic Models of Logic"
:: Items 2.3, 2.4, p. 92
:: The same set of properties, but with different numbers is also
:: in Rasiowa's "An Algebraic Appproach to Non-Classical Logic"
::NdR RasiowaNonClassical: p 69 1.2 (5)

theorem :: NELSON_1:25

for L being Nelson_Algebra
for a being Element of L holds a =-> a = Top L

proof end;

::NdR RasiowaNonClassical: p 69 1.2 (6)

theorem :: NELSON_1:26

for L being Nelson_Algebra
for a, b, c being Element of L st a =-> b = Top L & b =-> c = Top L holds
a =-> c = Top L

proof end;

::NdR RasiowaNonClassical: p 69 1.2 (7)

theorem :: NELSON_1:27

for L being Nelson_Algebra
for a, b being Element of L st a =-> b = Top L & b =-> a = Top L holds
a = b

proof end;

::NdR RasiowaNonClassical: p 69 1.2 (8)

theorem :: NELSON_1:28

for L being Nelson_Algebra
for a being Element of L holds a =-> (Top L) = Top L

proof end;

::NdR RasiowaNonClassical: p 69 1.3 (9)

theorem Th16ter: :: NELSON_1:29

for L being Nelson_Algebra
for a being Element of L holds a => a = Top L

proof end;

::NdR RasiowaNonClassical: p 69 1.3 (10)

theorem :: NELSON_1:30

for L being Nelson_Algebra
for a, b, c being Element of L st a => b = Top L & b => c = Top L holds
a => c = Top L

proof end;

::NdR RasiowaNonClassical: p 69 1.3 (11)

theorem :: NELSON_1:31

for L being Nelson_Algebra
for a, b, c being Element of L st b < c holds
( a "\/" b < a "\/" c & a "/\" b < a "/\" c ) by Lm1;

::NdR p 69 1.3 (12)

theorem :: NELSON_1:32

for L being Nelson_Algebra
for a, b, c, d being Element of L st a < b & c < d holds
( a "\/" c < b "\/" d & a "/\" c < b "/\" d ) by Lm2;

::NdR RasiowaNonClassical: p 69 1.3 (13)

theorem Th17: :: NELSON_1:33

for L being Nelson_Algebra
for a, b being Element of L holds a "/\" (a => b) < b

proof end;

::NdR RasiowaNonClassical: p 69 1.3 (14)

theorem :: NELSON_1:34

for L being Nelson_Algebra
for a, b, c being Element of L holds a => (b => c) = (a "/\" b) => c by Lm3;

::NdR RasiowaNonClassical: p 69 1.3 (15)

theorem Th18: :: NELSON_1:35

for L being Nelson_Algebra
for a, b, c being Element of L holds a => (b => c) = b => (a => c)

proof end;

::NdR RasiowaNonClassical: p 69 1.3 (16)

theorem Th19: :: NELSON_1:36

for L being Nelson_Algebra
for a, b being Element of L holds a < (a => b) => b

proof end;

::NdR RasiowaNonClassical: p 71 PROOF (50)

theorem Th19bis: :: NELSON_1:37

for L being Nelson_Algebra
for a, b being Element of L holds a < b => (a "/\" b)

proof end;

::NdR RasiowaNonClassical: p 69 (18)

theorem :: NELSON_1:38

for L being Nelson_Algebra
for a, b being Element of L holds a "/\" (- a) <= b "\/" (- b)

proof end;

Lm4: for L being Nelson_Algebra
for a, b being Element of L holds ((- a) "\/" (- b)) "/\" a < - b

proof end;

Lm5: for L being Nelson_Algebra
for a, b being Element of L holds a < (- (a "/\" b)) => (- b)

proof end;

Lm6: for L being Nelson_Algebra
for a, b being Element of L holds - (b =-> (a "/\" b)) < - a

proof end;

theorem :: NELSON_1:39

for L being Nelson_Algebra
for a, b being Element of L holds a <= b =-> (a "/\" b)

proof end;

::NdR RasiowaNonClassical: p 70 1.3 (19)

theorem Th20: :: NELSON_1:40

for L being Nelson_Algebra
for a, b being Element of L holds a => (! b) = b => (! a)

proof end;

::NdR RasiowaNonClassical: p 70 1.3 (20)

theorem Th21: :: NELSON_1:41

for L being Nelson_Algebra
for a being Element of L holds a => (Top L) = Top L

proof end;

::NdR RasiowaNonClassical: p 70 1.3 (21)

theorem Th22: :: NELSON_1:42

for L being Nelson_Algebra
for a being Element of L holds (Bottom L) => a = Top L

proof end;

::NdR RasiowaNonClassical: p 70 1.3 (22)

theorem Th23: :: NELSON_1:43

for L being Nelson_Algebra
for b being Element of L holds (Top L) => b = b

proof end;

::NdR RasiowaNonClassical: p 70 1.3 (23)

theorem :: NELSON_1:44

for L being Nelson_Algebra
for a, b being Element of L st a = Top L & a => b = Top L holds
b = Top L by Th23;

::NdR RasiowaNonClassical: p 70 1.3 (24)

theorem Th24: :: NELSON_1:45

for L being Nelson_Algebra
for a, b being Element of L holds a => (b => a) = Top L

proof end;

::NdR RasiowaNonClassical: p 70 1.3 (25)

theorem Th25: :: NELSON_1:46

for L being Nelson_Algebra
for a, b, c being Element of L holds (a => (b => c)) => ((a => b) => (a => c)) = Top L

proof end;

::NdR RasiowaNonClassical: p 70 1.3 (26)

theorem Th26: :: NELSON_1:47

for L being Nelson_Algebra
for a, b being Element of L holds a => (a "\/" b) = Top L

proof end;

::NdR RasiowaNonClassical: p 70 1.3 (27)

theorem Th27: :: NELSON_1:48

for L being Nelson_Algebra
for a, b being Element of L holds b => (a "\/" b) = Top L

proof end;

::NdR RasiowaNonClassical: p 70 1.3 (28)

theorem Th28: :: NELSON_1:49

for L being Nelson_Algebra
for a, b, c being Element of L holds (a => c) => ((b => c) => ((a "\/" b) => c)) = Top L

proof end;

::NdR RasiowaNonClassical: p 70 1.3 (29)

theorem Th29: :: NELSON_1:50

for L being Nelson_Algebra
for a, b being Element of L holds (a "/\" b) => a = Top L

proof end;

::NdR RasiowaNonClassical: p 70 1.3 (30)

theorem Th30: :: NELSON_1:51

for L being Nelson_Algebra
for a, b being Element of L holds (a "/\" b) => b = Top L

proof end;

::NdR RasiowaNonClassical: p 70 1.3 (31)

theorem Th31: :: NELSON_1:52

for L being Nelson_Algebra
for a, b, c being Element of L holds (a => b) => ((a => c) => (a => (b "/\" c))) = Top L

proof end;

::NdR RasiowaNonClassical: p 70 1.3 (32)

theorem Th32: :: NELSON_1:53

for L being Nelson_Algebra
for a, b being Element of L holds (a => (! b)) => (b => (! a)) = Top L

proof end;

::NdR RasiowaNonClassical: p 70 1.3 (33)

theorem Th33: :: NELSON_1:54

for L being Nelson_Algebra
for a, b being Element of L holds (! (a => a)) => b = Top L

proof end;

::NdR RasiowaNonClassical: p 70 1.3 (34)

theorem Th34: :: NELSON_1:55

for L being Nelson_Algebra
for a, b being Element of L holds (- a) => (a => b) = Top L

proof end;

::NdR RasiowaNonClassical: p 70 1.3 (35)

theorem Th35: :: NELSON_1:56

for L being Nelson_Algebra
for a, b being Element of L holds ((- (a => b)) => (a "/\" (- b))) "/\" ((a "/\" (- b)) => (- (a => b))) = Top L

proof end;

::NdR RasiowaNonClassical: p 70 1.3 (36)

theorem Th36: :: NELSON_1:57

for L being Nelson_Algebra
for a being Element of L holds ((- (! a)) => a) "/\" (a => (- (! a))) = Top L

proof end;

::NdR RasiowaNonClassical: p 70 1.3 (37)

theorem :: NELSON_1:58

for L being Nelson_Algebra
for a being Element of L holds - (- a) = a by ROBBINS3:def 6;

::NdR RasiowaNonClassical: p 70 1.3 (39)

theorem Th37: :: NELSON_1:59

for L being Nelson_Algebra
for a, b being Element of L holds - (a "\/" b) = (- a) "/\" (- b)

proof end;

::NdR RasiowaNonClassical: p 70 1.3 (38)

theorem :: NELSON_1:60

for L being Nelson_Algebra
for a, b being Element of L holds - (a "/\" b) = (- a) "\/" (- b)

proof end;

::NdR RasiowaNonClassical: p 70 1.3 (40)

theorem Th38: :: NELSON_1:61

for L being Nelson_Algebra
for a, b, c being Element of L st a < b holds
( b => c < a => c & c => a < c => b )

proof end;

::NdR RasiowaNonClassical: p 70 1.3 (41)

theorem :: NELSON_1:62

for L being Nelson_Algebra
for a, b, c, d being Element of L holds (a => b) => ((c => d) => ((a "/\" c) => (b "/\" d))) = Top L

proof end;

::NdR RasiowaNonClassical: p 70 1.3 (42)

theorem :: NELSON_1:63

for L being Nelson_Algebra
for a, b, c, d being Element of L holds (a => b) => ((c => d) => ((a "\/" c) => (b "\/" d))) = Top L

proof end;

::NdR RasiowaNonClassical: p 70 1.3 (43)

theorem :: NELSON_1:64

for L being Nelson_Algebra
for a, b, c, d being Element of L holds (b => a) => ((c => d) => ((a => c) => (b => d))) = Top L

proof end;

definition

let L be non empty NelsonStr ;

attr L is satisfying_N0* means :: NELSON_1:def 22
for a, b being Element of L holds
( a <= b iff a =-> b = Top L );

::NdR RasiowaNonClassical: p 75 qpB1*

attr L is satisfying_N1* means :: NELSON_1:def 23
for a, b being Element of L holds a => (b => a) = Top L;

::NdR RasiowaNonClassical: p 75 qpB2*

attr L is satisfying_N2* means :: NELSON_1:def 24
for a, b, c being Element of L holds (a => (b => c)) => ((a => b) => (a => c)) = Top L;

::NdR RasiowaNonClassical: p 76 qpB3*

attr L is satisfying_N3* means :: NELSON_1:def 25
for a being Element of L holds (Top L) => a = a;

::NdR RasiowaNonClassical: p 76 qpB5*

attr L is satisfying_N5* means :: NELSON_1:def 26
for a, b being Element of L holds (a =-> b) => ((b =-> a) => b) = (b =-> a) => ((a =-> b) => a);

::NdR RasiowaNonClassical: p 76 qpB6*

attr L is satisfying_N6* means :: NELSON_1:def 27
for a, b being Element of L holds a => (a "\/" b) = Top L;

::NdR RasiowaNonClassical: p 76 qpB7*

attr L is satisfying_N7* means :: NELSON_1:def 28
for a, b being Element of L holds b => (a "\/" b) = Top L;

::NdR RasiowaNonClassical: p 77 qpB8*

attr L is satisfying_N8* means :: NELSON_1:def 29
for a, b, c being Element of L holds (a => c) => ((b => c) => ((a "\/" b) => c)) = Top L;

::NdR RasiowaNonClassical: p 77 qpB9*

attr L is satisfying_N9* means :: NELSON_1:def 30
for a, b being Element of L holds (a "/\" b) => a = Top L;

::NdR RasiowaNonClassical: p 77 qpB10*

attr L is satisfying_N10* means :: NELSON_1:def 31
for a, b being Element of L holds (a "/\" b) => b = Top L;

::NdR RasiowaNonClassical: p 77 qpB11*

attr L is satisfying_N11* means :: NELSON_1:def 32
for a, b, c being Element of L holds (a => b) => ((a => c) => (a => (b "/\" c))) = Top L;

::NdR RasiowaNonClassical: p 77 qpB12*

attr L is satisfying_N12* means :: NELSON_1:def 33
for a, b being Element of L holds (a => (! b)) => (b => (! a)) = Top L;

::NdR RasiowaNonClassical: p 77 qpB13*

attr L is satisfying_N13* means :: NELSON_1:def 34
for a, b being Element of L holds (! (a => a)) => b = Top L;

::NdR RasiowaNonClassical: p 77 qpB14*

attr L is satisfying_N14* means :: NELSON_1:def 35
for a, b being Element of L holds (- a) => (a => b) = Top L;

::NdR RasiowaNonClassical: p 77 qpB15*

attr L is satisfying_N15* means :: NELSON_1:def 36
for a, b being Element of L holds ((- (a => b)) => (a "/\" (- b))) "/\" ((a "/\" (- b)) => (- (a => b))) = Top L;

::NdR RasiowaNonClassical: p 77 qpB17*

attr L is satisfying_N17* means :: NELSON_1:def 37
for a, b being Element of L holds - (a "\/" b) = (- a) "/\" (- b);

::NdR RasiowaNonClassical: p 77 qpB19*

attr L is satisfying_N19* means :: NELSON_1:def 38
for a being Element of L holds ((- (! a)) => a) "/\" (a => (- (! a))) = Top L;

end;

:: deftheorem defines satisfying_N0* NELSON_1:def 22 :
for L being non empty NelsonStr holds
( L is satisfying_N0* iff for a, b being Element of L holds
( a <= b iff a =-> b = Top L ) );

:: deftheorem defines satisfying_N1* NELSON_1:def 23 :
for L being non empty NelsonStr holds
( L is satisfying_N1* iff for a, b being Element of L holds a => (b => a) = Top L );

:: deftheorem defines satisfying_N2* NELSON_1:def 24 :
for L being non empty NelsonStr holds
( L is satisfying_N2* iff for a, b, c being Element of L holds (a => (b => c)) => ((a => b) => (a => c)) = Top L );

:: deftheorem defines satisfying_N3* NELSON_1:def 25 :
for L being non empty NelsonStr holds
( L is satisfying_N3* iff for a being Element of L holds (Top L) => a = a );

:: deftheorem defines satisfying_N5* NELSON_1:def 26 :
for L being non empty NelsonStr holds
( L is satisfying_N5* iff for a, b being Element of L holds (a =-> b) => ((b =-> a) => b) = (b =-> a) => ((a =-> b) => a) );

:: deftheorem defines satisfying_N6* NELSON_1:def 27 :
for L being non empty NelsonStr holds
( L is satisfying_N6* iff for a, b being Element of L holds a => (a "\/" b) = Top L );

:: deftheorem defines satisfying_N7* NELSON_1:def 28 :
for L being non empty NelsonStr holds
( L is satisfying_N7* iff for a, b being Element of L holds b => (a "\/" b) = Top L );

:: deftheorem defines satisfying_N8* NELSON_1:def 29 :
for L being non empty NelsonStr holds
( L is satisfying_N8* iff for a, b, c being Element of L holds (a => c) => ((b => c) => ((a "\/" b) => c)) = Top L );

:: deftheorem defines satisfying_N9* NELSON_1:def 30 :
for L being non empty NelsonStr holds
( L is satisfying_N9* iff for a, b being Element of L holds (a "/\" b) => a = Top L );

:: deftheorem defines satisfying_N10* NELSON_1:def 31 :
for L being non empty NelsonStr holds
( L is satisfying_N10* iff for a, b being Element of L holds (a "/\" b) => b = Top L );

:: deftheorem defines satisfying_N11* NELSON_1:def 32 :
for L being non empty NelsonStr holds
( L is satisfying_N11* iff for a, b, c being Element of L holds (a => b) => ((a => c) => (a => (b "/\" c))) = Top L );

:: deftheorem defines satisfying_N12* NELSON_1:def 33 :
for L being non empty NelsonStr holds
( L is satisfying_N12* iff for a, b being Element of L holds (a => (! b)) => (b => (! a)) = Top L );

:: deftheorem defines satisfying_N13* NELSON_1:def 34 :
for L being non empty NelsonStr holds
( L is satisfying_N13* iff for a, b being Element of L holds (! (a => a)) => b = Top L );

:: deftheorem defines satisfying_N14* NELSON_1:def 35 :
for L being non empty NelsonStr holds
( L is satisfying_N14* iff for a, b being Element of L holds (- a) => (a => b) = Top L );

:: deftheorem defines satisfying_N15* NELSON_1:def 36 :
for L being non empty NelsonStr holds
( L is satisfying_N15* iff for a, b being Element of L holds ((- (a => b)) => (a "/\" (- b))) "/\" ((a "/\" (- b)) => (- (a => b))) = Top L );

:: deftheorem defines satisfying_N17* NELSON_1:def 37 :
for L being non empty NelsonStr holds
( L is satisfying_N17* iff for a, b being Element of L holds - (a "\/" b) = (- a) "/\" (- b) );

:: deftheorem defines satisfying_N19* NELSON_1:def 38 :
for L being non empty NelsonStr holds
( L is satisfying_N19* iff for a being Element of L holds ((- (! a)) => a) "/\" (a => (- (! a))) = Top L );

notation

let L be non empty NelsonStr ;
synonym satisfying_N4* L for satisfying_N4 ;
synonym satisfying_N16* L for DeMorgan ;
synonym satisfying_N18* L for involutive ;

end;

registration

cluster non empty Lattice-like bounded satisfying_A1 satisfying_A1b satisfying_A2 satisfying_N3 satisfying_N4 satisfying_N5 satisfying_N6 satisfying_N7 satisfying_N8 satisfying_N9 satisfying_N10 satisfying_N11 satisfying_N12 satisfying_N13 -> satisfying_N18* satisfying_N16* satisfying_N1* satisfying_N2* satisfying_N3* satisfying_N5* satisfying_N6* satisfying_N7* satisfying_N8* satisfying_N9* satisfying_N10* satisfying_N11* satisfying_N12* satisfying_N13* satisfying_N14* satisfying_N15* satisfying_N17* satisfying_N19* for NelsonStr ;

coherence
for b₁ being Nelson_Algebra holds
( b₁ is satisfying_N1* & b₁ is satisfying_N2* & b₁ is satisfying_N3* & b₁ is satisfying_N4* & b₁ is satisfying_N5* & b₁ is satisfying_N6* & b₁ is satisfying_N7* & b₁ is satisfying_N8* & b₁ is satisfying_N9* & b₁ is satisfying_N10* & b₁ is satisfying_N11* & b₁ is satisfying_N12* & b₁ is satisfying_N13* & b₁ is satisfying_N14* & b₁ is satisfying_N15* & b₁ is satisfying_N16* & b₁ is satisfying_N17* & b₁ is satisfying_N18* & b₁ is satisfying_N19* )

proof end;

end;

theorem :: NELSON_1:65

for L being non empty NelsonStr st L is satisfying_N0* holds
( L is Nelson_Algebra iff ( L is satisfying_N1* & L is satisfying_N2* & L is satisfying_N3* & L is satisfying_N4* & L is satisfying_N5* & L is satisfying_N6* & L is satisfying_N7* & L is satisfying_N8* & L is satisfying_N9* & L is satisfying_N10* & L is satisfying_N11* & L is satisfying_N12* & L is satisfying_N13* & L is satisfying_N14* & L is satisfying_N15* & L is satisfying_N16* & L is satisfying_N17* & L is satisfying_N18* & L is satisfying_N19* ) )

proof end;