:: Two Axiomatizations of {N}elson Algebras
:: by Adam Grabowski
::
:: Received April 19, 2015
:: Copyright (c) 2015 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, ROBBINS3;
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
(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)
::$N [see also \cite{RasiowaNonClassical} p. 69, Th. 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)
::$N [see also \cite{RasiowaNonClassical} p. 69, Th. 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)
::$N [see also \cite{RasiowaNonClassical} p. 69, Th. 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)
::$N [see also \cite{RasiowaNonClassical} p. 69, Th. 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)
::$N [see also \cite{RasiowaNonClassical} p. 69, Th. 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)
::$N [see also \cite{RasiowaNonClassical} p. 69, Th. 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)
::$N [see also \cite{RasiowaNonClassical} p. 69, Th. 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)
::$N [see also \cite{RasiowaNonClassical} p. 69, Th. 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)
::$N [see also \cite{RasiowaNonClassical} p. 69, Th. 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)
::$N [see also \cite{RasiowaNonClassical} p. 69, Th. 1.3 (14)]
theorem :: (2.16)
a =-> (b =-> c) = (a "/\" b) =-> c by Lm3;
::NdR RasiowaNonClassical: p 69 1.3 (15)
::$N [see also \cite{RasiowaNonClassical} p. 69, Th. 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)
::$N [see also \cite{RasiowaNonClassical} p. 69, Th. 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)
::$N [see also \cite{RasiowaNonClassical} p. 71, Th. 1.3 (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)
::$N [see also \cite{RasiowaNonClassical} p. 69, Th. 1.3 (17)]
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;
::$N [see also \cite{RasiowaNonClassical} p. 70, Th. 1.3 (18)]
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)
::$N [see also \cite{RasiowaNonClassical} p. 70, Th. 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)
::$N [see also \cite{RasiowaNonClassical} p. 70, Th. 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)
::$N [see also \cite{RasiowaNonClassical} p. 70, Th. 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)
::$N [see also \cite{RasiowaNonClassical} p. 70, Th. 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)
::$N [see also \cite{RasiowaNonClassical} p. 70, Th. 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)
::$N [see also \cite{RasiowaNonClassical} p. 70, Th. 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)
::$N [see also \cite{RasiowaNonClassical} p. 70, Th. 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)
::$N [see also \cite{RasiowaNonClassical} p. 70, Th. 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)
::$N [see also \cite{RasiowaNonClassical} p. 70, Th. 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)
::$N [see also \cite{RasiowaNonClassical} p. 70, Th. 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)
::$N [see also \cite{RasiowaNonClassical} p. 70, Th. 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)
::$N [see also \cite{RasiowaNonClassical} p. 70, Th. 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)
::$N [see also \cite{RasiowaNonClassical} p. 70, Th. 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)
::$N [see also \cite{RasiowaNonClassical} p. 70, Th. 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)
::$N [see also \cite{RasiowaNonClassical} p. 70, Th. 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)
::$N [see also \cite{RasiowaNonClassical} p. 70, Th. 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)
::$N [see also \cite{RasiowaNonClassical} p. 70, Th. 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)
::$N [see also \cite{RasiowaNonClassical} p. 70, Th. 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)
::$N [see also \cite{RasiowaNonClassical} p. 70, Th. 1.3 (37)]
theorem :: (2.38)
--a = a by ROBBINS3:def 6;
::NdR RasiowaNonClassical: p 70 1.3 (39)
::$N [see also \cite{RasiowaNonClassical} p. 70, Th. 1.3 (38)]
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)
::$N [see also \cite{RasiowaNonClassical} p. 70, Th. 1.3 (39)]
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)
::$N [see also \cite{RasiowaNonClassical} p. 70, Th. 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)
::$N [see also \cite{RasiowaNonClassical} p. 70, Th. 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)
::$N [see also \cite{RasiowaNonClassical} p. 70, Th. 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)
::$N [see also \cite{RasiowaNonClassical} p. 70, Th. 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;