:: Two Axiomatizations of {N}elson Algebras :: by Adam Grabowski :: :: Received April 19, 2015 :: Copyright (c) 2015-2018 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) 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;