FUZIMPL3: On Fuzzy Negations Generated by Fuzzy Implications

:: On Fuzzy Negations Generated by Fuzzy Implications
:: by Adam Grabowski
::
:: Received February 26, 2020
:: Copyright (c) 2020-2021 Association of Mizar Users

theorem LemmaImp: :: FUZIMPL3:1

for x, r being Real st 0 <= x & x <= 1 & r > - 1 holds
(x * r) + 1 > 0

proof end;

theorem Wazne1: :: FUZIMPL3:2

for z being Real st z in [.0,1.] & z <> 0 holds
ex w being Element of [.0,1.] st w < z

proof end;

theorem Wazne2: :: FUZIMPL3:3

for z being Real st z in [.0,1.] & z <> 1 holds
ex w being Element of [.0,1.] st w > z

proof end;

registration

cluster Relation-like [.0,1.] -defined [.0,1.] -valued Function-like non empty total quasi_total bijective complex-valued ext-real-valued real-valued increasing for Element of bool [:[.0,1.],[.0,1.]:];

proof end;

end;

registration

cluster Function-like quasi_total bijective non-decreasing -> increasing for Element of bool [:[.0,1.],[.0,1.]:];

cluster Function-like quasi_total bijective increasing -> non-decreasing for Element of bool [:[.0,1.],[.0,1.]:];

end;

registration

let f be bijective increasing UnOp of [.0,1.];

cluster f " -> real-valued ;

end;

registration

let f be bijective increasing UnOp of [.0,1.];

cluster (f | [.0,1.]) " -> real-valued ;

end;

RF220: for h being REAL -defined real-valued Function
for 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 end;

theorem :: FUZIMPL3:4

