:: by Adam Grabowski

::

:: Received April 19, 2015

:: Copyright (c) 2015-2017 Association of Mizar Users

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

for L being non empty OrthoLattStr holds

( L is DeMorgan iff for x, y being Element of L holds (x "/\" y) ` = (x `) "\/" (y `) );

registration

coherence

for b_{1} being non empty OrthoLattStr st b_{1} is de_Morgan & b_{1} is involutive holds

b_{1} is DeMorgan

for b_{1} being non empty OrthoLattStr st b_{1} is DeMorgan & b_{1} is involutive holds

b_{1} is de_Morgan

end;
for b

b

proof end;

coherence for b

b

proof end;

registration

coherence

for b_{1} being non empty OrthoLattStr st b_{1} is trivial holds

b_{1} is DeMorgan
by STRUCT_0:def 10;

end;
for b

b

registration

existence

ex b_{1} being non empty OrthoLattStr st

( b_{1} is DeMorgan & b_{1} is involutive & b_{1} is bounded & b_{1} is distributive & b_{1} is Lattice-like )

end;
ex b

( b

proof end;

definition
end;

definition

attr c_{1} is strict ;

struct NelsonStr -> OrthoLattStr ;

aggr NelsonStr(# carrier, unity, Compl, Nnegation, Iimpl, impl, L_join, L_meet #) -> NelsonStr ;

sel unity c_{1} -> Element of the carrier of c_{1};

sel Nnegation c_{1} -> UnOp of the carrier of c_{1};

sel Iimpl c_{1} -> BinOp of the carrier of c_{1};

sel impl c_{1} -> BinOp of the carrier of c_{1};

end;
struct NelsonStr -> OrthoLattStr ;

aggr NelsonStr(# carrier, unity, Compl, Nnegation, Iimpl, impl, L_join, L_meet #) -> NelsonStr ;

sel unity c

sel Nnegation c

sel Iimpl c

sel impl c

registration
end;

registration

existence

ex b_{1} being non empty NelsonStr st

( b_{1} is trivial & b_{1} is DeMorgan & b_{1} is involutive & b_{1} is bounded & b_{1} is distributive & b_{1} is Lattice-like )

end;
ex b

( b

proof end;

definition

let L be non empty NelsonStr ;

let a, b be Element of L;

coherence

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

end;
let a, b be Element of L;

coherence

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

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

for L being non empty NelsonStr

for a, b being Element of L holds a => b = the Iimpl of L . (a,b);

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

for L being non empty NelsonStr

for a, b being Element of L holds

( a < b iff a => b = Top L );

:: Lattice-like ordering

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

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;

coherence

the Nnegation of L . a is Element of L ;

end;
let a be Element of L;

coherence

the Nnegation of L . a is Element of L ;

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

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;

coherence

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

end;
let a, b be Element of L;

coherence

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

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

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 ;

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

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

a < c;

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

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

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 ;

end;
attr L is satisfying_A2 means :: NELSON_1:def 9

( L is DeMorgan & L is involutive & L is distributive );

( L is DeMorgan & L is involutive & L is distributive );

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

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

for b_{1} being non empty Lattice-like bounded NelsonStr st b_{1} is satisfying_A2 holds

( b_{1} is DeMorgan & b_{1} is involutive & b_{1} is distributive )
;

for b_{1} being non empty Lattice-like bounded NelsonStr st b_{1} is DeMorgan & b_{1} is involutive & b_{1} is distributive holds

b_{1} is satisfying_A2
;

end;

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

coherence for b

( b

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

coherence for b

b

:: 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.

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

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

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

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

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;

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;

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

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

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

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;

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;

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

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

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

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

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

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

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

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

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

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

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

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

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

for L being non empty NelsonStr holds

( L is satisfying_N13 iff for a being Element of L holds ! a = a => (- (Top L)) );

registration

ex b_{1} being non empty Lattice-like bounded NelsonStr st

( b_{1} is satisfying_A1 & b_{1} is satisfying_A1b & b_{1} is satisfying_A2 & b_{1} is satisfying_N3 & b_{1} is satisfying_N4 & b_{1} is satisfying_N5 & b_{1} is satisfying_N6 & b_{1} is satisfying_N7 & b_{1} is satisfying_N8 & b_{1} is satisfying_N9 & b_{1} is satisfying_N10 & b_{1} is satisfying_N11 & b_{1} is satisfying_N12 & b_{1} is satisfying_N13 )
end;

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

( b

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

compatibility

for b_{1} being Element of L holds

( b_{1} = a =-> b iff b_{1} = (a => b) "/\" ((- b) => (- a)) )
by Def5;

end;
let a, b be Element of L;

compatibility

for b

( b

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

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

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

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)

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

theorem :: NELSON_1:12

::NdR RasiowaNonClassical: p 70 (38)

theorem :: NELSON_1:14

for L being Nelson_Algebra

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

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

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

( a "\/" b <= a "\/" c & a "/\" b <= a "/\" c )

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

for a, b being Element of L holds (a => b) "/\" ((- 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)

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)

for x, y, z being Element of L st - x < - y holds

- (z => x) < - (z => 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)

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)

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

::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

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

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)

::NdR RasiowaNonClassical: p 69 1.3 (9)

::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

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

::NdR p 69 1.3 (12)

theorem :: NELSON_1:32

::NdR RasiowaNonClassical: p 69 1.3 (13)

::NdR RasiowaNonClassical: p 69 1.3 (14)

theorem :: NELSON_1:34

::NdR RasiowaNonClassical: p 69 1.3 (15)

::NdR RasiowaNonClassical: p 69 1.3 (16)

::NdR RasiowaNonClassical: p 71 PROOF (50)

::NdR RasiowaNonClassical: p 69 (18)

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;

::NdR RasiowaNonClassical: p 70 1.3 (19)

::NdR RasiowaNonClassical: p 70 1.3 (20)

::NdR RasiowaNonClassical: p 70 1.3 (21)

::NdR RasiowaNonClassical: p 70 1.3 (22)

::NdR RasiowaNonClassical: p 70 1.3 (23)

theorem :: NELSON_1:44

::NdR RasiowaNonClassical: p 70 1.3 (24)

::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

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)

::NdR RasiowaNonClassical: p 70 1.3 (27)

::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

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)

::NdR RasiowaNonClassical: p 70 1.3 (30)

::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

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)

::NdR RasiowaNonClassical: p 70 1.3 (33)

::NdR RasiowaNonClassical: p 70 1.3 (34)

::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

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

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

::NdR RasiowaNonClassical: p 70 1.3 (39)

::NdR RasiowaNonClassical: p 70 1.3 (38)

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

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

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

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

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 ;

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

for a, b being Element of L holds

( a <= b iff a =-> b = Top L );

attr L is satisfying_N1* means :: NELSON_1:def 23

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

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

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;

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

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

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

attr L is satisfying_N6* means :: NELSON_1:def 27

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

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

attr L is satisfying_N7* means :: NELSON_1:def 28

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

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

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;

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

attr L is satisfying_N9* means :: NELSON_1:def 30

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

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

attr L is satisfying_N10* means :: NELSON_1:def 31

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

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

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;

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

attr L is satisfying_N12* means :: NELSON_1:def 33

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

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

attr L is satisfying_N13* means :: NELSON_1:def 34

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

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

attr L is satisfying_N14* means :: NELSON_1:def 35

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

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

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;

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

attr L is satisfying_N17* means :: NELSON_1:def 37

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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;
synonym satisfying_N4* L for satisfying_N4 ;

synonym satisfying_N16* L for DeMorgan ;

synonym satisfying_N18* L for involutive ;

registration

for b_{1} being Nelson_Algebra holds

( b_{1} is satisfying_N1* & b_{1} is satisfying_N2* & b_{1} is satisfying_N3* & b_{1} is satisfying_N4* & b_{1} is satisfying_N5* & b_{1} is satisfying_N6* & b_{1} is satisfying_N7* & b_{1} is satisfying_N8* & b_{1} is satisfying_N9* & b_{1} is satisfying_N10* & b_{1} is satisfying_N11* & b_{1} is satisfying_N12* & b_{1} is satisfying_N13* & b_{1} is satisfying_N14* & b_{1} is satisfying_N15* & b_{1} is satisfying_N16* & b_{1} is satisfying_N17* & b_{1} is satisfying_N18* & b_{1} is satisfying_N19* )
end;

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

( b

proof 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* ) )

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