:: Two Axiomatizations of {N}elson Algebras
:: by Adam Grabowski
::
:: Received April 19, 2015
:: Copyright (c) 2015-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies LATTICES, BINOP_1, XBOOLE_0, EQREL_1, XBOOLEAN, XXREAL_0,
REALSET1, SUBSET_1, STRUCT_0, XXREAL_2, FUNCT_1, ARYTM_3, ARYTM_1,
ROBBINS1, NELSON_1, PBOOLE, ZFMISC_1, OPOSET_1;
notations TARSKI, XBOOLE_0, LATTICES, SUBSET_1, BINOP_1, FUNCT_2, STRUCT_0,
ROBBINS1, ROBBINS3;
constructors BINOP_1, ROBBINS3;
registrations STRUCT_0, LATTICES, LATTICE2, ROBBINS1, ROBBINS3, XBOOLE_0,
ZFMISC_1, LATTAD_1;
requirements SUBSET, BOOLE;
definitions LATTICES;
expansions ROBBINS1, ROBBINS3, LATTICES;
theorems STRUCT_0, LATTICES, ROBBINS3, TARSKI;
begin :: De Morgan Algebras
definition let L be non empty OrthoLattStr;
attr L is DeMorgan means :Def1:
for x, y being Element of L holds
(x "/\" y)` = x` "\/" y`;
end;
registration
cluster de_Morgan involutive -> DeMorgan for non empty OrthoLattStr;
coherence
proof
let L be non empty OrthoLattStr;
assume
A1: L is de_Morgan involutive;
let x,y be Element of L;
x "/\" y = (x` "\/" y`)` by A1;
hence thesis by A1;
end;
cluster DeMorgan involutive -> de_Morgan for non empty OrthoLattStr;
coherence
proof
let L be non empty OrthoLattStr;
assume
A1: L is DeMorgan involutive;
now let x,y be Element of L;
x` "\/" y` = (x "/\" y)` by A1;
hence (x` "\/" y`)` = x "/\" y by A1;
end;
hence thesis;
end;
end;
registration
cluster trivial -> DeMorgan for non empty OrthoLattStr;
coherence by STRUCT_0:def 10;
end;
registration
cluster DeMorgan involutive bounded distributive Lattice-like for
non empty OrthoLattStr;
existence
proof
take TrivOrtLat;
thus thesis;
end;
end;
definition
mode DeMorgan_Algebra is DeMorgan involutive
distributive Lattice-like non empty OrthoLattStr;
end;
definition
mode Quasi-Boolean_Algebra is bounded DeMorgan_Algebra;
end;
reserve L for Quasi-Boolean_Algebra,
x, y, z for Element of L;
theorem Th1:
(x "\/" y)` = x` "/\" y`
proof
(x` "/\" y`)` = x`` "\/" y`` by Def1;
hence x` "/\" y` = (x`` "\/" y``)` by ROBBINS3:def 6
.= (x "\/" y``)` by ROBBINS3:def 6
.= (x "\/" y)` by ROBBINS3:def 6;
end;
theorem Th2:
(Top L)` = Bottom L
proof
thus (Top L)` = (Top L)` "\/" Bottom L
.= (Top L)` "\/" (Bottom L)`` by ROBBINS3:def 6
.= ((Top L) "/\" (Bottom L)`)` by Def1
.= Bottom L by ROBBINS3:def 6;
end;
theorem
(Bottom L)` = Top L
proof
thus (Bottom L)` = ((Bottom L)` "/\" (Top L))`` by ROBBINS3:def 6
.= ((Bottom L)`` "\/" (Top L)`)` by Def1
.= ((Bottom L) "\/" (Top L)`)` by ROBBINS3:def 6
.= Top L by ROBBINS3:def 6;
end;
theorem
x "/\" (x "/\" y) = x "/\" y
proof
thus x "/\" (x "/\" y) = (x "/\" x) "/\" y by LATTICES:def 7
.= x "/\" y;
end;
theorem
x "\/" (x "\/" y) = x "\/" y
proof
thus x "\/" (x "\/" y) = (x "\/" x) "\/" y by LATTICES:def 5
.= x "\/" y;
end;
begin :: The Structure and Operators in Nelson Algebras
definition
struct (OrthoLattStr) NelsonStr
(# carrier -> set,
unity -> Element of the carrier,
Compl, Nnegation -> UnOp of the carrier,
Iimpl, impl, L_join, L_meet -> BinOp of the carrier #);
end;
registration
cluster strict non empty for NelsonStr;
existence
proof
set A = {{}};
set B = the Element of A;
set C = the UnOp of A;
set D = the BinOp of A;
take NelsonStr (#A,B,C,C,D,D,D,D#);
thus thesis;
end;
end;
registration
cluster trivial DeMorgan involutive bounded distributive Lattice-like for
non empty NelsonStr;
existence
proof
set A = {{}};
set B = the Element of A;
set C = the UnOp of A;
set D = the BinOp of A;
reconsider N=NelsonStr(#A,B,C,C,D,D,D,D#) as non empty NelsonStr;
take N;
A1: now let x,y be Element of N;
x = {} & y = {} by TARSKI:def 1;
hence x = y & x = {};
end;
thus N is trivial;
thus N is DeMorgan by A1;
thus N is involutive by A1;
thus N is bounded distributive
proof
reconsider E = {} as Element of N by TARSKI:def 1;
for x be Element of N holds
E "\/" x = E & x "\/" E = E &
x "/\" E = E & E "/\" x = E by TARSKI:def 1;
then N is lower-bounded upper-bounded;
hence N is bounded;
let x,y,z being Element of N;
thus x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z) by A1;
end;
N is join-commutative join-associative meet-absorbing
meet-commutative meet-associative join-absorbing by A1;
hence thesis;
end;
end;
definition let L be non empty NelsonStr,
a, b be Element of L;
func a => b -> Element of L equals
(the Iimpl of L).(a,b);
coherence;
end;
definition let L be non empty NelsonStr,
a, b be Element of L;
pred a < b means
a => b = Top L;
end;
:: Lattice-like ordering
definition let L be non empty NelsonStr,
a, b be Element of L;
pred a <= b means
a = a "/\" b;
end;
:: Strong negation operator
definition let L be non empty NelsonStr,
a be Element of L;
func ! a -> Element of L equals
(the Nnegation of L).a;
coherence;
end;
:: Strong implication
definition let L be non empty NelsonStr,
a, b be Element of L;
func a =-> b -> Element of L equals
(the impl of L).(a,b);
coherence;
end;
begin :: The Non-Equational Axiomatization of Nelson Algebras
::NdR _A1, _A2 : quasi_ordering on A
definition let L be non empty NelsonStr;
attr L is satisfying_A1 means :Def2:
for a being Element of L holds
a < a;
attr L is satisfying_A1b means :Def3:
for a, b, c being Element of L holds
a < b & b < c implies a < c;
end;
definition let L be bounded Lattice-like non empty NelsonStr;
attr L is satisfying_A2 means
L is DeMorgan involutive distributive;
end;
registration
cluster satisfying_A2 -> DeMorgan involutive distributive
for bounded Lattice-like non empty NelsonStr;
coherence;
cluster DeMorgan involutive distributive -> satisfying_A2
for bounded Lattice-like non empty NelsonStr;
coherence;
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;
attr L is satisfying_N3 means :Def4:
for x, a, b being Element of L holds
a "/\" x < b iff x < (a => b);
attr L is satisfying_N4 means :Def5:
for a, b being Element of L holds
a =-> b = (a => b) "/\" ((-b) => -a);
attr L is satisfying_N5 means :Def6:
for a, b being Element of L holds
a =-> b = Top L iff a "/\" b = a;
attr L is satisfying_N6 means :Def7:
for a, b, c being Element of L holds
a < c & b < c implies a "\/" b < c;
attr L is satisfying_N7 means :Def8:
for a, b, c being Element of L holds
a < b & a < c implies a < b "/\" c;
attr L is satisfying_N8 means :Def9:
for a, b being Element of L holds
(a "/\" -b) < -(a => b);
attr L is satisfying_N9 means :Def10:
for a, b being Element of L holds
-(a => b) < (a "/\" -b);
attr L is satisfying_N10 means :Def11:
for a being Element of L holds
a < -!a;
attr L is satisfying_N11 means :Def12:
for a being Element of L holds
-!a < a;
attr L is satisfying_N12 means :Def13:
for a, b being Element of L holds
a "/\" -a < b;
attr L is satisfying_N13 means :Def14:
for a being Element of L holds
! a = a => - Top L;
end;
registration
cluster 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 bounded Lattice-like non empty NelsonStr;
existence
proof
set L = the trivial non empty NelsonStr;
reconsider LL = L as bounded Lattice-like non empty NelsonStr;
A1: LL is satisfying_A1
proof
let a be Element of LL;
thus thesis by STRUCT_0:def 10;
end;
A2: LL is satisfying_A1b by STRUCT_0:def 10;
A3: LL is satisfying_N8
proof
let a, b be Element of LL;
thus thesis by STRUCT_0:def 10;
end;
A4: LL is satisfying_N9
proof
let a, b be Element of LL;
thus thesis by STRUCT_0:def 10;
end;
A5: LL is satisfying_A2 satisfying_N4 satisfying_N6 satisfying_N7
satisfying_N5 by STRUCT_0:def 10;
A6: LL is satisfying_N10
proof
let a be Element of LL;
thus thesis by STRUCT_0:def 10;
end;
A7: LL is satisfying_N11
proof
let a be Element of LL;
thus thesis by STRUCT_0:def 10;
end;
A8: LL is satisfying_N12
proof
let a be Element of LL;
thus thesis by STRUCT_0:def 10;
end;
A9: LL is satisfying_N3
proof
let x, a, b be Element of LL;
thus thesis by STRUCT_0:def 10;
end;
LL is satisfying_N13 by STRUCT_0:def 10;
hence thesis by A1,A2,A3,A4,A5,A6,A7,A8,A9;
end;
end;
definition
mode Nelson_Algebra is 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 bounded Lattice-like non empty NelsonStr;
end;
definition let L be satisfying_N4 bounded non empty NelsonStr,
a, b be Element of L;
redefine func a =-> b equals :: redefines =-> (NELSON_1, definition)
(a => b) "/\" ((-b) => -a);
compatibility by Def5;
end;
reserve L for Nelson_Algebra,
a, b, c, d, x, y, z for Element of L;
theorem
a [= b iff a <= b by LATTICES:4;
theorem Th3:
a <= b & b <= a iff a = b
proof
thus a <= b & b <= a implies a = b
proof
assume a <= b & b <= a; then
a [= b & b [= a by LATTICES:4;
hence thesis by LATTICES:8;
end;
thus thesis;
end;
theorem Th4:
a "/\" b = Top L iff a = Top L & b = Top L
proof
hereby assume
A1: a "/\" b = Top L; then
Top L [= a by LATTICES:6;
hence a = Top L;
Top L [= b by A1,LATTICES:6;
hence b = Top L;
end;
thus thesis;
end;
::NdR RasiowaNonClassical: p 69 1.1 (2) <=> (4)
theorem Th5: :: (2.1) (2.3 <=> 2.5)
a <= b iff a < b & -b < -a
proof
thus a <= b implies a < b & -b < -a
proof
assume a <= b; then
a =-> b = Top L by Def6;
hence a < b & -b < -a by Th4;
end;
assume a < b & -b < -a; then
a =-> b = Top L;
hence thesis by Def6;
end;
theorem Th6:
a "/\" b < a
proof
a "/\" b <= a by LATTICES:4,6;
hence thesis by Th5;
end;
theorem Th7:
a < a "\/" b
proof
a <= a "\/" b by LATTICES:4,5;
hence thesis by Th5;
end;
::NdR RasiowaNonClassical: p 69 1.1 (2) <=> (3)
theorem :: (2.1) (2.3 <=> 2.4)
a <= b iff a =-> b = Top L by Def6;
::NdR RasiowaNonClassical: p 70 (38)
theorem Th8:
-(a "/\" b) = (-a) "\/" (-b)
proof
thus -(a "/\" b) = -((-(-a)) "/\" b) by ROBBINS3:def 6
.= -((-(-a)) "/\" (-(-b))) by ROBBINS3:def 6
.= -(-((-a) "\/"(- b))) by Th1
.= ((-a) "\/" (-b)) by ROBBINS3:def 6;
end;
theorem
(a "/\" -a) "/\" (b "\/" -b) = a "/\" -a
proof
((-b) "/\" (--b)) < ((-a) "\/" a) by Def13; then
-(b "\/" (-b)) < ((-a) "\/" a) by Th1; then
-(b "\/" (-b)) < ((-a) "\/"(--a)) by ROBBINS3:def 6; then
-(b "\/" (-b)) < -(a "/\"(-a)) by Th8; then
(a "/\" -a) <= (b "\/" -b) by Th5,Def13;
hence thesis;
end;
Lm1:
b < c implies a "\/" b < a "\/" c & a "/\" b < a "/\" c
proof
assume
A1: b < c;
A2: a < a "\/" c by Th7;
c < a "\/" c by Th7; then
A3: b < a "\/" c by A1,Def3;
A4: a "/\" b < a by Th6;
a "/\" b < b by Th6; then
a "/\" b < c by A1,Def3;
hence thesis by A3,A4,Def8,A2,Def7;
end;
theorem Th9:
a <= b & b <= c implies a <= c
proof
assume a <= b & b <= c; then
a [= b & b [= c by LATTICES:4;
hence thesis by LATTICES:4,7;
end;
theorem Th10:
b <= c implies a "\/" b <= a "\/" c & a "/\" b <= a "/\" c
proof
assume
A1: b <= c;
A2: a "\/" b < a "\/" c
proof
b < c by A1,Th5;
hence thesis by Lm1;
end;
A3: -(a "\/" c) < -(a "\/" b)
proof
-c < - b by A1,Th5; then
(-a) "/\" (-c) < (-a) "/\" (-b) by Lm1; then
-(a "\/" c) < (-a) "/\" (-b) by Th1;
hence thesis by Th1;
end;
A4: a "/\" b < a "/\" c
proof
b < c by A1,Th5;
hence thesis by Lm1;
end;
-(a "/\" c) < -(a "/\" b)
proof
-c < -b by A1,Th5; then
(-a) "\/" (-c) < (-a) "\/" (-b) by Lm1; then
-(a "/\" c) < (-a) "\/" (-b) by Th8;
hence thesis by Th8;
end;
hence thesis by A4,Th5,A2,A3;
end;
theorem Th11:
(-a) "\/" b <= a => b
proof
a < -!a by Def11; then
(a "/\" (-b)) < ((-!a) "/\" (-b)) by Lm1; then
A1: (a "/\" -b) < -((!a) "\/" b) by Th1;
-(a => b) < (a "/\" -b) by Def10; then
A2: -(a => b) < -((!a) "\/" b) by A1,Def3;
(a => (Bottom L)) < a => Bottom L by Def2; then
((a => (Bottom L)) "/\" a) < Bottom L by Def4; then
(a "/\" (a => (Top L)`)) < Bottom L by Th2; then
A3: a "/\" (!a) < (Bottom L) by Def14;
Bottom L <= b; then
Bottom L < b by Th5; then
a "/\" (!a) < b by A3,Def3; then
A4: (!a) < (a => b) by Def4;
b "/\" a < b by Th6; then
b < (a => b) by Def4; then
A5: (!a) "\/" b <= (a => b) by A2,Th5,A4,Def7;
(a "/\" (-a)) < Bottom L by Def13; then
A6: (-a) < (a => (Bottom L)) by Def4;
(a => (Top L)`) = (!a) by Def14; then
A7: (-a) < (!a) by A6,Th2;
A8: (-!a) < a by Def12;
a = (--a) by ROBBINS3:def 6; then
-a <= (!a) by A8,A7,Th5; then
b "\/" (-a) <= b "\/" (!a) by Th10;
hence thesis by A5,Th9;
end;
theorem Th12:
(a => b) "/\" ((-a) "\/" b) = (-a) "\/" b
proof
A1: -((-a) "\/" b) < -((a => b) "/\" ((-a) "\/" b))
proof
A2: -((-a) "\/" b) = (--a) "/\" (-b) by Th1;
A3: (--a) "/\" (-b) = a "/\" (-b) by ROBBINS3:def 6;
a "/\" (-b) < -(a => b) by Def9; then
(-((-a) "\/" b)) "\/" (-((-a) "\/" b)) <
(-(a => b)) "\/" (-((-a) "\/" b)) by A2,A3,Lm1;
hence thesis by Th8;
end;
A4: ((-a) "\/" b) <= ((a => b) "/\" ((-a) "\/" b))
proof
((-a) "\/" b) <= (a => b) by Th11;
hence thesis;
end;
(a => b) "/\" ((-a) "\/" b) <= (-a) "\/" b by Th6,A1,Th5;
hence thesis by A4,Th3;
end;
theorem Th13:
(-a) "\/" b < a => b
proof
(a => b) "/\" ((-a) "\/" b) = (-a) "\/" b by Th12; then
(-a) "\/" b <= a => b;
hence thesis by Th5;
end;
theorem Th14:
a "/\" (a => b) = a "/\" ((-a) "\/" b)
proof
A1: a "/\" (a => b) < a "/\" ((-a) "\/" b)
proof
a => b < a => b by Def2; then
A2: a "/\" (a => b) < b by Def4;
b < b "\/" (-a) by Th7; then
A3: a "/\" (a => b) < (-a) "\/" b by A2,Def3;
a "/\" (a => b) < a by Th6;
hence thesis by A3,Def8;
end;
A4: -(a "/\" ((-a)"\/"b)) < -(a "/\" (a => b))
proof
A5: -(a "/\" ((-a) "\/" b)) = (-a) "\/" -((-a) "\/" b) by Th8;
A6: (-a) "\/" -((-a) "\/" b) = (-a) "\/" ((--a) "/\" (-b)) by Th1;
A7: (-a) "\/" ((--a) "/\" (-b)) = (-a) "\/" (a "/\" (-b))
by ROBBINS3:def 6;
A8: (a "/\" (-b)) < -(a => b) by Def9;
-(a => b) < (-a) "\/" -(a => b) by Th7; then
A9: -(a => b) < -(a "/\" (a => b)) by Th8;
A10: (-a) < (-a) "\/" -(a => b) by Th7;
A11: (a "/\" (-b)) < -(a "/\" (a => b)) by A8,A9,Def3;
(-a) < -(a "/\" (a => b)) by A10,Th8;
hence thesis by A5,A6,A7,A11,Def7;
end;
A12: a "/\" ((-a) "\/" b) < a "/\" (a => b)
proof
((-a) "\/" b) < (a => b) by Th13;
hence thesis by Lm1;
end;
A13: -(a "/\" (a => b)) < -(a "/\" ((-a)"\/"b))
proof
-(a => b) < a "/\" (-b) by Def10; then
(-a) "\/" -(a => b) < (-a) "\/" (a "/\" (-b)) by Lm1; then
-(a "/\" (a => b)) < (-a) "\/" (a "/\" (-b)) by Th8; then
-(a "/\" (a => b)) < (-a) "\/" ((--a) "/\" (-b))
by ROBBINS3:def 6; then
-(a "/\" (a => b)) < (-a) "\/" -((-a) "\/" b) by Th1;
hence thesis by Th8;
end;
A14: a "/\" ((-a)"\/"b) <= a "/\" (a => b) by A12,A13,Th5;
a "/\" (a => b) <= a "/\" ((-a) "\/" b) by A1,A4,Th5;
hence thesis by A14,Th3;
end;
Lm2:
a < b & c < d implies a "\/" c < b "\/" d & a "/\" c < b "/\" d
proof
assume a < b & c < d; then
a "\/" c < a "\/" d & a "/\" c < a "/\" d &
a "\/" d < b "\/" d & a "/\" d < b "/\" d by Lm1;
hence thesis by Def3;
end;
theorem Th15:
-x < -y implies -(z => x) < -(z => y)
proof
assume
A1: -x < -y;
A2: -(z => x) < z "/\" (-x) by Def10;
z "/\" (-x) < z "/\" (-y) by A1,Lm1; then
A3: -(z => x) < z "/\" (-y) by A2,Def3;
z "/\" (-y) < -(z => y) by Def9;
hence thesis by A3,Def3;
end;
theorem Th16:
x < y implies a "/\" (a => x) < y
proof
assume
A1: x < y;
A2: a "/\" (a => x) = a "/\" ((-a) "\/" x) by Th14;
A3: a "/\" ((-a) "\/" x) = (a "/\" (-a)) "\/" (a "/\" x)
by LATTICES:def 11;
A4: (a "/\" x) < x by Th6;
(a "/\" (-a)) < x by Def13; then
a "/\" (a => x) < x by A3,A2,A4,Def7;
hence thesis by A1,Def3;
end;
theorem Th16bis:
x < y implies a => x < a => y
proof
assume x < y; then
a "/\" (a => x) < y by Th16;
hence thesis by Def4;
end;
theorem
a => (b "/\" c) = (a => b) "/\" (a => c)
proof
A1: -((a => b) "/\" (a => c)) < -(a => (b "/\" c))
proof
A2: -(a => b) < (a "/\" (-b)) by Def10;
(-b) < (-b) "\/" (-c) by Th7; then
(-b) < -(b "/\" c) by Th8; then
A3: a "/\" (-b) < a "/\" -(b "/\" c) by Lm1;
A4: -(a => b) < a "/\" -(b "/\" c) by A2,A3,Def3;
a "/\" -(b "/\" c) < -(a => (b "/\" c)) by Def9; then
A5: -(a => b) < -(a => (b "/\" c)) by A4,Def3;
A6: -(a => c) < (a "/\" (-c)) by Def10;
(-c) < (-b) "\/" (-c) by Th7; then
(-c) < -(b "/\" c) by Th8; then
a "/\" (-c) < a "/\" -(b "/\" c) by Lm1; then
A7: -(a => c) < a "/\" -(b "/\" c) by A6,Def3;
a "/\" -(b "/\" c) < -(a => (b "/\" c)) by Def9; then
-(a => c) < -(a => (b "/\" c)) by A7,Def3; then
(-(a => b)) "\/" (-(a => c)) < -(a => (b "/\" c)) by A5,Def7;
hence thesis by Th8;
end;
A8: -(a => (b "/\" c)) < -((a => b) "/\" (a => c))
proof
A9: -(a => (b "/\" c)) < a "/\" -(b "/\" c) by Def10;
A10: a "/\" (-b) < -(a => b) by Def9;
a "/\" (-c) < -(a => c) by Def9; then
(a "/\" (-b)) "\/" (a "/\" (-c)) < (-(a => b)) "\/" (-(a => c))
by A10,Lm2; then
a "/\" ((-b) "\/" (-c)) < (-(a => b)) "\/" (-(a => c))
by LATTICES:def 11; then
a "/\" -(b "/\" c) < (-(a => b)) "\/" (-(a => c)) by Th8; then
a "/\" -(b "/\" c) < -((a => b) "/\" (a => c)) by Th8;
hence thesis by A9,Def3;
end;
A11: a => (b "/\" c) < (a => b) "/\" (a => c)
proof
A12: a => (b "/\" c) < a => b by Th6,Th16bis;
a => (b "/\" c) < a => c by Th6,Th16bis;
hence thesis by A12,Def8;
end;
A13: (a => b) "/\" (a => c) < a => (b "/\" c)
proof
a => b < a => b by Def2; then
A14: a "/\" (a => b) < b by Def4;
a => c < a => c by Def2; then
a "/\" (a => c) < c by Def4; then
(a "/\" (a => b)) "/\" (a "/\" (a => c)) < b "/\" c by A14,Lm2; then
(a "/\" (a => b)) "/\" a "/\" (a => c) < b "/\" c
by LATTICES:def 7; then
(a "/\" a) "/\" (a => b) "/\" (a => c) < b "/\" c
by LATTICES:def 7; then
a "/\" ((a => b) "/\" (a => c)) < b "/\" c by LATTICES:def 7;
hence thesis by Def4;
end;
A15: a => (b "/\" c) <= (a => b) "/\" (a => c) by A1,A11,Th5;
(a => b) "/\" (a => c) <= a => (b "/\" c) by A8,A13,Th5;
hence thesis by A15,Th3;
end;
Lm3:
a => (b => c) = (a "/\" b) => c
proof
A1: a => (b => c) < (a "/\" b) => c
proof
A2: a "/\" ((-b) "\/" c) < ((-b) "\/" c) by Th6;
((-b) "\/" c) < b => c by Th13; then
A3: a "/\" ((-b)"\/" c) < b => c by A2,Def3;
a "/\" (-a) < b => c by Def13; then
(a "/\" ((-b) "\/" c)) "\/" (a "/\" (-a)) < b => c by A3,Def7; then
a "/\" (((-b) "\/" c) "\/" (-a)) < b => c by LATTICES:def 11; then
b "/\" (a "/\" ((-b) "\/" c "\/" (-a))) < c by Def4; then
b "/\" (a "/\" (((-b) "\/" (-a)) "\/" c)) < c by LATTICES:def 5; then
A4: (b "/\" a) "/\" (((-a) "\/" (-b)) "\/" c) < c by LATTICES:def 7;
A5: b "/\" a "/\" ((-a) "\/" ((-b) "\/" c)) =
(b "/\" a "/\" (-a)) "\/"
(b "/\" a "/\" ((-b) "\/" c)) by LATTICES:def 11;
b "/\" ((-b) "\/" c) = b "/\" (b => c) by Th14; then
A6: (b "/\" a "/\" (-a)) "\/" (a "/\" (b "/\" ((-b) "\/" c))) =
((b "/\" a) "/\" (-a)) "\/" ((a "/\" b) "/\" (b => c))
by LATTICES:def 7
.= (b "/\" a) "/\" ((-a) "\/" (b => c)) by LATTICES:def 11;
a "/\" ((-a) "\/" (b => c)) = a "/\" (a => (b => c)) by Th14; then
A7: (b "/\" a) "/\"((-a) "\/" (b => c)) = b "/\" (a "/\" (a => (b => c)))
by LATTICES:def 7;
A8: (b "/\" a) "/\" ((-a) "\/" ((-b) "\/" c)) < c by A4,LATTICES:def 5;
(b "/\" a) "/\" ((-a) "\/" ((-b) "\/" c)) =
(b "/\" a "/\" (-a)) "\/" (a "/\" (b "/\" ((-b) "\/" c)))
by A5,LATTICES:def 7; then
(b "/\" a) "/\" (a => (b => c)) < c by LATTICES:def 7,A7,A6,A8;
hence thesis by Def4;
end;
A9: -(a => (b => c)) < -((a "/\" b) => c)
proof
A10: -(a => (b => c)) < a "/\" -(b => c) by Def10;
-(b => c) < b "/\" (-c) by Def10; then
a "/\" -(b => c) < a "/\" (b "/\" (-c)) by Lm1; then
A11: -(a => (b => c)) < a "/\" (b "/\" (-c)) by A10,Def3;
A12: a "/\" (b "/\" (-c)) = (a "/\" b) "/\" (-c) by LATTICES:def 7;
(a "/\" b) "/\" (-c) < -((a "/\" b) => c) by Def9;
hence thesis by A11,A12,Def3;
end;
A13: (a "/\" b) => c < a => (b => c)
proof
((a "/\" b) => c) < ((a "/\" b) => c) by Def2; then
a "/\" b "/\" ((a "/\" b) => c) < c by Def4; then
b "/\" (a "/\" (a "/\" b) => c) < c by LATTICES:def 7; then
a "/\" ((a "/\" b) => c) < b => c by Def4;
hence thesis by Def4;
end;
A14: -((a "/\" b) => c) < -(a => (b => c))
proof
A15: -((a "/\" b) => c) < (a "/\" b) "/\" (-c) by Def10;
A16: (a "/\" b) "/\" (-c) = a "/\" (b "/\" (-c)) by LATTICES:def 7
.= a "/\" ((--b) "/\" (-c)) by ROBBINS3:def 6
.= a "/\" -((-b) "\/" c) by Th1;
a "/\" -((-b) "\/" c) < -(a => ((-b) "\/" c)) by Def9; then
A17: -((a "/\" b) => c) < -(a => ((-b) "\/" c)) by A15,A16,Def3;
A18: b "/\" (-c) < -(b => c) by Def9;
b "/\" (-c) = (--b) "/\" (-c) by ROBBINS3:def 6
.= -((-b) "\/" c) by Th1; then
-(a => ((-b) "\/" c)) < -(a => (b => c)) by Th15,A18;
hence thesis by A17,Def3;
end;
A19: a => (b => c) <= (a "/\" b) => c by Th5,A1,A14;
(a "/\" b) => c <= a => (b => c) by Th5,A13,A9;
hence thesis by A19,Th3;
end;
begin :: Properties of Nelson Algebras
:: 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 :: (2.7)
a =-> a = Top L
proof
a "/\" a = a;
hence thesis by Def6;
end;
::NdR RasiowaNonClassical: p 69 1.2 (6)
theorem :: (2.8)
a =-> b = Top L & b =-> c = Top L implies a =-> c = Top L
proof
assume a =-> b = Top L & b =-> c = Top L; then
a "/\" b = a & b "/\" c = b by Def6; then
a "/\" c = a by LATTICES:def 7;
hence thesis by Def6;
end;
::NdR RasiowaNonClassical: p 69 1.2 (7)
theorem :: (2.9)
a =-> b = Top L & b =-> a = Top L implies a = b
proof
assume a =-> b = Top L & b =-> a = Top L; then
a "/\" b = a & b "/\" a = b by Def6;
hence thesis;
end;
::NdR RasiowaNonClassical: p 69 1.2 (8)
theorem :: (2.10)
a =-> Top L = Top L
proof
a "/\" Top L = a;
hence thesis by Def6;
end;
::NdR RasiowaNonClassical: p 69 1.3 (9)
theorem Th16ter: :: (2.11)
a => a = Top L
proof
a < a by Def2;
hence thesis;
end;
::NdR RasiowaNonClassical: p 69 1.3 (10)
theorem :: (2.12)
(a => b) = (Top L) & (b => c) = (Top L) implies (a => c) = (Top L)
proof
assume
A1: (a => b) = (Top L) & (b => c) = (Top L);
A2: a < b by A1;
A3: b < c by A1;
a < c by Def3,A2,A3;
hence thesis;
end;
::NdR RasiowaNonClassical: p 69 1.3 (11)
theorem :: (2.13)
b < c implies a "\/" b < a "\/" c & a "/\" b < a "/\" c by Lm1;
::NdR p 69 1.3 (12)
theorem :: (2.14)
a < b & c < d implies a "\/" c < b "\/" d & a "/\" c < b "/\" d
by Lm2;
::NdR RasiowaNonClassical: p 69 1.3 (13)
theorem Th17: :: (2.15)
a "/\" (a => b) < b
proof
(a => b) < (a => b) by Def2;
hence thesis by Def4;
end;
::NdR RasiowaNonClassical: p 69 1.3 (14)
theorem :: (2.16)
a => (b => c) = (a "/\" b) => c by Lm3;
::NdR RasiowaNonClassical: p 69 1.3 (15)
theorem Th18: :: (2.17)
a => (b => c) = b => (a => c)
proof
a => (b => c) = (a "/\" b) => c by Lm3
.= b => (a => c) by Lm3;
hence thesis;
end;
::NdR RasiowaNonClassical: p 69 1.3 (16)
theorem Th19: :: (2.18)
a < ((a => b) => b)
proof
a "/\" (a => b) < b by Th17;
hence thesis by Def4;
end;
::NdR RasiowaNonClassical: p 71 PROOF (50)
theorem Th19bis: :: (2.19)
a < b => (a "/\" b)
proof
b "/\" a <= a "/\" b; then
b "/\" a < a "/\" b by Th5;
hence thesis by Def4;
end;
::NdR RasiowaNonClassical: p 69 (18)
theorem :: RasiowaNonClassical: p 69 (17)
a "/\" -a <= b "\/" -b
proof
-(b "\/" -b) = (-b) "/\" (--b) by Th1
.= b "/\" -b by ROBBINS3:def 6;
then -(b "\/" -b) < -(a "/\" -a) by Def13;
hence thesis by Def13,Th5;
end;
Lm4: ::RasiowaNonClassical: p 71 (51)
(-a) "\/" (-b) "/\" a < -b
proof
((-b) "/\" a) <= (-b) by LATTICES:4,6;
then
A1: (-b) "/\" a < (-b) by Th5;
(-a) "/\" a < (-b) by Def13;
then ((-a) "/\" a) "\/" ((-b) "/\" a) < (-b) "\/" (-b) by A1,Lm2;
hence thesis by LATTICES:def 11;
end;
Lm5: ::RasiowaNonClassical: p 71 (52)
a < (-( a "/\" b)) => -b
proof
(-a) "\/" (-b) "/\" a < -b by Lm4;
then a < ((-a) "\/" (-b)) => -b by Def4;
hence thesis by Th8;
end;
Lm6: ::RasiowaNonClassical: p 72 (55)
-(b =-> (a "/\" b)) < -a
proof
A1: (-b) "\/" (-a) "/\" b < -a by Lm4;
then
A2: (-(a "/\" b)) "/\" b < -a by Th8;
-((-(a "/\" b)) => (-b)) < ((-(a "/\" b)) "/\" -(-b)) by Def10;
then -((-(a "/\" b)) => (-b)) < (-(a "/\" b)) "/\" b by ROBBINS3:def 6;
then
A3: -((-(a "/\" b)) => (-b)) < -a by A2,Def3;
A4: b "/\" (-(b "/\" a)) < -a by A1,Th8;
-(b => (a "/\" b)) < (b "/\" -(a "/\" b)) by Def10;
then
A5: -(b => (a "/\" b)) < -a by A4,Def3;
-(b =-> (a "/\" b))
= (-((-(a "/\" b)) => (-b))) "\/" -(b => (a "/\" b)) by Th8;
hence thesis by A3,A5,Def7;
end;
theorem :: RasiowaNonClassical: p 69 (18)
a <= b =-> (a "/\" b)
proof
A1: a < b => (b "/\" a) & a < (-(b "/\" a)) => -b by Lm5,Th19bis;
-( b =-> (b "/\" a)) < -a by Lm6;
hence thesis by A1,Th5,Def8;
end;
::NdR RasiowaNonClassical: p 70 1.3 (19)
theorem Th20: :: (2.20)
a => !b = b => !a
proof
(a => !b) = a => (b => (-Top L)) by Def14
.= b => (a => (-Top L)) by Th18
.= b => !a by Def14;
hence thesis;
end;
::NdR RasiowaNonClassical: p 70 1.3 (20)
theorem Th21: :: (2.21)
(a => Top L) = Top L
proof
a <= Top L by LATTICES:4,19; then
a < Top L by Th5;
hence thesis;
end;
::NdR RasiowaNonClassical: p 70 1.3 (21)
theorem Th22: :: (2.22)
((Bottom L) => a) = Top L
proof
Bottom L <= a; then
Bottom L < a by Th5;
hence thesis;
end;
::NdR RasiowaNonClassical: p 70 1.3 (22)
theorem Th23: :: (2.23)
((Top L) => b) = b
proof
(b "/\" (Top L)) < b by Def2; then
A1: b < ((Top L) => b) by Def4;
-((Top L) => b) < ((Top L) "/\" -b) by Def10; then
A2: b <= ((Top L) => b) by A1,Th5;
A3: (Top L) "/\" ((Top L) => b) < b by Th17;
(Top L) "/\" -b < -((Top L) => b) by Def9; then
((Top L) => b) <= b by Th5,A3;
hence thesis by A2,Th3;
end;
::NdR RasiowaNonClassical: p 70 1.3 (23)
theorem :: (2.24)
a = Top L & a => b = Top L implies b = Top L by Th23;
::NdR RasiowaNonClassical: p 70 1.3 (24)
theorem Th24: :: (2.25)
a => (b => a) = Top L
proof
b "/\" a <= a by LATTICES:4,6; then
b "/\" a < a by Th5; then
a < b => a by Def4;
hence thesis;
end;
::NdR RasiowaNonClassical: p 70 1.3 (25)
theorem Th25: :: (2.26)
((a => (b => c)) => ((a => b) => (a => c))) = Top L
proof
a "/\" (a => b) < b by Th17; then
a "/\" (a => b) "/\" (a => (b => c)) < b "/\" (a => (b => c))
by Lm1; then
a "/\" (a => b) "/\" (a => (b => c)) < b "/\" (b => (a => c))
by Th18; then
A1: a "/\" (a => b) "/\" (b => (a => c)) < b "/\" (b => (a => c)) by Th18;
A2: b "/\" (b => (a => c)) < a => c by Th17;
a "/\" (a => b) "/\" (b => (a => c)) < a => c by Def3,A1,A2; then
a "/\" (a "/\" (a => b) "/\" (b => (a => c))) < c by Def4; then
a "/\" (a "/\" ((a => b) "/\" (b => (a => c)))) < c by LATTICES:def 7; then
(a "/\" a) "/\" ((a => b) "/\" (b => (a => c))) < c by LATTICES:def 7; then
a "/\" ((a => b) "/\" (a => (b => c))) < c by Th18; then
(a => b) "/\" (a => (b => c)) < (a => c) by Def4; then
(a => (b => c)) < ((a => b) => (a => c)) by Def4;
hence thesis;
end;
::NdR RasiowaNonClassical: p 70 1.3 (26)
theorem Th26: :: (2.27)
(a => (a "\/" b)) = Top L
proof
a < a "\/" b by Th7;
hence thesis;
end;
::NdR RasiowaNonClassical: p 70 1.3 (27)
theorem Th27: :: (2.28)
b => (a "\/" b) = Top L
proof
b < a "\/" b by Th7;
hence thesis;
end;
::NdR RasiowaNonClassical: p 70 1.3 (28)
theorem Th28: :: (2.29)
(a => c) => ((b => c) => ((a "\/" b) => c)) = Top L
proof
A1: a "/\" (a => c) < c by Th17;
A2: b "/\" (b => c) < c by Th17;
(a "/\" (a => c)) "/\" (b => c) < (a "/\" (a => c)) by Th6; then
A3: (a "/\" (a => c)) "/\" (b => c) < c by A1,Def3;
(b "/\" (b => c)) "/\" (a => c) < (b "/\" (b => c)) by Th6; then
(b "/\" (b => c)) "/\" (a => c) < c by A2,Def3; then
(a "/\" (a => c) "/\" (b => c)) "\/" (b "/\" (b => c)"/\" (a => c)) < c
by Def7,A3; then
(a "/\" ((a => c) "/\" (b => c))) "\/" (b "/\" (b => c) "/\" (a => c)) < c
by LATTICES:def 7; then
(a "/\" ((a => c) "/\" (b => c))) "\/" ( b "/\" ((b => c)"/\" (a => c)))
< c by LATTICES:def 7; then
((b => c) "/\" (a => c)) "/\" (a "\/" b) < c by LATTICES:def 11; then
((b => c) "/\" (a => c)) < (a "\/" b) => c by Def4; then
(a => c) < (b => c) => ((a "\/" b) => c) by Def4;
hence thesis;
end;
::NdR RasiowaNonClassical: p 70 1.3 (29)
theorem Th29: :: (2.30)
(a "/\" b) => a = Top L
proof
a "/\" b < a by Th6;
hence thesis;
end;
::NdR RasiowaNonClassical: p 70 1.3 (30)
theorem Th30: :: (2.31)
(a "/\" b) => b = Top L
proof
a "/\" b < b by Th6;
hence thesis;
end;
::NdR RasiowaNonClassical: p 70 1.3 (31)
theorem Th31: :: (2.32)
(a => b) => ((a => c) => (a => (b "/\" c))) = Top L
proof
A1: a "/\" (a => c) < c by Th17;
A2: a "/\" (a => b) < b by Th17;
(a "/\" (a => c)) "/\" (a "/\" (a => b)) < c "/\" b by Lm2,A1,A2; then
((a => c) "/\" a) "/\" a "/\" ((a => b)) < c "/\" b
by LATTICES:def 7; then
(a => c) "/\" (a "/\" a) "/\" ((a => b)) < c "/\" b
by LATTICES:def 7; then
a "/\" ((a => c) "/\" (a => b)) < b "/\" c by LATTICES:def 7; then
((a => c) "/\" (a => b)) < (a => (b "/\" c)) by Def4; then
(a => b) < ((a => c) => (a => (b "/\" c))) by Def4;
hence thesis;
end;
::NdR RasiowaNonClassical: p 70 1.3 (32)
theorem Th32: :: (2.33)
(a => !b) => (b => !a) = Top L
proof
a => !b = b => !a by Th20;
hence thesis by Th16ter;
end;
::NdR RasiowaNonClassical: p 70 1.3 (33)
theorem Th33: :: (2.34)
(!(a => a)) => b = Top L
proof
A1: a => a = Top L by Th16ter;
A2: !(Top L) = ((Top L) => - (Top L)) by Def14;
(!a => a) => b = ((Top L) => (Bottom L)) => b by Th2,A2,A1
.= (Bottom L) => b by Th23
.= Top L by Th22;
hence thesis;
end;
::NdR RasiowaNonClassical: p 70 1.3 (34)
theorem Th34: :: (2.35)
(-a) => (a => b) = Top L
proof
a "/\" -a < b by Def13; then
(-a) < (a => b) by Def4;
hence thesis;
end;
::NdR RasiowaNonClassical: p 70 1.3 (35)
theorem Th35: :: (2.36)
((-(a => b)) => (a "/\" -b)) "/\" ((a "/\" -b) => -(a => b)) = Top L
proof
A1: -(a => b) < (a "/\" -b) by Def10;
(a "/\" -b) < -(a => b) by Def9;
hence thesis by A1;
end;
::NdR RasiowaNonClassical: p 70 1.3 (36)
theorem Th36: :: (2.37)
((-!a) => a) "/\" (a => (-!a)) = Top L
proof
A1: -!a < a by Def12;
a < -!a by Def11;
hence thesis by A1;
end;
::NdR RasiowaNonClassical: p 70 1.3 (37)
theorem :: (2.38)
--a = a by ROBBINS3:def 6;
::NdR RasiowaNonClassical: p 70 1.3 (39)
theorem Th37: :: (2.39)
-(a "\/" b) = ((-a) "/\" (-b))
proof
(a "\/" b)` = (a`` "\/" b)` by ROBBINS3:def 6
.= (a`` "\/" b``)` by ROBBINS3:def 6
.= (a` "/\" b`)`` by Def1
.= (a` "/\" b`) by ROBBINS3:def 6;
hence thesis;
end;
::NdR RasiowaNonClassical: p 70 1.3 (38)
theorem :: (2.40)
-(a "/\" b) = ((-a) "\/" (-b))
proof
(a "/\" b)` = (a`` "/\" b)` by ROBBINS3:def 6
.= (a`` "/\" b ``)` by ROBBINS3:def 6
.= (a` "\/" b`)`` by Th1
.= (a` "\/" b`) by ROBBINS3:def 6;
hence thesis;
end;
::NdR RasiowaNonClassical: p 70 1.3 (40)
theorem Th38: :: (2.41)
a < b implies b => c < a => c & c => a < c => b
proof
assume
A1: a < b;
(Top L) => (a => c) = (a => c) by Th23; then
A2: (a => (b => c)) < (a => c) by A1,Th25;
(a "/\" (b => c)) < (b => c) by Th6; then
A3: (b => c) < (a => (b => c)) by Def4;
A4: c => Top L = Top L by Th21;
(c => (a => b)) => ((c => a) => (c => b)) = Top L by Th25;
hence thesis by A1,A2,A3,A4,Th23,Def3;
end;
::NdR RasiowaNonClassical: p 70 1.3 (41)
theorem :: (2.42)
(a => b) => ((c => d) => ((a "/\" c) => (b "/\" d))) = Top L
proof
A1: (a "/\" (a => b)) < b by Th17;
(c "/\" (c => d)) < d by Th17; then
(c "/\" (c => d)) "/\" (a "/\" (a => b)) < (b "/\" d) by Lm2,A1; then
(c "/\" (c => d))"/\" a "/\" ((a => b)) < (d "/\" b)
by LATTICES:def 7; then
(a "/\" c "/\" (c => d)) "/\" ((a => b)) < (b "/\" d)
by LATTICES:def 7; then
(a "/\" c) "/\" ((c => d) "/\" (a => b)) < (b "/\" d)
by LATTICES:def 7; then
(c => d) "/\" (a => b) < ((a "/\" c) => (b "/\" d)) by Def4; then
(a => b) < ((c => d) => ((a "/\" c) => (b "/\" d))) by Def4;
hence thesis;
end;
::NdR RasiowaNonClassical: p 70 1.3 (42)
theorem :: (2.43)
(a => b) => ((c => d) => ((a "\/" c) => (b "\/" d))) = Top L
proof
((c => d) "/\" (a => b)) < (a => b) by Th6; then
A1: (((c => d) "/\" (a => b)) "/\" a) < b by Def4;
((c => d) "/\" (a => b)) < (c => d) by Th6; then
(c "/\" ((c => d) "/\" (a => b))) < d by Def4; then
(((c => d) "/\" (a => b)) "/\" a) "\/" (((c => d) "/\" (a => b)) "/\" c) <
(b "\/" d) by Lm2,A1; then
((c => d) "/\" (a => b)) "/\" (a "\/" c) < (b "\/" d)
by LATTICES:def 11; then
(c => d) "/\" (a => b) < ((a "\/" c) => (b "\/" d)) by Def4; then
(a => b)< ((c => d) => ((a "\/" c) => (b "\/" d))) by Def4;
hence thesis;
end;
::NdR RasiowaNonClassical: p 70 1.3 (43)
theorem :: (2.44)
(b => a) => ((c => d) => ((a => c) => (b => d))) = Top L
proof
A1: c "/\" (c => d) < d by Th17;
a "/\" (a => c) < c by Th17; then
a "/\" (a => c) "/\" (c => d) < c "/\" (c => d) by Lm1; then
A2: a "/\" (a => c) "/\" (c => d) < d by Def3,A1;
b "/\" (b => a) < a by Th17; then
(a => c) "/\" (b "/\" (b => a)) < (a => c) "/\" a &
(a => c) "\/" (b "/\" (b => a)) < (a => c) "\/" a by Lm1; then
(a => c) "/\" (b "/\" (b => a))"/\" (c => d) <
(a => c) "/\" a "/\" (c => d) by Lm1; then
(a => c) "/\" (b "/\" (b => a))"/\" (c => d) < d by A2,Def3; then
(a => c) "/\" (c => d) "/\" (b "/\" (b => a)) < d by LATTICES:def 7; then
((a => c) "/\" (c => d)) "/\" b "/\" (b => a) < d by LATTICES:def 7; then
(a => c) "/\" b "/\" (c => d) "/\" (b => a) < d by LATTICES:def 7; then
b "/\" (a => c) "/\" ((c => d) "/\" (b => a)) < d by LATTICES:def 7; then
b "/\"((a => c) "/\" ((c => d) "/\" (b => a))) < d by LATTICES:def 7; then
(a => c) "/\" ((c => d) "/\" (b => a)) < (b => d) by Def4; then
((c => d) "/\" (b => a)) < (a => c) => (b => d) by Def4; then
(b => a) < ((c => d) => ((a => c) => (b => d))) by Def4;
hence thesis;
end;
begin :: Alternative Equational Axiomatics by Rasiowa
definition let L be non empty NelsonStr;
attr L is satisfying_N0* means
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
for a, b being Element of L holds
a => (b => a) = Top L;
::NdR RasiowaNonClassical: p 75 qpB2*
attr L is satisfying_N2* means
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
for a being Element of L holds
((Top L) => a) = a;
::NdR RasiowaNonClassical: p 76 qpB5*
attr L is satisfying_N5* means
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
for a, b being Element of L holds
a => (a "\/" b) = Top L;
::NdR RasiowaNonClassical: p 76 qpB7*
attr L is satisfying_N7* means
for a, b being Element of L holds
b => (a "\/" b) = Top L;
::NdR RasiowaNonClassical: p 77 qpB8*
attr L is satisfying_N8* means
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
for a, b being Element of L holds
(a "/\" b) => a = Top L;
::NdR RasiowaNonClassical: p 77 qpB10*
attr L is satisfying_N10* means
for a, b being Element of L holds
(a "/\" b) => b = Top L;
::NdR RasiowaNonClassical: p 77 qpB11*
attr L is satisfying_N11* means
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
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
for a, b being Element of L holds
(!(a => a)) => b = Top L;
::NdR RasiowaNonClassical: p 77 qpB14*
attr L is satisfying_N14* means
for a, b being Element of L holds
(-a) => (a => b) = Top L;
::NdR RasiowaNonClassical: p 77 qpB15*
attr L is satisfying_N15* means
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
for a, b being Element of L holds
-(a "\/" b) = ((-a) "/\" (-b));
::NdR RasiowaNonClassical: p 77 qpB19*
attr L is satisfying_N19* means
for a being Element of L holds
((-!a) => a) "/\" (a => (-!a)) = Top L;
end;
notation
let L be non empty NelsonStr;
::NdR RasiowaNonClassical: p 77 qpB4*
synonym L is satisfying_N4* for L is satisfying_N4;
::NdR RasiowaNonClassical: p 77 qpB16*
synonym L is satisfying_N16* for L is DeMorgan;
::NdR RasiowaNonClassical: p 77 qpB18*
synonym L is satisfying_N18* for L is involutive;
end;
registration
cluster -> satisfying_N1* satisfying_N2* satisfying_N3* satisfying_N4*
satisfying_N5* satisfying_N6* satisfying_N7* satisfying_N8*
satisfying_N9* satisfying_N10* satisfying_N11* satisfying_N12*
satisfying_N13* satisfying_N14* satisfying_N15* satisfying_N16*
satisfying_N17* satisfying_N18* satisfying_N19* for Nelson_Algebra;
coherence
proof
let L be Nelson_Algebra;
thus L is satisfying_N1* by Th24;
thus L is satisfying_N2* by Th25;
thus L is satisfying_N3* by Th23;
thus L is satisfying_N4*;
thus L is satisfying_N5*
proof
now let a, b be Element of L;
set ab = a =-> b;
set ba = b =-> a;
A1: (ab => (ba => b)) < (ba => (ab => a))
proof
A2: b < (b => a) => a by Th19;
A3: ((b => a) => a) < ((-a) => (-b)) => ((b => a) => a) by Th24;
A4: ((-a) => (-b)) => ((b => a) => a) =
((-a) => (-b) "/\" (b => a)) => a by Lm3;
b < ba => a by Def3,A2,A3,A4; then
(ba => b) < ba => (ba => a) by Th38; then
ab => ((b =-> a) => b) < ab => (ba => (ba => a)) by Th38; then
ab => (ba => b) < (a =-> b) => ((ba "/\" ba) => a) by Lm3;
hence thesis by Th18;
end;
A5: (-a) "/\" ((-a) => (-b)) < (-b) by Th17;
A6: -(ba => (ab => a)) < -(ab => (ba => b))
proof
A7: ab "/\" ba < ab "/\" ba by Def2;
(ab "/\" ba) "/\" ((-a) "/\" ((-a) => (-b))) =
(ab "/\" (b => a) "/\" ((-a) => (-b))) "/\"
((-a) "/\" ((-a) => (-b))) by LATTICES:def 7
.= (ab "/\" (b => a) "/\" ((-a) => (-b))) "/\" ((-a) =>
(-b)) "/\" (-a) by LATTICES:def 7
.= ab "/\" (b => a) "/\" (((-a) => (-b)) "/\" ((-a) =>
(-b))) "/\" (-a) by LATTICES:def 7
.= ab "/\" ((b => a) "/\" ((-a) => (-b))) "/\" (-a)
by LATTICES:def 7
.= ab "/\" (ba "/\" (-a)) by LATTICES:def 7; then
A8: ab "/\" (ba "/\" (-a)) < ab "/\" ba "/\" (-b) by A7,Lm2,A5;
-(ba => a) < (ba "/\" (-a)) by Def10; then
A9: ab "/\" (-(ba => a)) < ab "/\" (ba "/\" (-a)) by Lm1;
A10: -(ab => (ba => a)) < ab "/\" (-(ba => a)) by Def10;
ba "/\" (-b) < -(ba => b) by Def9; then
A11: ab "/\" (ba "/\" (-b)) < ab "/\" (-(ba => b)) by Lm1;
ab "/\" (-(ba => b)) < -(ab => (ba => b)) by Def9; then
ab "/\" (ba "/\" (-b)) < -(ab => (ba => b)) by Def3, A11; then
ab "/\" ba "/\" (-b) < -(ab => (ba => b)) by LATTICES:def 7; then
ab "/\" (ba "/\" (-a)) < -(ab => (ba => b)) by Def3,A8; then
ab "/\" (-(ba => a)) < -(ab => (ba => b)) by Def3, A9; then
-(ab => (ba => a)) < -(ab => (ba => b)) by Def3,A10;
hence thesis by Th18;
end;
A12: (ba => (ab => a)) < (ab => (ba => b))
proof
A13: a < (a => b) => b by Th19;
A14: (a => b) => b < ((-b) => (-a)) => ((a => b) => b) by Th24;
A15: ((-b) => (-a)) => ((a => b) => b) =
((-b) => (-a) "/\" (a => b)) => b by Lm3;
a < ab => b by Def3,A13,A14,A15; then
(ab => a) < ab => (ab => b) by Th38; then
ba => (ab => a) < ba => (ab => (ab => b)) by Th38; then
ba => (ab => a) < ba => ((ab "/\" ab) => b) by Lm3;
hence thesis by Th18;
end;
A16: -(ab => (ba => b)) < -(ba => (ab => a))
proof
A17: (-b) "/\" ((-b) => (-a)) < (-a) by Th17;
A18: ba "/\" ab < ba "/\" ab by Def2;
(ba "/\" ab) "/\" ((-b) "/\" ((-b) => (-a))) =
(ba "/\" (a => b) "/\" ((-b) => (-a))) "/\"
((-b) "/\" ((-b) => (-a))) by LATTICES:def 7
.= (ba "/\" (a => b) "/\" ((-b) => (-a))) "/\"
((-b) => (-a)) "/\" (-b) by LATTICES:def 7
.= ba "/\" (a => b) "/\" (((-b) => (-a)) "/\"
((-b) => (-a))) "/\" (-b) by LATTICES:def 7
.= ba "/\" ((a => b) "/\" ((-b) => (-a))) "/\" (-b)
by LATTICES:def 7
.= ba "/\" (ab "/\" (-b)) by LATTICES:def 7; then
A19: ba "/\" (ab "/\" (-b)) < ba "/\" ab "/\" (-a) by A18,Lm2,A17;
(-(ab => b)) < (ab "/\" (-b)) by Def10; then
A20: ba "/\" (-(ab => b)) < ba "/\" (ab "/\" (-b)) by Lm1;
A21: -(ba => (ab => b)) < ba "/\" (-(ab => b)) by Def10;
ab "/\" (-a) < -(ab => a) by Def9; then
A22: ba "/\" (ab "/\" (-a)) < ba "/\" (-(ab => a)) by Lm1;
ba "/\" (-(ab => a)) < -(ba => (ab => a)) by Def9; then
ba "/\" (ab "/\" (-a)) < -(ba => (ab => a)) by Def3, A22; then
ba "/\" ab "/\" (-a) < -(ba => (ab => a)) by LATTICES:def 7; then
ba "/\" (ab "/\" (-b)) < -(ba => (ab => a)) by Def3,A19; then
ba "/\" (-(ab => b)) < -(ba => (ab => a)) by Def3, A20; then
-(ba => (ab => b)) < -(ba => (ab => a)) by Def3,A21;
hence thesis by Th18;
end;
A23: (ab => (ba => b)) <= (ba => (ab => a)) by A6,A1,Th5;
(ba => (ab => a)) <= (ab => (ba => b)) by A12,A16,Th5;
hence (ab => (ba => b)) = (ba => (ab => a)) by A23,Th3;
end;
hence thesis;
end;
thus L is satisfying_N6* by Th26;
thus L is satisfying_N7* by Th27;
thus L is satisfying_N8* by Th28;
thus L is satisfying_N9* by Th29;
thus L is satisfying_N10* by Th30;
thus L is satisfying_N11* by Th31;
thus L is satisfying_N12* by Th32;
thus L is satisfying_N13* by Th33;
thus L is satisfying_N14* by Th34;
thus L is satisfying_N15* by Th35;
thus L is satisfying_N16*;
thus L is satisfying_N17* by Th37;
thus L is satisfying_N18*;
thus L is satisfying_N19* by Th36;
end;
end;
theorem
for L be non empty NelsonStr st
L is satisfying_N0* holds
L is Nelson_Algebra iff
L is satisfying_N1* satisfying_N2* satisfying_N3* satisfying_N4*
satisfying_N5* satisfying_N6* satisfying_N7* satisfying_N8*
satisfying_N9* satisfying_N10* satisfying_N11* satisfying_N12*
satisfying_N13* satisfying_N14* satisfying_N15* satisfying_N16*
satisfying_N17* satisfying_N18* satisfying_N19*
proof
let L be non empty NelsonStr;
assume
A1: L is satisfying_N0*;
thus L is Nelson_Algebra implies L is satisfying_N1* satisfying_N2*
satisfying_N3* satisfying_N4* satisfying_N5* satisfying_N6*
satisfying_N7* satisfying_N8* satisfying_N9* satisfying_N10*
satisfying_N11* satisfying_N12* satisfying_N13* satisfying_N14*
satisfying_N15* satisfying_N16* satisfying_N17* satisfying_N18*
satisfying_N19*;
assume
A2: L is satisfying_N1* satisfying_N2* satisfying_N3* satisfying_N4*
satisfying_N5* satisfying_N6* satisfying_N7* satisfying_N8*
satisfying_N9* satisfying_N10* satisfying_N11* satisfying_N12*
satisfying_N13* satisfying_N14* satisfying_N15* satisfying_N16*
satisfying_N17* satisfying_N18* satisfying_N19*; then
reconsider L1 = L as DeMorgan non empty NelsonStr;
A3: for a, b being Element of L1 holds a "/\" b = Top L1 implies
a = Top L1 & b = Top L1
proof
let a, b be Element of L1;
assume a "/\" b = (Top L1); then
Top L1 < a & Top L1 < b by A2;
hence thesis by A2;
end;
set w = Top L1;
A4: w => w = w by A2; then
w => ((w => w) => (w => (w "/\" w))) = w by A2; then
(w => (w => (w "/\" w))) = w by A4,A2; then
(w => (w "/\" w)) = w by A2; then
A5: w "/\" w = w by A2;
A6: for a, b being Element of L1 holds a <= b iff a < b & -b < -a
proof
let a, b be Element of L1;
A7: a =-> b = (a => b) "/\" ((-b) => (-a)) by A2;
thus a <= b implies a < b & -b < -a
proof
assume a <= b; then
a =-> b = Top L1 by A1;
hence thesis by A3,A7;
end;
assume a < b & -b < -a;
hence thesis by A7,A5,A1;
end;
set d = (Top L)`;
A8: for a being Element of L holds a <= Top L
proof
let a be Element of L;
a => Top L = (Top L) => (a => Top L) by A2; then
A9: a < Top L by A2;
(-Top L) => (Top L => -a) = Top L by A2; then
-Top L < -a by A2;
hence thesis by A6,A9;
end;
A10: for a being Element of L holds d <= a
proof
let a be Element of L;
(-Top L) => (Top L => a) = Top L by A2; then
A11: -Top L < a by A2;
-a <= Top L by A8; then
-a < Top L by A2; then
-a < -d by A2;
hence thesis by A11,A6;
end;
A12: for a being Element of L holds d "/\" a = d
proof
let a be Element of L;
d <= a by A10;
hence thesis;
end;
A13: for a being Element of L1 holds a => (Top L1) = (Top L1)
proof
let a be Element of L1;
(Top L1) => (a => (Top L1)) = Top L1 by A2;
hence thesis by A2;
end;
A14: for a, b, c being Element of L1 holds
a => b = (Top L1) & b => c = (Top L1) implies a => c = (Top L1)
proof
let a, b, c be Element of L1;
assume
A15: (a => b) = (Top L1) & b => c = (Top L1);
(a => c) = (Top L1) => (a => c) by A2
.= (Top L1) => ((Top L1) => (a => c)) by A2
.= (a => (Top L1)) => ((Top L1) => (a => c)) by A13
.= (Top L1) by A2,A15;
hence thesis;
end;
A16: L1 is satisfying_A1b
proof
let a, b, c be Element of L1;
assume a < b & b < c;
hence thesis by A14;
end;
A17: L1 is satisfying_N6
proof
let a, b, c be Element of L1;
assume
A18: a < c & b < c;
(a => c) => ((b => c) => ((a "\/" b) => c)) = Top L1 by A2; then
((b => c) => ((a "\/" b) => c)) = Top L1 by A18,A2;
hence thesis by A2,A18;
end;
A19: for a being Element of L1 holds a => a = Top L1
proof
let a be Element of L1;
A20: (a => ((a => a) => a)) => ((a => (a => a)) => (a => a)) = Top L1
by A2;
a => ((a => a) => a) = Top L1 by A2; then
A21: ((a => (a => a)) => (a => a)) = Top L1 by A20,A2;
a => (a => a) = Top L1 by A2;
hence thesis by A21,A2;
end;
A22: L1 is satisfying_N7
proof
let a, b, c be Element of L1;
assume
A23: a < b & a < c;
(a => b) => ((a => c) => (a => (b "/\" c))) = Top L1 by A2; then
(a => c) => (a => (b "/\" c)) = Top L1 by A23,A2;
hence thesis by A2,A23;
end;
A24: for a, b being Element of L1 holds b < a "\/" b by A2;
A25: for a, b being Element of L1 holds a "/\" b <= a
proof
let a, b be Element of L1;
A26: -(a "/\" b) = (-a) "\/" (-b) by A2;
A27: a "/\" b < a by A2;
-a < (-a) "\/" (-b) by A2;
hence thesis by A27,A6,A26;
end;
A28: for a, b being Element of L1 holds a <= a "\/" b
proof
let a, b be Element of L1;
A29: (-a) "/\" (-b) < -a by A2;
A30: a < a "\/" b by A2;
-(a "\/" b) = (-a) "/\" (-b) by A2;
hence thesis by A29,A30,A6;
end;
A31: for a, b being Element of L1 holds b <= a "\/" b
proof
let a, b be Element of L1;
A32: b < a "\/" b by A2;
A33: -(a "\/" b) = (-a) "/\" (-b) by A2;
(-a) "/\" (-b) < -b by A2;
hence thesis by A6,A32,A33;
end;
A34: for a, b being Element of L1 holds a "/\" b <= b
proof
let a, b be Element of L1;
A35: -(a "/\" b) = (-a) "\/" (-b) by A2;
A36: a "/\" b < b by A2;
-b < (-a) "\/" (-b) by A2;
hence thesis by A35,A36,A6;
end;
A37: for a being Element of L1 holds a =-> a = Top L1
proof
let a be Element of L1;
a =-> a = (a => a) "/\" ((-a) => -a) by A2
.= (Top L1) "/\" ((-a) => -a) by A19
.= Top L1 by A19,A5;
hence thesis;
end;
A38:
for a, b being Element of L1 holds
a = b iff a =-> b = Top L1 & b =-> a = Top L1
proof
let a, b be Element of L1;
a =-> b = Top L1 & b =-> a = Top L implies a = b
proof
assume
A39: a =-> b = Top L1 & b =-> a = Top L; then
(b =-> a) => ((a =-> b) => a) = (Top L1) => ((b =-> a) => b)
by A2; then
(b =-> a) => ((a =-> b) => a) = (Top L1) => b by A2,A39; then
(b =-> a) => ((Top L1) => a) = b by A39,A2; then
(Top L1) => a = b by A39,A2;
hence thesis by A2;
end;
hence thesis by A37;
end;
A40: for a, b being Element of L1 holds a <= b & b <= a iff a = b
proof
let a, b be Element of L1;
thus a <= b & b <= a implies a = b
proof
assume a <= b & b <= a; then
a =-> b = Top L & b =-> a = Top L by A1;
hence thesis by A38;
end;
assume a = b; then
a =-> b = Top L & b =-> a = Top L by A38;
hence thesis by A1;
end;
A41: for b being Element of L1 holds Top L1 < b implies b = Top L1 by A2;
A42: L1 is satisfying_A1
proof
let a be Element of L1;
thus thesis by A19;
end;
A43: for a, b, c being Element of L1 holds
a < b implies b => c < a => c & c => a < c => b
proof
let a, b, c be Element of L1;
assume
A44: a < b;
A45: b => c < a => (b => c) by A2;
a => (b => c) < ((a => b) => (a => c)) by A2; then
A46: (b => c) < ((a => b) => (a => c)) by A45,A16;
(c => (Top L1)) => ((c => a) => (c => b)) = (Top L1) by A2,A44; then
(Top L1) => ((c => a) => (c => b)) = (Top L1) by A13;
hence thesis by A46,A2,A44;
end;
A47: for a, b being Element of L1 holds a => (b => (a "/\" b)) = Top L1
proof
let a, b be Element of L1;
(b => a) < ((b => b) => (b => (a "/\" b))) by A2; then
(b => a) < ((Top L1) => (b => (a "/\" b))) by A19; then
(b => a) < (b => (a "/\" b)) by A2; then
a => (b => a) < a => (b => (a "/\" b)) by A43; then
(Top L1) < a => (b => (a "/\" b)) by A2;
hence thesis by A2;
end;
A48: for a,b,c being Element of L1 st
a < (b => c) holds b < (a => c)
proof
let a, b, c be Element of L1;
assume
A49: a < (b => c);
a => (b => c) < (a => b) => (a => c) by A2; then
A50: (a => b) < (a => c) by A2,A49;
b < (a => b) by A2;
hence thesis by A50,A16;
end;
A51: for a, c being Element of L1 holds a => (a => c) < a => c
proof
let a, c be Element of L1;
a => (a => c) < (a => a) => (a => c) by A2; then
a => (a => c) < (Top L1) => (a => c) by A19;
hence thesis by A2;
end;
A52: L1 is satisfying_N3
proof
let x, a, b be Element of L1;
A53: a "/\" x < b implies x < a => b
proof
assume a "/\" x < b; then
(x => (a "/\" x)) < (x => b) by A43; then
A54: a => (x => (a "/\" x)) < a => (x => b) by A43;
a => (x => (a "/\" x)) = (Top L1) by A47; then
a < (x => b) by A2,A54;
hence thesis by A48;
end;
x < a => b implies a "/\" x < b
proof
assume
A55: x < a => b;
(a "/\" x) < x by A2; then
(a "/\" x) < a => b by A55,A16; then
A56: a < (a "/\" x) => b by A48;
a "/\" x < a by A2; then
a "/\" x < (a "/\" x) => b by A16,A56;
hence thesis by A41,A51;
end;
hence thesis by A53;
end;
A57: for a, b, c being Element of L1 st
b < c holds a "/\" b < a "/\" c
proof
let a, b, c be Element of L1;
assume
A58: b < c;
a "/\" b < b by A2; then
A59: a "/\" b < c by A58,A16;
a "/\" b < a by A2;
hence thesis by A22,A59;
end;
A58: for a, b, c being Element of L1 st
b < c holds a "\/" b < a "\/" c
proof
let a, b, c be Element of L1;
assume
A60: b < c;
A61: a < a "\/" c by A2;
c < a "\/" c by A2; then
b < a "\/" c by A60,A16;
hence thesis by A61,A17;
end;
A62: for a, b, c being Element of L1 st
a <= c & b <= c holds a "\/" b <= c
proof
let a, b, c be Element of L1;
assume
A63: a <= c & b <= c; then
A64: a < c & -c < -a by A6;
A65: b < c & -c < -b by A63,A6;
((-c) => (-a)) => (((-c) => (-b)) => ((-c) => ((-a) "/\" -b))) = Top L1
by A2; then
(((-c) => (-b)) => ((-c) => ((-a) "/\" -b))) = Top L1 by A64,A2; then
((-c) => ((-a) "/\" -b)) = Top L1 by A65,A2; then
-c < -(a "\/" b) by A2;
hence thesis by A65,A64,A17,A6;
end;
A66: for a, b, c being Element of L1 st
c <= a & c <= b holds c <= a "/\" b
proof
let a, b, c be Element of L1;
assume
A67: c <= a & c <= b; then
A68: c < a & -a < -c by A6;
A69: c < b & -b < -c by A67,A6;
((-a) => (-c)) => (((-b) => (-c)) => (((-a) "\/" -b) => -c)) = Top L1
by A2; then
(((-b) => (-c)) => (((-a) "\/" -b) => -c)) = Top L1 by A68,A2; then
((((-a) "\/" -b) => -c)) = Top L1 by A69,A2; then
-(a "/\" b) < -c by A2;
hence thesis by A69,A68,A22,A6;
end;
A70: for a,b being Element of L1 holds
b "\/" a <= a "\/" b
proof
let a,b be Element of L1;
A71: a <= a "\/" b by A28;
b <= a "\/" b by A31;
hence thesis by A71,A62;
end;
A72: for a,b being Element of L1 holds
a "\/" b = b "\/" a
proof
let a,b be Element of L1;
A73: a "\/" b <= b "\/" a by A70;
b "\/" a <= a "\/" b by A70;
hence thesis by A73,A40;
end;
A74: for a,b being Element of L1 holds
a "/\" b <= b "/\" a
proof
let a,b be Element of L1;
A75: a "/\" b <= a by A25;
a "/\" b <= b by A34;
hence thesis by A75,A66;
end;
for a,b being Element of L1 holds
a "/\" b = b "/\" a
proof
let a,b be Element of L1;
A76: a "/\" b <= b "/\" a by A74;
b "/\" a <= a "/\" b by A74;
hence thesis by A40,A76;
end; then
reconsider L1 as DeMorgan meet-commutative join-commutative
non empty NelsonStr by A72,LATTICES:def 4, def 6;
A77: for a, b, c being Element of L1 holds
a <= b implies a "\/" c <= b "\/" c
proof
let a,b,c be Element of L1;
assume a <= b; then
A78: a < b & -b < -a by A6; then
(-b) "/\" -c < (-a) "/\" -c by A57; then
- (b "\/" c) < (-a) "/\" -c by A2; then
- (b "\/" c) < - (a "\/" c) by A2;
hence thesis by A78,A58,A6;
end;
set d = -Top L1;
A79: for a being Element of L1 holds d "/\" a = d & a "/\" d = d by A12;
for a, b being Element of L1 holds
b = (a "/\" b) "\/" b
proof
let a, b be Element of L1;
A80: b <= (a "/\" b) "\/" b by A31;
a "/\" b <= b & b <= b by A40,A25; then
(a "/\" b) "\/" b <= b by A62;
hence thesis by A80,A40;
end; then
A81: L1 is meet-absorbing;
for a,b being Element of L1 holds
a "/\" (a "\/" b) = a
proof
let a, b be Element of L1;
a <= a & a <= a "\/" b by A40,A31;
hence thesis;
end; then
A82: L1 is join-absorbing;
A83: for a, b, c being Element of L1 holds
b <= c implies a "/\" b <= a "/\" c
proof
let a, b, c be Element of L1;
assume
A84: b <= c; then
A85: a "/\" b < a "/\" c by A57,A6;
-(a "/\" c) < -(a "/\" b)
proof
-c < -b by A84,A6; then
(-a) "\/" (-c) < (-a) "\/" (-b) by A58; then
-(a "/\" c) < (-a) "\/" (-b) by A2;
hence thesis by A2;
end;
hence thesis by A85,A6;
end;
A86: for a,b,c being Element of L1 st a <= b & b <= c holds a <= c
proof
let a,b,c be Element of L1;
assume a <= b & b <= c; then
a < b & b < c & -c < -b & -b < -a by A6; then
a < c & (-c) < -a by A14;
hence thesis by A6;
end;
A87: for a,b,c being Element of L1 holds
a "/\" (b "/\" c) = (a "/\" b) "/\" c
proof
let a,b,c be Element of L1;
A88: a "/\" (b "/\" c) <= a "/\" b by A34,A83;
A89: a "/\" (b "/\" c) <= b "/\" c by A34;
b "/\" c <= c by A34; then
a "/\" (b "/\" c) <= c by A86,A89; then
A90: a "/\" (b "/\" c) <= (a "/\" b) "/\" c by A88,A66;
A91: a "/\" b <= a by A25;
(a "/\" b) "/\" c <= a "/\" b by A25; then
A92: (a "/\" b) "/\" c <= a by A91,A86;
(a "/\" b) "/\" c <= b "/\" c by A25,A83; then
(a "/\" b) "/\" c <= a "/\" (b "/\" c) by A92,A66;
hence thesis by A90,A40;
end;
for a,b,c being Element of L1 holds
a "\/" (b "\/" c) = (a "\/" b) "\/" c
proof
let a,b,c be Element of L1;
A93: a <= a "\/" b by A28;
a "\/" b <= (a "\/" b) "\/" c by A28; then
A94: a <= (a "\/" b) "\/" c by A86,A93;
b "\/" c <= (a "\/" b) "\/" c by A28,A77; then
A95: a "\/" (b "\/" c) <= (a "\/" b) "\/" c by A94,A62;
A96: c <= b "\/" c by A28;
b "\/" c <= a "\/" (b "\/" c) by A28; then
A97: c <= a "\/" (b "\/" c) by A96,A86;
a "\/" b <= a "\/" (b "\/" c) by A28,A77; then
(a "\/" b) "\/" c <= a "\/" (b "\/" c) by A97,A62;
hence thesis by A95,A40;
end; then
L1 is join-associative meet-associative by A87; then
reconsider L1 as Lattice-like
lower-bounded DeMorgan non empty NelsonStr
by A81,A79,A82,LATTICES:def 13;
set c = Top L1;
for a being Element of L1 holds c "\/" a = c & a "\/" c = c
proof
let a be Element of L1;
a <= c by A8;
hence thesis by LATTICES:4,def 3;
end; then
L is upper-bounded; then
reconsider L1 as DeMorgan involutive bounded Lattice-like
non empty NelsonStr by A2;
A98: L1 is distributive
proof
let a, b, c be Element of L1;
A99: b < a => ((a "/\" b) "\/" (a "/\" c)) by A52,A24;
c < a => ((a "/\" b) "\/" (a "/\" c)) by A52,A24; then
A100: b "\/" c < a => ((a "/\" b) "\/" (a "/\" c)) by A99,A17;
A101: for a, b, c being Element of L1 holds
a "/\" (b "\/" c) < (a "/\" b) "\/" (a "/\" c)
proof
let a, b, c be Element of L1;
A102: b < a => ((a "/\" b) "\/" (a "/\" c)) by A52,A24;
c < a => ((a "/\" b) "\/" (a "/\" c)) by A52,A24; then
b "\/" c < a => ((a "/\" b) "\/" (a "/\" c)) by A102,A17;
hence thesis by A52;
end;
A103: ((-a) "\/" (-b)) "/\" ((-a) "\/" (-c)) <
(((-a) "\/" (-b)) "/\" (-a)) "\/" (((-a) "\/" (-b)) "/\" (-c)) by A101;
A104: (((-a) "\/" (-b)) "/\" (-a)) "\/" (((-a) "\/" (-b)) "/\" (-c)) =
(-a) "\/" (((-a) "\/" (-b)) "/\" (-c)) by LATTICES:def 9;
(-a) "\/"((-c) "/\" ((-a) "\/" (-b))) <
(-a) "\/" (((-c) "/\" (-a)) "\/" ((-c) "/\" (-b))) by A101,A58; then
A105:((-a) "\/" (-b)) "/\" ((-a) "\/" (-c)) <
(-a) "\/" (((-a) "/\" (-c)) "\/" ((-b) "/\" (-c))) by A16,A103,A104;
(-a) "\/" (((-a) "/\" (-c)) "\/" ((-b) "/\" (-c))) =
((-a) "\/" ((-a) "/\" (-c))) "\/" ((-b) "/\" (-c)) by LATTICES:def 5
.= (-a) "\/" ((-b) "/\" (-c)) by LATTICES:def 8
.= (-a) "\/" -(b "\/" c) by A2; then
((-a) "\/" (-b)) "/\" (-(a "/\" c)) < (-a) "\/" (-(b "\/" c))
by A2,A105; then
(-(a "/\" b)) "/\" (-(a "/\" c)) < (-a) "\/" (-(b "\/" c))
by A2; then
(-(a "/\" b)) "/\" (-(a "/\" c)) < -(a "/\" (b "\/" c)) by A2; then
-((a "/\" b) "\/" (a "/\" c)) < -(a "/\" (b "\/" c)) by A2; then
A106: a "/\" (b "\/" c) <= (a "/\" b) "\/" (a "/\" c) by A6,A100,A52;
A107: a "/\" b <= a "/\" (b "\/" c) by A28,A83;
a "/\" c <= a "/\" (b "\/" c) by A28,A83; then
(a "/\" b) "\/" (a "/\" c) <= a "/\" (b "\/" c) by A62,A107;
hence thesis by A106,A40;
end;
reconsider L1 as DeMorgan involutive bounded distributive Lattice-like
non empty NelsonStr by A98;
A108: L1 is satisfying_N5
proof
let a, b be Element of L1;
A109: a =-> b = Top L1 implies a "/\" b = a
proof
assume a =-> b = Top L1; then
a <= b by A1;
hence thesis;
end;
a "/\" b = a implies a =-> b = Top L1
proof
assume a "/\" b = a; then
a <= b;
hence thesis by A1;
end;
hence thesis by A109;
end;
A110: L1 is satisfying_N8
proof
let a, b be Element of L1;
((-(a => b)) => (a "/\" -b)) "/\" ((a "/\" -b) =>
(-(a => b))) = Top L1 by A2;
hence thesis by A3;
end;
A111: L1 is satisfying_N9
proof
let a, b be Element of L1;
((-(a => b)) => (a "/\" -b)) "/\" ((a "/\" -b) =>
(-(a => b))) = Top L1 by A2;
hence thesis by A3;
end;
A112: L1 is satisfying_N10
proof
let a be Element of L1;
((-!a) => a) "/\" (a => (-!a)) = Top L1 by A2;
hence thesis by A3;
end;
A113: L1 is satisfying_N11
proof
let a be Element of L1;
((-!a) => a) "/\" (a => (-!a)) = Top L1 by A2;
hence thesis by A3;
end;
A114: L1 is satisfying_N12
proof
let a, b be Element of L1;
(-a) < a => b by A2;
hence thesis by A52;
end;
A115: for a, b, c being Element of L1 holds !(Top L1) = -(Top L1)
proof
let a, b, c be Element of L1;
A116: -(Top L1) <= !(Top L1) by A10;
!(Top L1) <= -(Top L1)
proof
(!(a => a)) => -( Top L1) = (Top L1) by A2; then
A117: !(Top L1) < -(Top L1) by A19;
A118: -(-(Top L1)) = (Top L1) by A2;
(Top L1) < (-(!(Top L1))) by A112;
hence thesis by A117,A118,A6;
end;
hence thesis by A116,A40;
end;
A119: for a, b being Element of L1 holds a => !b = b => !a
proof
let a, b be Element of L1;
A120: a => !b < b => !a by A2;
A121: -(b => !a) < b "/\" -(!a) by A111;
b "/\" -(!a) < b "/\" a by A113,A57; then
A122: -(b => !a) < a "/\" b by A121,A16;
A123: a "/\" b < a "/\" -(!b) by A112,A57;
a "/\" -(!b) < -(a => !b) by A110; then
a "/\" b < -(a => !b) by A123,A16; then
-(b => !a) < -(a => !b) by A16,A122; then
A124: a => !b <= b => !a by A120,A6;
A125: b => !a < a => !b by A2;
A126: -(a => !b) < a "/\" -(!b) by A111;
a "/\" -(!b) < a "/\" b by A113,A57; then
A127: -(a => !b) < b "/\" a by A126,A16;
A128: b "/\" a < b "/\" -(!a) by A112,A57;
b "/\" -(!a) < -(b => !a) by A110; then
b "/\" a < -(b => !a) by A128,A16; then
-(a => !b) < -(b => !a) by A16,A127; then
b => !a <= a => !b by A125,A6;
hence thesis by A124,A40;
end;
L1 is satisfying_N13
proof
let a be Element of L1;
(!a) = (Top L1) => (!a) by A2
.= a => !(Top L1) by A119
.= a => -(Top L1) by A115;
hence thesis;
end;
hence thesis by A108,A42,A52,A2,A17,A22,A110,A111,A112,A113,A114,A16;
end;