for f being one-to-one UnOp of [.0,1.]
for d being Element of [.0,1.] st d in rng f holds
(f ") . d in dom f

proof end;

Cosik1: for f being bijective UnOp of [.0,1.] holds (f | [.0,1.]) " is REAL -defined

proof end;

FC9: for f being bijective increasing UnOp of [.0,1.] holds ((f | [.0,1.]) ") | (f .: [.0,1.]) is increasing

proof end;

theorem LemmaIncreas: :: FUZIMPL3:5

for f being bijective increasing UnOp of [.0,1.] holds f " is increasing

proof end;

registration

let f be bijective increasing UnOp of [.0,1.];

cluster f " -> increasing ;

coherence by LemmaIncreas;

end;

theorem Rosnie: :: FUZIMPL3:6

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

theorem NonInc: :: FUZIMPL3:7

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

theorem Decreas: :: FUZIMPL3:8

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

theorem RosnieI: :: FUZIMPL3:9

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

theorem LemmaBound: :: FUZIMPL3:10

for f being bijective increasing UnOp of [.0,1.] holds
( f . 0 = 0 & f . 1 = 1 )

proof end;

registration

let f be bijective increasing UnOp of [.0,1.];

cluster f " -> bijective increasing for UnOp of [.0,1.];

end;

definition

func Theta -> set equals :: FUZIMPL3:def 1
{ f where f is bijective increasing UnOp of [.0,1.] : verum } ;

end;

:: deftheorem defines Theta FUZIMPL3:def 1 :

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: :: FUZIMPL3:def 2
for x1, x2 being Element of [.0,1.] holds it . (x1,x2) = (h ") . (f . ((h . x1),(h . x2)));

proof end;

proof end;

end;

:: deftheorem BIDef defines ConjImpl FUZIMPL3:def 2 :

definition

let f, g be BinOp of [.0,1.];

pred f,g are_conjugate means :: FUZIMPL3:def 3
ex h being bijective increasing UnOp of [.0,1.] st g = ConjImpl (f,h);

end;

:: deftheorem defines are_conjugate FUZIMPL3:def 3 :

registration

let I be Fuzzy_Implication;
let 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 ;

proof end;

end;

theorem :: FUZIMPL3:11

for I being Fuzzy_Implication
for f being bijective increasing UnOp of [.0,1.] holds ConjImpl (I,f) is Fuzzy_Implication ;

registration

cluster Relation-like [:[.K89(),1.],[.K89(),1.]:] -defined [.K89(),1.] -valued Function-like total quasi_total quasi_total complex-valued ext-real-valued real-valued decreasing_on_1st increasing_on_2nd 00-dominant 11-dominant 10-weak 01-dominant with_properties_of_fuzzy_implication with_properties_of_classical_implication satisfying_(LB) satisfying_(RB) satisfying_(NP) satisfying_(EP) satisfying_(IP) satisfying_(OP) for Element of bool [:[:[.K89(),1.],[.K89(),1.]:],[.K89(),1.]:];

proof end;

end;

theorem Prop136a: :: FUZIMPL3:12

for I being Fuzzy_Implication
for f being bijective increasing UnOp of [.0,1.] st I is satisfying_(NP) holds
ConjImpl (I,f) is satisfying_(NP)

proof end;

theorem Prop136b: :: FUZIMPL3:13

for I being Fuzzy_Implication
for f being bijective increasing UnOp of [.0,1.] st I is satisfying_(EP) holds
ConjImpl (I,f) is satisfying_(EP)

proof end;

theorem Prop136c: :: FUZIMPL3:14

for I being Fuzzy_Implication
for f being bijective increasing UnOp of [.0,1.] st I is satisfying_(IP) holds
ConjImpl (I,f) is satisfying_(IP)

proof end;

theorem Prop136d: :: FUZIMPL3:15

for I being Fuzzy_Implication
for f being bijective increasing UnOp of [.0,1.] st I is satisfying_(OP) holds
ConjImpl (I,f) is satisfying_(OP)

proof end;

registration

let I be satisfying_(NP) Fuzzy_Implication;
let 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;
let 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;
let 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;
let f be bijective increasing UnOp of [.0,1.];

cluster ConjImpl (I,f) -> satisfying_(OP) ;

coherence by Prop136d;

end;

theorem :: FUZIMPL3:16

for I being Fuzzy_Implication
for f being bijective increasing UnOp of [.0,1.] holds ConjImpl (I,f) = ((f ") * I) * [:f,f:]

proof end;

definition

let N be UnOp of [.0,1.];

attr N is satisfying_(N1) means :N1Def: :: FUZIMPL3:def 4
( N . 0 = 1 & N . 1 = 0 );

attr N is satisfying_(N2) means :N2Def: :: FUZIMPL3:def 5
N is non-increasing ;

end;

:: deftheorem N1Def defines satisfying_(N1) FUZIMPL3:def 4 :

:: deftheorem N2Def defines satisfying_(N2) FUZIMPL3:def 5 :

definition

func N_CC -> UnOp of [.0,1.] means :NDef: :: FUZIMPL3:def 6
for x being Element of [.0,1.] holds it . x = 1 - x;

proof end;

proof end;

end;

:: deftheorem NDef defines N_CC FUZIMPL3:def 6 :

registration

cluster N_CC -> satisfying_(N1) satisfying_(N2) ;

proof end;

end;

registration

cluster N_CC -> bijective decreasing ;

proof end;

end;

registration

cluster Relation-like [.0,1.] -defined [.0,1.] -valued Function-like non empty total quasi_total bijective complex-valued ext-real-valued real-valued decreasing for Element of bool [:[.0,1.],[.0,1.]:];

proof end;

end;

registration

cluster Relation-like [.0,1.] -defined [.0,1.] -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued satisfying_(N1) satisfying_(N2) for Element of bool [:[.0,1.],[.0,1.]:];

proof 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 :: FUZIMPL3:def 7
ex g being Function of I[01],I[01] st
( f = g & g is continuous );

end;

:: deftheorem defines continuous FUZIMPL3:def 7 :

definition

let N be UnOp of [.0,1.];

attr N is involutive means :: FUZIMPL3:def 8
for x being Element of [.0,1.] holds N . (N . x) = x;

end;

:: deftheorem defines involutive FUZIMPL3:def 8 :

definition

let N be UnOp of [.0,1.];

attr N is satisfying_(N3) means :: FUZIMPL3:def 9
N is decreasing ;

attr N is satisfying_(N4) means :: FUZIMPL3:def 10
N is continuous ;

attr N is satisfying_(N5) means :: FUZIMPL3:def 11
N is involutive ;

end;

:: deftheorem defines satisfying_(N3) FUZIMPL3:def 9 :

:: deftheorem defines satisfying_(N4) FUZIMPL3:def 10 :

:: deftheorem defines satisfying_(N5) FUZIMPL3:def 11 :

definition

let N be UnOp of [.0,1.];

attr N is negation-strict means :: FUZIMPL3:def 12
( N is satisfying_(N3) & N is satisfying_(N4) );

end;

:: deftheorem defines negation-strict FUZIMPL3:def 12 :

definition

let N be UnOp of [.0,1.];

attr N is negation-strong means :: FUZIMPL3:def 13
N is satisfying_(N5) ;

attr N is non-vanishing means :: FUZIMPL3:def 14
for x being Element of [.0,1.] holds
( N . x = 0 iff x = 1 );

attr N is non-filling means :: FUZIMPL3:def 15
for x being Element of [.0,1.] holds
( N . x = 1 iff x = 0 );

end;

:: deftheorem defines negation-strong FUZIMPL3:def 13 :

:: deftheorem defines non-vanishing FUZIMPL3:def 14 :

:: deftheorem defines non-filling FUZIMPL3:def 15 :

theorem :: FUZIMPL3:17

for f being bijective decreasing UnOp of [.0,1.] holds
( f . 0 = 1 & f . 1 = 0 )

proof end;

definition

let I be BinOp of [.0,1.];

func FNegation I -> UnOp of [.0,1.] means :FNeg: :: FUZIMPL3:def 16
for x being Element of [.0,1.] holds it . x = I . (x,0);

proof end;

proof end;

end;

:: deftheorem FNeg defines FNegation FUZIMPL3:def 16 :

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

proof end;

end;

:: Definition 1.4.15

theorem :: FUZIMPL3:18

for I being Fuzzy_Implication holds FNegation I is Fuzzy_Negation ;

definition

func NegationD1 -> UnOp of [.0,1.] means :D1Def: :: FUZIMPL3:def 17
for x being Element of [.0,1.] holds
( ( x = 0 implies it . x = 1 ) & ( x <> 0 implies it . x = 0 ) );

proof end;

proof end;

func NegationD2 -> UnOp of [.0,1.] means :D2Def: :: FUZIMPL3:def 18
for x being Element of [.0,1.] holds
( ( x = 1 implies it . x = 0 ) & ( x <> 1 implies it . x = 1 ) );

proof end;

proof end;

end;

:: deftheorem D1Def defines NegationD1 FUZIMPL3:def 17 :

:: deftheorem D2Def defines NegationD2 FUZIMPL3:def 18 :

:: The Ordering of Fuzzy Negations

definition

let f1, f2 be UnOp of [.0,1.];

pred f1 <= f2 means :: FUZIMPL3:def 19
for a being Element of [.0,1.] holds f1 . a <= f2 . a;

end;

:: deftheorem defines <= FUZIMPL3:def 19 :

registration

cluster NegationD1 -> satisfying_(N1) satisfying_(N2) ;

proof end;

cluster NegationD2 -> satisfying_(N1) satisfying_(N2) ;

proof end;

end;

theorem :: FUZIMPL3:19

for N being Fuzzy_Negation holds
( NegationD1 <= N & N <= NegationD2 )

proof end;

:: On Fuzzy Negations Generated by Fuzzy Implications

theorem :: FUZIMPL3:20

FNegation I_LK = N_CC

proof end;

theorem :: FUZIMPL3:21

FNegation I_GD = NegationD1

proof end;

theorem :: FUZIMPL3:22

FNegation I_RC = N_CC

proof end;

theorem :: FUZIMPL3:23

FNegation I_KD = N_CC

proof end;

theorem :: FUZIMPL3:24

FNegation I_GG = NegationD1

proof end;

theorem :: FUZIMPL3:25

FNegation I_RS = NegationD1

proof end;

theorem :: FUZIMPL3:26

FNegation I_YG = NegationD1

proof end;

theorem :: FUZIMPL3:27

FNegation I_WB = NegationD2

proof end;

theorem :: FUZIMPL3:28

FNegation I_FD = N_CC

proof end;

theorem :: FUZIMPL3:29

for I being satisfying_(EP) satisfying_(OP) BinOp of [.0,1.] holds FNegation I is Fuzzy_Negation ;

theorem Prop1417ii: :: FUZIMPL3:30

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

theorem :: FUZIMPL3:31

for I being satisfying_(EP) satisfying_(OP) BinOp of [.0,1.] holds ((FNegation I) * (FNegation I)) * (FNegation I) = FNegation I

proof end;

definition

let x, l be Real;

attr l is x _greater means :GreatDef: :: FUZIMPL3:def 20
l > x;

end;

:: deftheorem GreatDef defines _greater FUZIMPL3:def 20 :

registration

cluster V31() ext-real V38() - 1 _greater for object ;

proof end;

end;

definition

let l be Real;
assume A0: l > - 1 ;

func SugenoNegation l -> UnOp of [.0,1.] means :DefSugeno: :: FUZIMPL3:def 21
for x being Element of [.0,1.] holds it . x = (1 - x) / (1 + (l * x));

proof end;

proof end;

end;

:: deftheorem DefSugeno defines SugenoNegation FUZIMPL3:def 21 :

theorem :: FUZIMPL3:32

N_CC = SugenoNegation 0

proof end;

registration

let r be - 1 _greater Real;

cluster SugenoNegation r -> satisfying_(N1) satisfying_(N2) ;

proof end;

end;

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: :: FUZIMPL3:def 22
for x being Element of [.0,1.] holds it . x = (h ") . (f . (h . x));

proof end;

proof end;

end;

:: deftheorem CNDef defines ConjNeg FUZIMPL3:def 22 :

theorem :: FUZIMPL3:33

for I being Fuzzy_Negation
for f being bijective increasing UnOp of [.0,1.] holds ConjNeg (I,f) = ((f ") * I) * f

proof end;

definition

let f, g be UnOp of [.0,1.];

pred f,g are_conjugate means :: FUZIMPL3:def 23
ex h being bijective increasing UnOp of [.0,1.] st g = ConjNeg (f,h);

end;

:: deftheorem defines are_conjugate FUZIMPL3:def 23 :

:: Proposition 1.4.8

registration

let N be Fuzzy_Negation;
let h be bijective increasing UnOp of [.0,1.];

cluster ConjNeg (N,h) -> satisfying_(N1) satisfying_(N2) ;

proof end;

end;

theorem :: FUZIMPL3:34

for I being Fuzzy_Implication
for h being bijective increasing UnOp of [.0,1.] holds ConjNeg ((FNegation I),h) = FNegation (ConjImpl (I,h))

proof end;