:: On Fuzzy Negations Generated by Fuzzy Implications
:: by Adam Grabowski
::
:: Received February 26, 2020
:: Copyright (c) 2020-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, XXREAL_1, REAL_1, XXREAL_0, FUZIMPL1, SUBSET_1, CARD_1,
TARSKI, ARYTM_1, ARYTM_3, POWER, FUNCT_1, XBOOLE_0, RELAT_1, BINOP_1,
FUZIMPL2, ORDINAL2, WAYBEL29, VALUED_0, FUNCT_2, FUZIMPL3, MEMBERED,
PARTFUN1, ZFMISC_1, BORSUK_1, OPOSET_1, NAT_6;
notations TARSKI, XBOOLE_0, SUBSET_1, XCMPLX_0, XXREAL_0, NUMBERS, BINOP_1,
ZFMISC_1, VALUED_0, XREAL_0, RELAT_1, FUNCT_1, FUNCT_2, FUNCT_3,
STRUCT_0, RCOMP_1, PARTFUN1, MEMBERED, POWER, BORSUK_1, NAT_6,
FUZIMPL1, FUZIMPL2;
constructors SEQ_4, TOPMETR, PREPOWER, POWER, FUZIMPL1, FUZIMPL2, FUNCT_3,
NAT_6;
registrations XBOOLE_0, RELSET_1, XXREAL_0, XREAL_0, MEMBERED, ORDINAL1,
FUZNORM1, VALUED_0, NUMBERS, FUNCT_2, FOMODEL0, FUNCT_1, EULRPART,
RELAT_1, FUZIMPL2, BORSUK_1, FUZIMPL1, NAT_6;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
definitions TARSKI, VALUED_0, FUZIMPL2;
equalities XCMPLX_0;
expansions VALUED_0, FUZIMPL1;
theorems FUNCT_1, FUNCT_2, RELAT_1, POWER, XCMPLX_1, XREAL_1, XXREAL_0,
XXREAL_1, FUZNORM1, FUZIMPL1, VALUED_0, PARTFUN2, XBOOLE_0, ZFMISC_1,
BINOP_1, FUZIMPL2, FUNCT_3, NAT_6;
schemes FUZNORM1, BINOP_2, FUNCT_2, LMOD_7;
begin :: Preliminaries
theorem LemmaImp:
for x, r being Real st 0 <= x <= 1 & r > -1 holds
x * r + 1 > 0
proof
let x, r be Real;
assume
AA: 0 <= x <= 1 & r > -1;
per cases;
suppose r < 0; then
r <= r * x by XREAL_1:152,AA; then
-1 < r * x by XXREAL_0:2,AA; then
x * r + 1 > -1 + 1 by XREAL_1:8;
hence thesis;
end;
suppose r >= 0;
hence thesis by AA;
end;
end;
theorem Wazne1:
for z being Real st z in [.0,1.] & z <> 0 holds
ex w being Element of [.0,1.] st w < z
proof
let z be Real;
assume
A1: z in [.0,1.] & z <> 0;
reconsider w = 0 as Element of [.0,1.] by XXREAL_1:1;
take w;
thus thesis by A1,XXREAL_1:1;
end;
theorem Wazne2:
for z being Real st z in [.0,1.] & z <> 1 holds
ex w being Element of [.0,1.] st w > z
proof
let z be Real;
assume
A1: z in [.0,1.] & z <> 1;
reconsider w = 1 as Element of [.0,1.] by XXREAL_1:1;
take w;
1 >= z by A1,XXREAL_1:1;
hence thesis by A1,XXREAL_0:1;
end;
registration
cluster bijective increasing for UnOp of [.0,1.];
existence
proof
reconsider f = id [.0,1.] as UnOp of [.0,1.];
take f;
thus f is bijective;
thus f is increasing;
end;
end;
registration
cluster bijective non-decreasing -> increasing for UnOp of [.0,1.];
coherence;
cluster bijective increasing -> non-decreasing for UnOp of [.0,1.];
coherence;
end;
registration let f be bijective increasing UnOp of [.0,1.];
cluster f" -> real-valued Function-like;
coherence;
end;
registration let f be bijective increasing UnOp of [.0,1.];
cluster (f|[.0,1.])" -> real-valued;
coherence;
end;
RF220: ::: RFUNCT_2:20
for h being REAL-defined real-valued Function,
Y being set holds
h|Y is increasing iff for r1,r2 being Real
st r1 in Y /\ dom h & r2 in Y /\ dom h & r1 < r2 holds
h.r1 < h.r2
proof
let h be REAL-defined real-valued Function,
Y be set;
thus h|Y is increasing implies for r1,r2 being Real
st r1 in Y /\ dom h & r2 in Y /\ dom h & r1<r2 holds h.r2 > h.r1
proof
assume
A1: h|Y is increasing;
let r1,r2 be Real such that
A2: r1 in Y /\ dom h and
A3: r2 in Y /\ dom h and
A4: r1<r2;
A5: r2 in dom(h|Y) by A3,RELAT_1:61; then
A6: (h|Y).r2 = h.r2 by FUNCT_1:47;
A7: r1 in dom(h|Y) by A2,RELAT_1:61;
then (h|Y).r1 = h.r1 by FUNCT_1:47;
hence thesis by A1,A4,A7,A5,A6;
end;
assume
A8: for r1,r2 being Real
st r1 in Y /\ dom h & r2 in Y /\ dom h & r1<r2 holds h.r1 < h.r2;
let r1,r2 be ExtReal;
assume that
A9: r1 in dom(h|Y) & r2 in dom(h|Y) and
A10: r1<r2;
aa: dom (h|Y) c= REAL by RELAT_1:def 18;
A11: (h|Y).r1 = h.r1 & (h|Y).r2 = h.r2 by A9,FUNCT_1:47;
r1 in Y /\ dom h & r2 in Y /\ dom h by A9,RELAT_1:61;
hence thesis by A11,A8,A10,aa,A9;
end;
theorem
for f being one-to-one UnOp of [.0,1.],
d being Element of [.0,1.] st
d in rng f holds (f").d in dom f
proof
let f be one-to-one UnOp of [.0,1.],
d be Element of [.0,1.];
set X = [.0,1.];
reconsider fX = f|X as PartFunc of X, X;
assume
a1: d in rng f;
YZ: dom f = rng (f") by FUNCT_1:33;
reconsider dd = d as Element of REAL;
dom (f") = rng f by FUNCT_1:33;
hence thesis by YZ,FUNCT_1:3,a1;
end;
Cosik1:
for f being bijective UnOp of [.0,1.]
holds (f | [.0,1.])" is REAL-defined
proof
let f be bijective UnOp of [.0,1.];
dom (f") = rng f by FUNCT_1:33;
hence thesis by RELAT_1:def 18,RELAT_1:def 19;
end;
FC9: :: FCONT_3:9
for f being bijective increasing UnOp of [.0,1.]
holds ((f|[.0,1.])") | (f.:[.0,1.]) is increasing
proof
let f be bijective increasing UnOp of [.0,1.];
set X = [.0,1.];
assume that
A2: not (f|X)"|(f.:X) is increasing;
BB: (f|X)" is REAL-defined by Cosik1;
consider r1,r2 being Real such that
A3: r1 in f.:X /\ dom ((f|X)") and
A4: r2 in f.:X /\ dom((f|X)") and
A5: r1 < r2 and
A6: ((f|X)").r1 >= ((f|X)").r2 by A2,RF220,BB;
BB: rng (f|X) c= X by RELAT_1:def 19;
a1: rng f c= [.0,1.] by RELAT_1:def 19;
b2: dom f = rng (f") by FUNCT_1:33;
rng f = dom (f") by FUNCT_1:33; then
a5: dom ((f|X)") = [.0,1.] by FUNCT_2:def 1;
A7: f.:X = rng (f|X) by RELAT_1:115; then
A8: r1 in rng (f|X) by A3,XBOOLE_0:def 4;
A9: r2 in rng (f|X) by A4,A7,XBOOLE_0:def 4;
A10:f|X|X is increasing;
now
per cases;
suppose
((f|X)").r1 = ((f|X)").r2;
then r1 = (f|X).(((f|X)").r2) by A8,FUNCT_1:35
.= r2 by A9,FUNCT_1:35;
hence contradiction by A5;
end;
suppose
A11: ((f|X)").r1 <> ((f|X)").r2;
reconsider d = r2 as Element of [.0,1.] by BB,A9;
set c = (f|X)".d;
a4: rng ((f|X)") c= X by b2,RELAT_1:def 19;
c in rng ((f|X)") by a5,FUNCT_1:3; then
reconsider c as Element of [.0,1.] by a4;
F1: r2 in rng f & c = (f").r2 implies c in dom f by PARTFUN2:60;
reconsider rr1 = r1 as Element of [.0,1.] by A8,a1;
aa: rr1 in rng f implies (f").rr1 in dom f by PARTFUN2:60;
((f|X)").r2 < ((f|X)").r1 by A6,A11,XXREAL_0:1;
then (f|X).(((f|X)").r2) < (f|X).(((f|X)").r1)
by A10,aa,A4,A7,XBOOLE_0:def 4,F1,A3;
then r2 < (f|X).(((f|X)").r1) by A9,FUNCT_1:35;
hence contradiction by A5,A8,FUNCT_1:35;
end;
end;
hence contradiction;
end;
theorem LemmaIncreas:
for f being bijective increasing UnOp of [.0,1.] holds
f" is increasing
proof
set X = [.0,1.];
let f be bijective increasing UnOp of [.0,1.];
A2: (f|X)" | (f.:X) is increasing by FC9;
A3: dom f = X & rng f = X by FUNCT_2:def 1,def 3;
f.:X = X by RELAT_1:113,A3;
hence thesis by A2;
end;
registration let f be bijective increasing UnOp of [.0,1.];
cluster f" -> increasing;
coherence by LemmaIncreas;
end;
theorem Rosnie:
for f being UnOp of [.0,1.] holds
f is non-decreasing iff
for a,b being Element of [.0,1.] st a <= b holds f.a <= f.b
proof
let f be UnOp of [.0,1.];
dom f = [.0,1.] by FUNCT_2:def 1;
hence f is non-decreasing implies
for a,b being Element of [.0,1.] st a <= b holds f.a <= f.b;
assume
B1: for a,b being Element of [.0,1.] st a <= b holds f.a <= f.b;
let e1,e2 be ExtReal;
assume
B2: e1 in dom f & e2 in dom f & e1 <= e2; then
reconsider ee1 = e1, ee2 = e2 as Element of [.0,1.] by FUNCT_2:def 1;
ee1 <= ee2 by B2;
hence thesis by B1;
end;
theorem NonInc:
for f being UnOp of [.0,1.] holds
f is non-increasing iff
for a,b being Element of [.0,1.] st a <= b holds f.a >= f.b
proof
let f be UnOp of [.0,1.];
dom f = [.0,1.] by FUNCT_2:def 1;
hence f is non-increasing implies
for a,b being Element of [.0,1.] st a <= b holds f.a >= f.b;
assume
B1: for a,b being Element of [.0,1.] st a <= b holds f.a >= f.b;
let e1,e2 be ExtReal;
assume
B2: e1 in dom f & e2 in dom f & e1 <= e2; then
reconsider ee1 = e1, ee2 = e2 as Element of [.0,1.] by FUNCT_2:def 1;
ee1 <= ee2 by B2;
hence thesis by B1;
end;
theorem Decreas:
for f being UnOp of [.0,1.] holds
f is decreasing iff
for a,b being Element of [.0,1.] st a < b holds f.a > f.b
proof
let f be UnOp of [.0,1.];
dom f = [.0,1.] by FUNCT_2:def 1;
hence f is decreasing implies
for a,b being Element of [.0,1.] st a < b holds f.a > f.b;
assume
B1: for a,b being Element of [.0,1.] st a < b holds f.a > f.b;
let e1,e2 be ExtReal;
assume
B2: e1 in dom f & e2 in dom f & e1 < e2; then
reconsider ee1 = e1, ee2 = e2 as Element of [.0,1.] by FUNCT_2:def 1;
ee1 < ee2 by B2;
hence thesis by B1;
end;
theorem RosnieI:
for f being UnOp of [.0,1.] holds
f is increasing iff
for a,b being Element of [.0,1.] st a < b holds f.a < f.b
proof
let f be UnOp of [.0,1.];
dom f = [.0,1.] by FUNCT_2:def 1;
hence f is increasing implies
for a,b being Element of [.0,1.] st a < b holds f.a < f.b;
assume
B1: for a,b being Element of [.0,1.] st a < b holds f.a < f.b;
let e1,e2 be ExtReal;
assume
B2: e1 in dom f & e2 in dom f & e1 < e2; then
reconsider ee1 = e1, ee2 = e2 as Element of [.0,1.] by FUNCT_2:def 1;
ee1 < ee2 by B2;
hence thesis by B1;
end;
theorem LemmaBound:
for f being increasing bijective UnOp of [.0,1.] holds
f.0 = 0 & f.1 = 1
proof
let f be increasing bijective UnOp of [.0,1.];
KK: f.0 = 0
proof
set y = f.0;
set X = [.0,1.];
K1: 0 in [.0,1.] by XXREAL_1:1;
reconsider y as Element of [.0,1.] by XXREAL_1:1,FUNCT_2:5;
assume
H0: f.0 <> 0;
I3: rng f = X by FUNCT_2:def 3;
reconsider z = f".0 as Element of [.0,1.] by XXREAL_1:1,FUNCT_2:5;
L1: f.z = 0 by FUNCT_1:35,I3,K1; then
consider zz being Element of [.0,1.] such that
L2: zz < z by Wazne1,H0;
f.zz < f.z by L2,RosnieI;
hence contradiction by L1,XXREAL_1:1;
end;
f.1 = 1
proof
set X = [.0,1.];
K1: 1 in [.0,1.] by XXREAL_1:1;
reconsider y = f.1 as Element of [.0,1.] by XXREAL_1:1,FUNCT_2:5;
assume
H0: f.1 <> 1;
I3: rng f = X by FUNCT_2:def 3;
reconsider z = f".1 as Element of [.0,1.] by XXREAL_1:1,FUNCT_2:5;
L1: f.z = 1 by FUNCT_1:35,I3,K1; then
consider zz being Element of [.0,1.] such that
L2: zz > z by Wazne2,H0;
f.zz > f.z by L2,RosnieI;
hence contradiction by L1,XXREAL_1:1;
end;
hence thesis by KK;
end;
registration let f be bijective increasing UnOp of [.0,1.];
cluster f" -> bijective increasing for UnOp of [.0,1.];
coherence;
end;
begin :: Conjugate Fuzzy Implications
definition
func Theta -> set equals
the set of all f where f is bijective increasing UnOp of [.0,1.];
coherence;
end;
definition let f be BinOp of [.0,1.];
let h be bijective increasing UnOp of [.0,1.];
func ConjImpl (f,h) -> BinOp of [.0,1.] means :BIDef:
for x1,x2 being Element of [.0,1.] holds
it.(x1,x2) = h".(f.(h.x1, h.x2));
existence
proof
deffunc F(Real,Real) = h".(f.(h.$1, h.$2));
A1: for a,b being Element of [.0,1.] holds F(a,b) in [.0,1.]
proof
let a,b be Element of [.0,1.];
h".(f.(h.a, h.b)) in [.0,1.];
hence thesis;
end;
ex f being BinOp of [.0,1.] st
for a,b being Element of [.0,1.] holds
f.(a,b) = F(a,b) from FUZNORM1:sch 1(A1);
hence thesis;
end;
uniqueness
proof
deffunc F(Real,Real) = h".(f.(h.$1, h.$2));
reconsider A = [.0,1.] as non empty real-membered set;
for o1,o2 being BinOp of A st (for a,b being Element of A holds
o1.(a,b) = F(a,b)) &
(for a,b being Element of A holds o2.(a,b) = F(a,b)) holds o1 = o2
from BINOP_2:sch 2;
hence thesis;
end;
end;
definition let f,g be BinOp of [.0,1.];
pred f,g are_conjugate means
ex h being bijective increasing UnOp of [.0,1.] st
g = ConjImpl (f,h);
end;
registration
let I be Fuzzy_Implication,
f be bijective non-decreasing UnOp of [.0,1.];
cluster ConjImpl (I,f) -> decreasing_on_1st increasing_on_2nd
00-dominant 11-dominant 10-weak;
coherence
proof
set g = ConjImpl (I,f);
set X = [.0,1.];
V1: for x1,x2,y being Element of [.0,1.] st
x1 <= x2 holds g.(x1,y) >= g.(x2,y)
proof
let x1,x2,y be Element of [.0,1.];
set h = (f|X)"|(f.:X);
U1: X = dom f by FUNCT_2:def 1;
rng f = X by FUNCT_2:def 3; then
Z8: h = (f")|X by U1,RELAT_1:113;
reconsider h as UnOp of [.0,1.] by Z8;
a0: dom f = [.0,1.] by FUNCT_2:def 1;
assume x1 <= x2; then
B1: f.x1 <= f.x2 by a0,VALUED_0:def 15;
A1: g.(x1,y) = f".(I.(f.x1, f.y)) by BIDef;
T1: g.(x2,y) = f".(I.(f.x2, f.y)) by BIDef;
I.(f.x1, f.y) >= I.(f.x2, f.y) by B1,FUZIMPL1:def 1;
hence thesis by A1,T1,Rosnie;
end;
v2: for x,y1,y2 being Element of [.0,1.] st
y1 <= y2 holds g.(x,y1) <= g.(x,y2)
proof
let x,y1,y2 be Element of [.0,1.];
assume
WW: y1 <= y2;
reconsider h = f" as UnOp of [.0,1.];
dom f = [.0,1.] by FUNCT_2:def 1; then
B1: f.y1 <= f.y2 by WW,VALUED_0:def 15;
A1: g.(x,y2) = f".(I.(f.x, f.y2)) by BIDef;
T1: g.(x,y1) = f".(I.(f.x, f.y1)) by BIDef;
I.(f.x, f.y1) <= I.(f.x, f.y2) by B1,FUZIMPL1:def 2;
hence thesis by A1,T1,Rosnie;
end;
reconsider x1 = 0, x2 = 1 as Element of [.0,1.] by XXREAL_1:1;
H2: f.0 = 0 by LemmaBound;
H3: f.1 = 1 by LemmaBound;
H5: f".0 = 0 by LemmaBound;
v3: g.(x1,x1) = f".(I.(f.x1, f.x1)) by BIDef
.= f".1 by FUZIMPL1:def 3,H2
.= 1 by LemmaBound;
v4: g.(x2,x2) = f".(I.(f.x2, f.x2)) by BIDef
.= f".1 by FUZIMPL1:def 4,H3
.= 1 by LemmaBound;
g.(x2,x1) = f".(I.(f.x2, f.x1)) by BIDef
.= 0 by H5,FUZIMPL1:def 5,H2,H3;
hence thesis by V1,v2,v3,v4;
end;
end;
theorem ::: Proposition 1.1.8 p. 6
for I being Fuzzy_Implication,
f being bijective increasing UnOp of [.0,1.] holds
ConjImpl (I,f) is Fuzzy_Implication;
registration
cluster satisfying_(NP) satisfying_(OP) satisfying_(EP) satisfying_(IP)
for Fuzzy_Implication;
existence
proof
take I_LK;
thus thesis;
end;
end;
theorem Prop136a: :: Proposition 1.3.6 a) p. 13
for I being Fuzzy_Implication,
f being bijective increasing UnOp of [.0,1.] st
I is satisfying_(NP) holds
ConjImpl (I,f) is satisfying_(NP)
proof
let I be Fuzzy_Implication,
f be bijective increasing UnOp of [.0,1.];
assume
B0: I is satisfying_(NP);
set g = ConjImpl (I,f);
A0: 1 in [.0,1.] by XXREAL_1:1;
let y be Element of [.0,1.];
g.(1,y) = f".(I.(f.1, f.y)) by A0,BIDef
.= f".(I.(1,f.y)) by LemmaBound
.= f".(f.y) by B0,FUZIMPL2:def 1;
hence thesis by FUNCT_2:26;
end;
theorem Prop136b: :: Proposition 1.3.6 b) p. 13
for I being Fuzzy_Implication,
f being bijective increasing UnOp of [.0,1.] st
I is satisfying_(EP) holds
ConjImpl (I,f) is satisfying_(EP)
proof
let I be Fuzzy_Implication,
f be bijective increasing UnOp of [.0,1.];
assume
B0: I is satisfying_(EP);
set g = ConjImpl (I,f);
let x,y,z be Element of [.0,1.];
I.(f.y,f.z) in [.0,1.]; then
BB: I.(f.y,f.z) in rng f by FUNCT_2:def 3;
I.(f.x,f.z) in [.0,1.]; then
B2: I.(f.x,f.z) in rng f by FUNCT_2:def 3;
g.(x,g.(y,z)) = g.(x,f".(I.(f.y, f.z))) by BIDef
.= f".(I.(f.x,f.(f".(I.(f.y, f.z))))) by BIDef
.= f".(I.(f.x,I.(f.y, f.z))) by FUNCT_1:35,BB
.= f".(I.(f.y,I.(f.x, f.z))) by B0,FUZIMPL2:def 2
.= f".(I.(f.y,f.(f".(I.(f.x, f.z))))) by B2,FUNCT_1:35
.= g.(y,f".(I.(f.x, f.z))) by BIDef
.= g.(y,g.(x,z)) by BIDef;
hence thesis;
end;
theorem Prop136c: :: Proposition 1.3.6 c) p. 13
for I being Fuzzy_Implication,
f being bijective increasing UnOp of [.0,1.] st
I is satisfying_(IP) holds
ConjImpl (I,f) is satisfying_(IP)
proof
let I be Fuzzy_Implication,
f be bijective increasing UnOp of [.0,1.];
assume
B0: I is satisfying_(IP);
set g = ConjImpl (I,f);
let x be Element of [.0,1.];
g.(x,x) = f".(I.(f.x,f.x)) by BIDef
.= f".1 by FUZIMPL2:def 3,B0
.= 1 by LemmaBound;
hence thesis;
end;
theorem Prop136d: :: Proposition 1.3.6 d) p. 13
for I being Fuzzy_Implication,
f being bijective increasing UnOp of [.0,1.] st
I is satisfying_(OP) holds
ConjImpl (I,f) is satisfying_(OP)
proof
let I be Fuzzy_Implication,
f be bijective increasing UnOp of [.0,1.];
assume
B0: I is satisfying_(OP);
set g = ConjImpl (I,f);
let x,y be Element of [.0,1.];
b3: rng f = [.0,1.] by FUNCT_2:def 3;
b4: dom f = [.0,1.] by FUNCT_2:def 1;
thus g.(x,y) = 1 implies x <= y
proof
assume g.(x,y) = 1; then
f".(I.(f.x,f.y)) = 1 by BIDef; then
f.(f".(I.(f.x,f.y))) = 1 by LemmaBound; then
I.(f.x,f.y) = 1 by FUNCT_1:35,b3; then
f.x <= f.y by FUZIMPL2:def 4,B0; then
f".(f.x) <= f".(f.y) by Rosnie; then
x <= f".(f.y) by b4,FUNCT_1:34;
hence thesis by b4,FUNCT_1:34;
end;
assume x <= y; then
f.x <= f.y by Rosnie; then
I.(f.x, f.y) = 1 by FUZIMPL2:def 4,B0; then
f".(I.(f.x,f.y)) = 1 by LemmaBound;
hence thesis by BIDef;
end;
registration
let I be satisfying_(NP) Fuzzy_Implication,
f be bijective increasing UnOp of [.0,1.];
cluster ConjImpl (I,f) -> satisfying_(NP);
coherence by Prop136a;
end;
registration
let I be satisfying_(EP) Fuzzy_Implication,
f be bijective increasing UnOp of [.0,1.];
cluster ConjImpl (I,f) -> satisfying_(EP);
coherence by Prop136b;
end;
registration
let I be satisfying_(IP) Fuzzy_Implication,
f be bijective increasing UnOp of [.0,1.];
cluster ConjImpl (I,f) -> satisfying_(IP);
coherence by Prop136c;
end;
registration
let I be satisfying_(OP) Fuzzy_Implication,
f be bijective increasing UnOp of [.0,1.];
cluster ConjImpl (I,f) -> satisfying_(OP);
coherence by Prop136d;
end;
theorem
for I being Fuzzy_Implication,
f being bijective increasing UnOp of [.0,1.] holds
ConjImpl (I,f) = f" * I * [:f,f:]
proof
let I be Fuzzy_Implication,
f be bijective increasing UnOp of [.0,1.];
set g = ConjImpl (I,f);
dom g = [:[.0,1.],[.0,1.]:] by FUNCT_2:def 1; then
A1: dom g = dom (f" * I * [:f,f:]) by FUNCT_2:def 1;
C2: dom f = [.0,1.] by FUNCT_2:def 1;
for x being object st x in dom g holds
g.x = (f" * I * [:f,f:]).x
proof
let x be object;
assume x in dom g; then
W1: x in [:[.0,1.],[.0,1.]:] by FUNCT_2:def 1; then
consider x1, x2 being object such that
C0: x1 in [.0,1.] & x2 in [.0,1.] & x = [x1,x2] by ZFMISC_1:def 2;
reconsider x1, x2 as Element of [.0,1.] by C0;
D1: x in dom [:f,f:] by W1,FUNCT_2:def 1;
X2: dom I = [:[.0,1.],[.0,1.]:] by FUNCT_2:def 1;
[f.x1,f.x2] in [:[.0,1.],[.0,1.]:] by ZFMISC_1:87; then
[:f,f:].(x1,x2) in dom I by X2; then
D2: [:f,f:].x in dom I by C0,BINOP_1:def 1;
g.x = g.(x1,x2) by C0,BINOP_1:def 1
.= f".(I.(f.x1, f.x2)) by BIDef
.= f".(I. [f.x1, f.x2]) by BINOP_1:def 1
.= f". (I.([:f,f:].(x1,x2))) by C2,FUNCT_3:def 8
.= f". (I.([:f,f:].x)) by C0,BINOP_1:def 1
.= (f" * I).(([:f,f:]).x) by FUNCT_1:13,D2
.= (f" * I * [:f,f:]).x by FUNCT_1:13,D1;
hence thesis;
end;
hence thesis by A1,FUNCT_1:2;
end;
begin :: Fuzzy Negations
definition let N be UnOp of [.0,1.];
attr N is satisfying_(N1) means :N1Def:
N.0 = 1 & N.1 = 0;
attr N is satisfying_(N2) means :N2Def:
N is non-increasing;
end;
definition
func N_CC -> UnOp of [.0,1.] means :NDef:
for x being Element of [.0,1.] holds
it.x = 1 - x;
existence
proof
deffunc F(Real) = 1 - $1;
A1: for a being Element of [.0,1.] holds F(a) in [.0,1.] by FUZNORM1:7;
ex f being UnOp of [.0,1.] st
for a being Element of [.0,1.] holds
f.a = F(a) from FUNCT_2:sch 8(A1);
hence thesis;
end;
uniqueness
proof
deffunc F(Real) = 1 - $1;
reconsider A = [.0,1.] as non empty real-membered set;
for o1,o2 being UnOp of A st
(for a being Element of A holds o1.a = F(a)) &
(for a being Element of A holds o2.a = F(a)) holds o1 = o2
from LMOD_7:sch 2;
hence thesis;
end;
end;
registration
cluster N_CC -> satisfying_(N1) satisfying_(N2);
coherence
proof
set g = N_CC;
T0: 0 in [.0,1.] & 1 in [.0,1.] by XXREAL_1:1; then
T1: g.0 = 1 - 0 by NDef
.= 1;
a1: g.1 = 1 - 1 by T0,NDef
.= 0;
for a,b being Element of [.0,1.] st a <= b holds
g.a >= g.b
proof
let a,b be Element of [.0,1.];
assume
Y0: a <= b;
g.a = 1 - a & g.b = 1 - b by NDef;
hence thesis by Y0,XREAL_1:13;
end;
hence thesis by a1,NonInc,T1;
end;
end;
registration
cluster N_CC -> bijective decreasing;
coherence
proof
set f = N_CC;
B1: [.0,1.] c= rng f
proof
let x be object;
assume x in [.0,1.]; then
reconsider xx = x as Element of [.0,1.];
set y = 1 - xx;
B3: 1 - xx in [.0,1.] by FUZNORM1:7; then
B2: y in dom f by FUNCT_2:def 1;
f.y = 1 - y by NDef,B3
.= xx;
hence thesis by B2,FUNCT_1:def 3;
end;
a0: rng f c= [.0,1.] by RELAT_1:def 19;
for x1,x2 being object st x1 in dom f & x2 in dom f & f.x1 = f.x2
holds x1 = x2
proof
let x1,x2 be object;
assume
A1: x1 in dom f & x2 in dom f & f.x1 = f.x2; then
reconsider xx1 = x1, xx2 = x2 as Element of [.0,1.] by FUNCT_2:def 1;
f.xx1 = 1 - xx1 & f.xx2 = 1 - xx2 by NDef; then
1 - xx1 = 1 - xx2 by A1;
hence thesis;
end; then
f is one-to-one onto by a0,FUNCT_1:def 4,FUNCT_2:def 3,B1,XBOOLE_0:def 10;
hence f is bijective;
for a,b being Element of [.0,1.] st a < b holds f.a > f.b
proof
let a,b be Element of [.0,1.];
assume
S0: a < b;
S1: f.a = 1 - a & f.b = 1 - b by NDef;
-a > -b by S0,XREAL_1:24;
hence thesis by S1,XREAL_1:6;
end;
hence f is decreasing by Decreas;
end;
end;
registration
cluster bijective decreasing for UnOp of [.0,1.];
existence
proof
take f = N_CC;
thus thesis;
end;
end;
registration
cluster satisfying_(N1) satisfying_(N2) for UnOp of [.0,1.];
existence
proof
take N_CC;
thus thesis;
end;
end;
definition
mode Fuzzy_Negation is satisfying_(N1) satisfying_(N2) UnOp of [.0,1.];
end;
definition let f be UnOp of [.0,1.];
attr f is continuous means
ex g being Function of I[01], I[01] st f = g &
g is continuous;
end;
definition let N be UnOp of [.0,1.];
attr N is involutive means
for x being Element of [.0,1.] holds
N.(N.x) = x;
end;
definition let N be UnOp of [.0,1.];
attr N is satisfying_(N3) means
N is decreasing;
attr N is satisfying_(N4) means
N is continuous;
attr N is satisfying_(N5) means
N is involutive;
end;
definition let N be UnOp of [.0,1.];
attr N is negation-strict means
N is satisfying_(N3) satisfying_(N4);
end;
definition let N be UnOp of [.0,1.];
attr N is negation-strong means
N is satisfying_(N5);
attr N is non-vanishing means
for x being Element of [.0,1.] holds
N.x = 0 iff x = 1;
attr N is non-filling means
for x being Element of [.0,1.] holds
N.x = 1 iff x = 0;
end;
begin :: Generating Fuzzy Negations from Fuzzy Implications
theorem
for f being decreasing bijective UnOp of [.0,1.] holds
f.0 = 1 & f.1 = 0
proof
let f be decreasing bijective UnOp of [.0,1.];
KK: f.0 = 1
proof
set y = f.0;
set X = [.0,1.];
K1: 1 in [.0,1.] by XXREAL_1:1;
reconsider y as Element of [.0,1.] by XXREAL_1:1,FUNCT_2:5;
assume
H0: f.0 <> 1;
I3: rng f = X by FUNCT_2:def 3;
reconsider z = f".1 as Element of [.0,1.] by XXREAL_1:1,FUNCT_2:5;
L1: f.z = 1 by FUNCT_1:35,I3,K1; then
consider zz being Element of [.0,1.] such that
L2: zz < z by Wazne1,H0;
f.zz > f.z by L2,Decreas;
hence contradiction by L1,XXREAL_1:1;
end;
f.1 = 0
proof
set X = [.0,1.];
K1: 0 in [.0,1.] by XXREAL_1:1;
reconsider y = f.1 as Element of [.0,1.] by XXREAL_1:1,FUNCT_2:5;
assume
H0: f.1 <> 0;
I3: rng f = X by FUNCT_2:def 3;
reconsider z = f".0 as Element of [.0,1.] by XXREAL_1:1,FUNCT_2:5;
L1: f.z = 0 by FUNCT_1:35,I3,K1; then
consider zz being Element of [.0,1.] such that
L2: zz > z by Wazne2,H0;
f.zz < f.z by L2,Decreas;
hence contradiction by L1,XXREAL_1:1;
end;
hence thesis by KK;
end;
definition let I be BinOp of [.0,1.];
func FNegation I -> UnOp of [.0,1.] means :FNeg:
for x being Element of [.0,1.] holds
it.x = I.(x,0);
existence
proof
deffunc F(Real) = I.($1,0);
A1: for a being Element of [.0,1.] holds F(a) in [.0,1.] by FUZNORM1:15;
ex f being UnOp of [.0,1.] st
for a being Element of [.0,1.] holds
f.a = F(a) from FUNCT_2:sch 8(A1);
hence thesis;
end;
uniqueness
proof
deffunc F(Real) = I.($1,0);
reconsider A = [.0,1.] as non empty real-membered set;
for o1,o2 being UnOp of A st
(for a being Element of A holds o1.a = F(a)) &
(for a being Element of A holds o2.a = F(a)) holds o1 = o2
from LMOD_7:sch 2;
hence thesis;
end;
end;
:: Lemma 1.4.14
registration let I be satisfying_(I1) satisfying_(I3) satisfying_(I5)
BinOp of [.0,1.];
cluster FNegation I -> satisfying_(N1) satisfying_(N2);
coherence
proof
set g = FNegation I;
T0: 0 in [.0,1.] & 1 in [.0,1.] by XXREAL_1:1; then
T1: g.0 = I.(0,0) by FNeg
.= 1 by FUZIMPL1:def 3;
a1: g.1 = I.(1,0) by T0,FNeg
.= 0 by FUZIMPL1:def 5;
for a,b being Element of [.0,1.] st a <= b holds
g.a >= g.b
proof
let a,b be Element of [.0,1.];
assume
Y0: a <= b;
g.a = I.(a,0) & g.b = I.(b,0) by FNeg;
hence thesis by Y0,T0,FUZIMPL1:def 1;
end;
hence thesis by a1,T1,NonInc;
end;
end;
:: Definition 1.4.15
theorem ::: natural negation generated by I
for I being Fuzzy_Implication holds
FNegation I is Fuzzy_Negation;
begin :: Boundary Fuzzy Negations
definition
func NegationD1 -> UnOp of [.0,1.] means :D1Def:
for x being Element of [.0,1.] holds
(x = 0 implies it.x = 1) &
(x <> 0 implies it.x = 0);
existence
proof
defpred C[object] means $1 = 0;
deffunc F(object) = 1;
deffunc G(object) = 0;
A1: for x being object st x in [.0,1.] holds
(C[x] implies F(x) in [.0,1.]) &
(not C[x] implies G(x) in [.0,1.]) by XXREAL_1:1;
ex f being Function of [.0,1.],[.0,1.] st
for x being object st x in [.0,1.] holds
(C[x] implies f.x = F(x)) &
(not C[x] implies f.x = G(x)) from FUNCT_2:sch 5(A1); then
consider f being Function of [.0,1.],[.0,1.] such that
B1: for x being object st x in [.0,1.] holds
(C[x] implies f.x = F(x)) & (not C[x] implies f.x = G(x));
take f;
let x be Element of [.0,1.];
thus x = 0 implies f.x = 1 by B1;
assume x <> 0;
hence thesis by B1;
end;
uniqueness
proof
let f1, f2 be UnOp of [.0,1.] such that
A1: for x being Element of [.0,1.] holds
(x = 0 implies f1.x = 1) &
(x <> 0 implies f1.x = 0) and
A2: for x being Element of [.0,1.] holds
(x = 0 implies f2.x = 1) &
(x <> 0 implies f2.x = 0);
for x being Element of [.0,1.] holds f1.x = f2.x
proof
let x be Element of [.0,1.];
per cases;
suppose
D1: x = 0;
hence f1.x = 1 by A1 .= f2.x by D1,A2;
end;
suppose
D1: x <> 0;
hence f1.x = 0 by A1 .= f2.x by D1,A2;
end;
end;
hence thesis by FUNCT_2:63;
end;
func NegationD2 -> UnOp of [.0,1.] means :D2Def:
for x being Element of [.0,1.] holds
(x = 1 implies it.x = 0) &
(x <> 1 implies it.x = 1);
existence
proof
defpred C[object] means $1 = 1;
deffunc F(object) = 0;
deffunc G(object) = 1;
A1: for x being object st x in [.0,1.] holds
(C[x] implies F(x) in [.0,1.]) &
(not C[x] implies G(x) in [.0,1.]) by XXREAL_1:1;
ex f being Function of [.0,1.],[.0,1.] st
for x being object st x in [.0,1.] holds
(C[x] implies f.x = F(x)) &
(not C[x] implies f.x = G(x)) from FUNCT_2:sch 5(A1); then
consider f being Function of [.0,1.],[.0,1.] such that
B1: for x being object st x in [.0,1.] holds
(C[x] implies f.x = F(x)) & (not C[x] implies f.x = G(x));
take f;
let x be Element of [.0,1.];
thus x = 1 implies f.x = 0 by B1;
assume x <> 1;
hence thesis by B1;
end;
uniqueness
proof
let f1, f2 be UnOp of [.0,1.] such that
A1: for x being Element of [.0,1.] holds
(x = 1 implies f1.x = 0) &
(x <> 1 implies f1.x = 1) and
A2: for x being Element of [.0,1.] holds
(x = 1 implies f2.x = 0) &
(x <> 1 implies f2.x = 1);
for x being Element of [.0,1.] holds f1.x = f2.x
proof
let x be Element of [.0,1.];
per cases;
suppose
D1: x = 1;
hence f1.x = 0 by A1 .= f2.x by D1,A2;
end;
suppose
D1: x <> 1;
hence f1.x = 1 by A1 .= f2.x by D1,A2;
end;
end;
hence thesis by FUNCT_2:63;
end;
end;
:: The Ordering of Fuzzy Negations
definition let f1, f2 be UnOp of [.0,1.];
pred f1 <= f2 means
for a being Element of [.0,1.] holds
f1.a <= f2.a;
end;
registration
cluster NegationD1 -> satisfying_(N1) satisfying_(N2);
coherence
proof
set f = NegationD1;
0 in [.0,1.] & 1 in [.0,1.] by XXREAL_1:1;
hence f is satisfying_(N1) by D1Def;
for x,y being Element of [.0,1.] st x <= y holds f.x >= f.y
proof
let x,y be Element of [.0,1.];
assume
B2: x <= y;
per cases;
suppose x = 0; then
f.x = 1 by D1Def;
hence thesis by XXREAL_1:1;
end;
suppose
B1: x <> 0; then
B3: f.x = 0 by D1Def;
x > 0 by B1,XXREAL_1:1;
hence thesis by B3,D1Def,B2;
end;
end;
hence thesis by NonInc;
end;
cluster NegationD2 -> satisfying_(N1) satisfying_(N2);
coherence
proof
set f = NegationD2;
0 in [.0,1.] & 1 in [.0,1.] by XXREAL_1:1;
hence f is satisfying_(N1) by D2Def;
for x,y being Element of [.0,1.] st x <= y holds f.x >= f.y
proof
let x,y be Element of [.0,1.];
assume
B2: x <= y;
per cases;
suppose y = 1; then
f.y = 0 by D2Def;
hence thesis by XXREAL_1:1;
end;
suppose
B1: y <> 1; then
B3: f.y = 1 by D2Def;
y <= 1 by XXREAL_1:1; then
y < 1 by B1,XXREAL_0:1;
hence thesis by B3,D2Def,B2;
end;
end;
hence thesis by NonInc;
end;
end;
theorem
for N being Fuzzy_Negation holds
NegationD1 <= N <= NegationD2
proof
set f = NegationD1;
set g = NegationD2;
let N be Fuzzy_Negation;
thus f <= N
proof
let x be Element of [.0,1.];
per cases;
suppose
A1: x = 0; then
f.x = 1 by D1Def;
hence thesis by A1,N1Def;
end;
suppose x <> 0; then
f.x = 0 by D1Def;
hence thesis by XXREAL_1:1;
end;
end;
let x be Element of [.0,1.];
per cases;
suppose
A1: x = 1; then
N.x = 0 by N1Def;
hence thesis by A1,D2Def;
end;
suppose x <> 1; then
g.x = 1 by D2Def;
hence thesis by XXREAL_1:1;
end;
end;
begin :: Table 1.7:
:: On Fuzzy Negations Generated by Fuzzy Implications
theorem
FNegation I_LK = N_CC
proof
set I = I_LK;
set f = FNegation I;
set g = N_CC;
A1: 0 in [.0,1.] by XXREAL_1:1;
for x being Element of [.0,1.] holds f.x = g.x
proof
let x be Element of [.0,1.];
1 - x in [.0,1.] by FUZNORM1:7; then
A2: 1 - x <= 1 by XXREAL_1:1;
f.x = I.(x,0) by FNeg
.= min (1,1-x+0) by A1,FUZIMPL1:def 14
.= 1 - x by A2,XXREAL_0:def 9
.= g.x by NDef;
hence thesis;
end;
hence thesis by FUNCT_2:63;
end;
theorem
FNegation I_GD = NegationD1
proof
set I = I_GD;
set f = FNegation I;
set g = NegationD1;
A1: 0 in [.0,1.] by XXREAL_1:1;
for x being Element of [.0,1.] holds f.x = g.x
proof
let x be Element of [.0,1.];
per cases;
suppose
B1: x <= 0; then
B2: x = 0 by XXREAL_1:1;
f.x = I.(x,0) by FNeg
.= 1 by FUZIMPL1:def 16,B1,A1
.= g.x by D1Def,B2;
hence thesis;
end;
suppose
B1: x > 0;
f.x = I.(x,0) by FNeg
.= 0 by A1,B1,FUZIMPL1:def 16
.= g.x by D1Def,B1;
hence thesis;
end;
end;
hence thesis by FUNCT_2:63;
end;
theorem
FNegation I_RC = N_CC
proof
set I = I_RC;
set f = FNegation I;
set g = N_CC;
A1: 0 in [.0,1.] by XXREAL_1:1;
for x being Element of [.0,1.] holds f.x = g.x
proof
let x be Element of [.0,1.];
f.x = I.(x,0) by FNeg
.= 1 - x + x * 0 by FUZIMPL1:def 17,A1
.= g.x by NDef;
hence thesis;
end;
hence thesis by FUNCT_2:63;
end;
theorem
FNegation I_KD = N_CC
proof
set I = I_KD;
set f = FNegation I;
set g = N_CC;
A1: 0 in [.0,1.] by XXREAL_1:1;
for x being Element of [.0,1.] holds f.x = g.x
proof
let x be Element of [.0,1.];
1 - x in [.0,1.] by FUZNORM1:7; then
A2: 1 - x >= 0 by XXREAL_1:1;
f.x = I.(x,0) by FNeg
.= max (1 - x, 0) by FUZIMPL1:def 18,A1
.= 1 - x by A2,XXREAL_0:def 10
.= g.x by NDef;
hence thesis;
end;
hence thesis by FUNCT_2:63;
end;
theorem
FNegation I_GG = NegationD1
proof
set I = I_GG;
set f = FNegation I;
set g = NegationD1;
A1: 0 in [.0,1.] by XXREAL_1:1;
for x being Element of [.0,1.] holds f.x = g.x
proof
let x be Element of [.0,1.];
per cases;
suppose
B1: x <= 0; then
B2: x = 0 by XXREAL_1:1;
f.x = I.(x,0) by FNeg
.= 1 by FUZIMPL1:def 19,B1,A1
.= g.x by D1Def,B2;
hence thesis;
end;
suppose
B1: x > 0;
f.x = I.(x,0) by FNeg
.= 0 / x by A1,B1,FUZIMPL1:def 19
.= g.x by D1Def,B1;
hence thesis;
end;
end;
hence thesis by FUNCT_2:63;
end;
theorem
FNegation I_RS = NegationD1
proof
set I = I_RS;
set f = FNegation I;
set g = NegationD1;
A1: 0 in [.0,1.] by XXREAL_1:1;
for x being Element of [.0,1.] holds f.x = g.x
proof
let x be Element of [.0,1.];
per cases;
suppose
B1: x <= 0; then
B2: x = 0 by XXREAL_1:1;
f.x = I.(x,0) by FNeg
.= 1 by FUZIMPL1:def 20,B1,A1
.= g.x by D1Def,B2;
hence thesis;
end;
suppose
B1: x > 0;
f.x = I.(x,0) by FNeg
.= 0 by A1,B1,FUZIMPL1:def 20
.= g.x by D1Def,B1;
hence thesis;
end;
end;
hence thesis by FUNCT_2:63;
end;
theorem
FNegation I_YG = NegationD1
proof
set I = I_YG;
set f = FNegation I;
set g = NegationD1;
A1: 0 in [.0,1.] by XXREAL_1:1;
for x being Element of [.0,1.] holds f.x = g.x
proof
let x be Element of [.0,1.];
per cases;
suppose
x <= 0; then
B2: x = 0 by XXREAL_1:1;
f.x = I.(x,0) by FNeg
.= 1 by FUZIMPL1:def 21,B2
.= g.x by D1Def,B2;
hence thesis;
end;
suppose
B1: x > 0;
f.x = I.(x,0) by FNeg
.= 0 to_power x by A1,B1,FUZIMPL1:def 21
.= 0 by B1,POWER:def 2
.= g.x by D1Def,B1;
hence thesis;
end;
end;
hence thesis by FUNCT_2:63;
end;
theorem
FNegation I_WB = NegationD2
proof
set I = I_WB;
set f = FNegation I;
set g = NegationD2;
A1: 0 in [.0,1.] by XXREAL_1:1;
for x being Element of [.0,1.] holds f.x = g.x
proof
let x be Element of [.0,1.];
x <= 1 by XXREAL_1:1; then
per cases by XXREAL_0:1;
suppose
B1: x < 1;
f.x = I.(x,0) by FNeg
.= 1 by FUZIMPL1:def 22,B1,A1
.= g.x by D2Def,B1;
hence thesis;
end;
suppose
B1: x = 1;
f.x = I.(x,0) by FNeg
.= 0 by A1,B1,FUZIMPL1:def 22
.= g.x by D2Def,B1;
hence thesis;
end;
end;
hence thesis by FUNCT_2:63;
end;
theorem
FNegation I_FD = N_CC
proof
set I = I_FD;
set f = FNegation I;
set g = N_CC;
A1: 0 in [.0,1.] by XXREAL_1:1;
for x being Element of [.0,1.] holds f.x = g.x
proof
let x be Element of [.0,1.];
1 - x in [.0,1.] by FUZNORM1:7; then
A2: 1 - x >= 0 by XXREAL_1:1;
per cases;
suppose
x <= 0; then
B2: x = 0 by XXREAL_1:1;
f.x = I.(x,0) by FNeg
.= 1 - x by FUZIMPL1:def 23,B2
.= g.x by NDef;
hence thesis;
end;
suppose
B1: x > 0;
f.x = I.(x,0) by FNeg
.= max (1 - x, 0) by A1,B1,FUZIMPL1:def 23
.= 1 - x by XXREAL_0:def 10,A2
.= g.x by NDef;
hence thesis;
end;
end;
hence thesis by FUNCT_2:63;
end;
theorem :: Proposition 1.4.17 i)
for I being satisfying_(EP) satisfying_(OP) BinOp of [.0,1.] holds
FNegation I is Fuzzy_Negation;
theorem Prop1417ii: :: Proposition 1.4.17 ii)
for I being satisfying_(EP) satisfying_(OP) BinOp of [.0,1.]
for x being Element of [.0,1.] holds
x <= (FNegation I).((FNegation I).x)
proof
let I be satisfying_(EP) satisfying_(OP) BinOp of [.0,1.];
let x be Element of [.0,1.];
set f = FNegation I;
A1: 0 in [.0,1.] by XXREAL_1:1;
f.x in [.0,1.]; then
A2: I.(x,0) in [.0,1.] by FNeg; then
a7: I.(x,(I.(I.(x,0),0))) = I.(I.(x,0),I.(x,0)) by A1,FUZIMPL2:def 2
.= 1 by A2,FUZIMPL2:def 3;
I.(I.(x,0),0) = I.(f.x,0) by FNeg
.= f.(f.x) by FNeg;
hence thesis by a7,FUZIMPL2:def 4;
end;
theorem :: Proposition 1.4.17 iii)
for I being satisfying_(EP) satisfying_(OP) BinOp of [.0,1.] holds
(FNegation I) * (FNegation I) * (FNegation I) = FNegation I
proof
let I be satisfying_(EP) satisfying_(OP) BinOp of [.0,1.];
set f = FNegation I;
now let x be Element of [.0,1.];
f is non-increasing by N2Def; then
R2: f.(f.(f.x)) <= f.x by NonInc,Prop1417ii;
v1: f.x = I.(x,0) by FNeg;
v2: I.(I.(I.(x,0),0),0) = I.(I.(f.x,0),0) by FNeg
.= I.(f.(f.x),0) by FNeg
.= f.(f.(f.x)) by FNeg;
vz: f.(f.x) = I.(I.(x,0),0) by FNeg,v1;
r1: dom (f * f) = [.0,1.] by FUNCT_2:def 1;
0 in [.0,1.] by XXREAL_1:1; then
I.(I.(x,0),I.(I.(I.(x,0),0),0)) = I.(I.(I.(x,0),0),I.(I.(x,0),0))
by FUZIMPL2:def 2,vz,v1
.= 1 by vz,FUZIMPL2:def 3; then
f.x <= I.(I.(f.x,0),0) by v1,v2,FUZIMPL2:def 4; then
f.x <= I.(f.(f.x),0) by FNeg; then
f.x <= f.(f.(f.x)) by FNeg; then
f.x = f.(f.(f.x)) by R2,XXREAL_0:1; then
f.x = f.((f * f).x) by r1,FUNCT_1:12
.= (f * (f * f)).x by FUNCT_1:13,r1;
hence (f * f * f).x = f.x by RELAT_1:36;
end;
hence thesis by FUNCT_2:63;
end;
begin :: Sugeno Negation
definition
::$CD
let l be Real;
assume
A0: l > -1;
func SugenoNegation l -> UnOp of [.0,1.] means :DefSugeno:
for x being Element of [.0,1.] holds
it.x = (1 - x) / (1 + l * x);
existence
proof
deffunc F(Real) = (1 - $1) / (1 + l * $1);
A1: for a being Element of [.0,1.] holds F(a) in [.0,1.]
proof
let a be Element of [.0,1.];
1 - a in [.0,1.] by FUZNORM1:7; then
B2: 1 - a >= 0 by XXREAL_1:1;
B3: a >= 0 by XXREAL_1:1; then
l * a >= (-1) * a by A0,XREAL_1:64; then
b1: 1 + l * a >= 1 - 1 * a by XREAL_1:6;
(-1) * a <= l * a by A0,B3,XREAL_1:64; then
1 - a <= 1 + l * a by XREAL_1:6; then
(1 - a) / (1 + l * a) <= 1 by XREAL_1:183,B2;
hence thesis by B2,b1,XXREAL_1:1;
end;
ex f being UnOp of [.0,1.] st
for a being Element of [.0,1.] holds
f.a = F(a) from FUNCT_2:sch 8(A1);
hence thesis;
end;
uniqueness
proof
deffunc F(Real) = (1 - $1) / (1 + l * $1);
reconsider A = [.0,1.] as non empty real-membered set;
for o1,o2 being UnOp of A st
(for a being Element of A holds o1.a = F(a)) &
(for a being Element of A holds o2.a = F(a)) holds o1 = o2
from LMOD_7:sch 2;
hence thesis;
end;
end;
theorem
N_CC = SugenoNegation 0
proof
set f = N_CC, g = SugenoNegation 0;
for x being object st x in [.0,1.] holds f.x = g.x
proof
let x be object;
assume x in [.0,1.]; then
reconsider xx = x as Element of [.0,1.];
g.xx = (1 - xx) / (1 + 0 * xx) by DefSugeno
.= f.xx by NDef;
hence thesis;
end;
hence thesis by FUNCT_2:12;
end;
registration let r be -1_greater Real;
cluster SugenoNegation r -> satisfying_(N1) satisfying_(N2);
coherence
proof
set f = SugenoNegation r;
AA: r > -1 by NAT_6:def 1;
AB: 0 in [.0,1.] & 1 in [.0,1.] by XXREAL_1:1; then
AJ: f.0 = (1 - 0) / (1 + r * 0) by DefSugeno,AA
.= 1;
f.1 = (1 - 1) / (1 + r * 1) by DefSugeno,AA,AB
.= 0;
hence f is satisfying_(N1) by AJ;
for x,y being Element of [.0,1.] st x <= y holds f.x >= f.y
proof
let x,y be Element of [.0,1.];
assume
B2: x <= y;
set m = (1 + r * x) * (1 + r * y);
t1: y - x >= x - x by B2,XREAL_1:6;
St: 1 + r > 1 + -1 by NAT_6:def 1,XREAL_1:6;
0 <= x <= 1 by XXREAL_1:1; then
S2: 1 + r * x > 0 by LemmaImp,NAT_6:def 1;
0 <= y <= 1 by XXREAL_1:1; then
S1: 1 + r * y > 0 by LemmaImp,NAT_6:def 1;
R1: f.x = (1 - x) / (1 + r * x) by DefSugeno,AA
.= ((1 - x) * (1 + r * y)) / ((1 + r * x) * (1 + r * y))
by XCMPLX_1:91,S1;
R2: f.y = (1 - y) / (1 + r * y) by DefSugeno,AA
.= ((1 - y) * (1 + r * x)) / ((1 + r * x) * (1 + r * y))
by XCMPLX_1:91,S2;
f.x - f.y = ((y - x) * (1 + r)) / m by R1,R2; then
f.x - f.y + f.y >= 0 + f.y by S1,XREAL_1:6,t1,St,S2;
hence thesis;
end;
hence thesis by NonInc;
end;
end;
begin :: Conjugate Fuzzy Negations
definition let f be UnOp of [.0,1.];
let h be bijective increasing UnOp of [.0,1.];
func ConjNeg (f,h) -> UnOp of [.0,1.] means :CNDef:
for x being Element of [.0,1.] holds
it.x = h".(f.(h.x));
existence
proof
deffunc F(Real) = h".(f.(h.$1));
A1: for a being Element of [.0,1.] holds F(a) in [.0,1.]
proof
let a be Element of [.0,1.];
h".(f.(h.a)) in [.0,1.];
hence thesis;
end;
ex f being UnOp of [.0,1.] st
for a being Element of [.0,1.] holds
f.a = F(a) from FUNCT_2:sch 8(A1);
hence thesis;
end;
uniqueness
proof
deffunc F(Real) = h".(f.(h.$1));
reconsider A = [.0,1.] as non empty real-membered set;
for o1,o2 being UnOp of A st
(for a being Element of A holds o1.a = F(a)) &
(for a being Element of A holds o2.a = F(a)) holds o1 = o2
from LMOD_7:sch 2;
hence thesis;
end;
end;
theorem
for I being Fuzzy_Negation,
f being bijective increasing UnOp of [.0,1.] holds
ConjNeg (I,f) = f" * I * f
proof
let I be Fuzzy_Negation,
f be bijective increasing UnOp of [.0,1.];
set g = ConjNeg (I,f);
AA: dom f = [.0,1.] by FUNCT_2:def 1;
A0: dom g = [.0,1.] by FUNCT_2:def 1;
A1: dom g = dom (f" * I * f) by A0,FUNCT_2:def 1;
for x being object st x in dom g holds
g.x = (f" * I * f).x
proof
let x be object;
assume x in dom g; then
reconsider x as Element of [.0,1.] by FUNCT_2:def 1;
f.x in [.0,1.]; then
AB: f.x in dom I by FUNCT_2:def 1;
g.x = f".(I.(f.x)) by CNDef
.= (f" * I).(f.x) by FUNCT_1:13,AB
.= (f" * I * f).x by FUNCT_1:13,AA;
hence thesis;
end;
hence thesis by A1,FUNCT_1:2;
end;
definition let f,g be UnOp of [.0,1.];
pred f,g are_conjugate means
ex h being bijective increasing UnOp of [.0,1.] st
g = ConjNeg (f,h);
end;
:: Proposition 1.4.8
registration
let N be Fuzzy_Negation,
h be bijective increasing UnOp of [.0,1.];
cluster ConjNeg (N,h) -> satisfying_(N1) satisfying_(N2);
coherence
proof
set CN = ConjNeg (N,h);
AA: 0 in [.0,1.] & 1 in [.0,1.] by XXREAL_1:1; then
A0: CN.0 = h".(N.(h.0)) by CNDef
.= h".(N.0) by LemmaBound
.= h".1 by N1Def
.= 1 by LemmaBound;
A1: CN.1 = h".(N.(h.1)) by AA,CNDef
.= h".(N.1) by LemmaBound
.= h".0 by N1Def
.= 0 by LemmaBound;
for a,b being Element of [.0,1.] st a <= b holds CN.a >= CN.b
proof
let a,b be Element of [.0,1.];
assume a <= b; then
h.a <= h.b by Rosnie; then
B1: N.(h.a) >= N.(h.b) by N2Def,NonInc;
B2: CN.a = h".(N.(h.a)) by CNDef;
CN.b = h".(N.(h.b)) by CNDef;
hence thesis by Rosnie,B1,B2;
end;
hence thesis by A0,A1,NonInc;
end;
end;
theorem :: Theorem 1.4.21
for I being Fuzzy_Implication,
h being bijective increasing UnOp of [.0,1.] holds
ConjNeg (FNegation I,h) = FNegation ConjImpl (I,h)
proof
let I be Fuzzy_Implication,
h be bijective increasing UnOp of [.0,1.];
set f = ConjNeg (FNegation I,h);
set g = FNegation ConjImpl (I,h);
AA: 0 in [.0,1.] by XXREAL_1:1;
for x being Element of [.0,1.] holds f.x = g.x
proof
let x be Element of [.0,1.];
f.x = h".((FNegation I).(h.x)) by CNDef
.= h".(I.(h.x,0)) by FNeg
.= h".(I.(h.x,h.0)) by LemmaBound
.= (ConjImpl (I,h)).(x,0) by AA,BIDef
.= g.x by FNeg;
hence thesis;
end;
hence thesis by FUNCT_2:63;
end;