:: 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 b1 being non empty OrthoLattStr st b1 is de_Morgan & b1 is involutive holds
b1 is DeMorgan
proof end;
cluster non empty involutive DeMorgan -> non empty de_Morgan for OrthoLattStr ;
coherence
for b1 being non empty OrthoLattStr st b1 is DeMorgan & b1 is involutive holds
b1 is de_Morgan
proof end;
end;

registration
cluster non empty trivial -> non empty DeMorgan for OrthoLattStr ;
coherence
for b1 being non empty OrthoLattStr st b1 is trivial holds
b1 is DeMorgan
by STRUCT_0:def 10;
end;

registration
cluster non empty Lattice-like distributive bounded involutive DeMorgan for OrthoLattStr ;
existence
ex b1 being non empty OrthoLattStr st
( b1 is DeMorgan & b1 is involutive & b1 is bounded & b1 is distributive & b1 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 c1 is strict ;
struct NelsonStr -> OrthoLattStr ;
aggr NelsonStr(# carrier, unity, Compl, Nnegation, Iimpl, impl, L_join, L_meet #) -> NelsonStr ;
sel unity c1 -> Element of the carrier of c1;
sel Nnegation c1 -> UnOp of the carrier of c1;
sel Iimpl c1 -> BinOp of the carrier of c1;
sel impl c1 -> BinOp of the carrier of c1;
end;

registration
cluster non empty strict for NelsonStr ;
existence
ex b1 being NelsonStr st
( b1 is strict & not b1 is empty )
proof end;
end;

registration
cluster non empty trivial Lattice-like distributive bounded involutive DeMorgan for NelsonStr ;
existence
ex b1 being non empty NelsonStr st
( b1 is trivial & b1 is DeMorgan & b1 is involutive & b1 is bounded & b1 is distributive & b1 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 b1 being non empty Lattice-like bounded NelsonStr st b1 is satisfying_A2 holds
( b1 is DeMorgan & b1 is involutive & b1 is distributive )
;
cluster non empty Lattice-like distributive bounded involutive DeMorgan -> non empty Lattice-like bounded satisfying_A2 for NelsonStr ;
coherence
for b1 being non empty Lattice-like bounded NelsonStr st b1 is DeMorgan & b1 is involutive & b1 is distributive holds
b1 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 b1 being non empty Lattice-like bounded NelsonStr st
( b1 is satisfying_A1 & b1 is satisfying_A1b & b1 is satisfying_A2 & b1 is satisfying_N3 & b1 is satisfying_N4 & b1 is satisfying_N5 & b1 is satisfying_N6 & b1 is satisfying_N7 & b1 is satisfying_N8 & b1 is satisfying_N9 & b1 is satisfying_N10 & b1 is satisfying_N11 & b1 is satisfying_N12 & b1 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 b1 being Element of L holds
( b1 = a =-> b iff b1 = (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 b1 being Nelson_Algebra holds
( b1 is satisfying_N1* & b1 is satisfying_N2* & b1 is satisfying_N3* & b1 is satisfying_N4* & b1 is satisfying_N5* & b1 is satisfying_N6* & b1 is satisfying_N7* & b1 is satisfying_N8* & b1 is satisfying_N9* & b1 is satisfying_N10* & b1 is satisfying_N11* & b1 is satisfying_N12* & b1 is satisfying_N13* & b1 is satisfying_N14* & b1 is satisfying_N15* & b1 is satisfying_N16* & b1 is satisfying_N17* & b1 is satisfying_N18* & b1 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;