:: Formal Introduction to Fuzzy Implications
:: by Adam Grabowski
::
:: Received September 3, 2017
:: Copyright (c) 2017-2021 Association of Mizar Users

theorem MaxMinIn01: :: FUZIMPL1:1

for a, b being Element of [.0,1.] holds max (b,(min ((1 - a),(1 - b)))) in [.0,1.]

proof end;

theorem LukaIn01: :: FUZIMPL1:2

for a, b being Element of [.0,1.] holds min (1,((1 - a) + b)) in [.0,1.]

proof end;

theorem ReichenbachIn01: :: FUZIMPL1:3

for a, b being Element of [.0,1.] holds (1 - a) + (a * b) in [.0,1.]

proof end;

theorem Max1In01: :: FUZIMPL1:4

for a, b being Element of [.0,1.] holds max ((1 - a),b) in [.0,1.]

proof end;

theorem PowerIn01: :: FUZIMPL1:5

for a, b being Element of [.0,1.] st ( a > 0 or b > 0 ) holds
b to_power a in [.0,1.]

proof end;

theorem QuoIn01: :: FUZIMPL1:6

for a, b being Element of [.0,1.] st a > b holds
b / a in [.0,1.]

proof end;

definition

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

attr f is decreasing_on_1st means :DefDecr: :: FUZIMPL1:def 1
for x1, x2, y being Element of [.0,1.] st x1 <= x2 holds
f . (x1,y) >= f . (x2,y);

attr f is increasing_on_2nd means :DefIncr: :: FUZIMPL1:def 2
for x, y1, y2 being Element of [.0,1.] st y1 <= y2 holds
f . (x,y1) <= f . (x,y2);

attr f is 00-dominant means :Def00: :: FUZIMPL1:def 3
f . (0,0) = 1;

attr f is 11-dominant means :Def11: :: FUZIMPL1:def 4
f . (1,1) = 1;

attr f is 10-weak means :Def10: :: FUZIMPL1:def 5
f . (1,0) = 0 ;

attr f is 01-dominant means :: FUZIMPL1:def 6
f . (0,1) = 1;

end;

:: deftheorem DefDecr defines decreasing_on_1st FUZIMPL1:def 1 :
for f being BinOp of [.0,1.] holds
( f is decreasing_on_1st iff for x1, x2, y being Element of [.0,1.] st x1 <= x2 holds
f . (x1,y) >= f . (x2,y) );

:: deftheorem DefIncr defines increasing_on_2nd FUZIMPL1:def 2 :
for f being BinOp of [.0,1.] holds
( f is increasing_on_2nd iff for x, y1, y2 being Element of [.0,1.] st y1 <= y2 holds
f . (x,y1) <= f . (x,y2) );

:: deftheorem Def00 defines 00-dominant FUZIMPL1:def 3 :
for f being BinOp of [.0,1.] holds
( f is 00-dominant iff f . (0,0) = 1 );

:: deftheorem Def11 defines 11-dominant FUZIMPL1:def 4 :
for f being BinOp of [.0,1.] holds
( f is 11-dominant iff f . (1,1) = 1 );

:: deftheorem Def10 defines 10-weak FUZIMPL1:def 5 :
for f being BinOp of [.0,1.] holds
( f is 10-weak iff f . (1,0) = 0 );

:: deftheorem defines 01-dominant FUZIMPL1:def 6 :
for f being BinOp of [.0,1.] holds
( f is 01-dominant iff f . (0,1) = 1 );

:: Classical Implication

definition

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

attr f is with_properties_of_fuzzy_implication means :: FUZIMPL1:def 7
( f is decreasing_on_1st & f is increasing_on_2nd & f is 00-dominant & f is 11-dominant & f is 10-weak );

attr f is with_properties_of_classical_implication means :: FUZIMPL1:def 8
( f is 00-dominant & f is 01-dominant & f is 11-dominant & f is 10-weak );

end;

:: deftheorem defines with_properties_of_fuzzy_implication FUZIMPL1:def 7 :
for f being BinOp of [.0,1.] holds
( f is with_properties_of_fuzzy_implication iff ( f is decreasing_on_1st & f is increasing_on_2nd & f is 00-dominant & f is 11-dominant & f is 10-weak ) );

:: deftheorem defines with_properties_of_classical_implication FUZIMPL1:def 8 :
for f being BinOp of [.0,1.] holds
( f is with_properties_of_classical_implication iff ( f is 00-dominant & f is 01-dominant & f is 11-dominant & f is 10-weak ) );

definition

func I_{-1} -> BinOp of [.0,1.] means :I1Def: :: FUZIMPL1:def 9
for x, y being Element of [.0,1.] holds it . (x,y) = max ((1 - x),(min (x,y)));

existence
ex b₁ being BinOp of [.0,1.] st
for x, y being Element of [.0,1.] holds b₁ . (x,y) = max ((1 - x),(min (x,y)))

proof end;

uniqueness
for b₁, b₂ being BinOp of [.0,1.] st ( for x, y being Element of [.0,1.] holds b₁ . (x,y) = max ((1 - x),(min (x,y))) ) & ( for x, y being Element of [.0,1.] holds b₂ . (x,y) = max ((1 - x),(min (x,y))) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem I1Def defines I_{-1} FUZIMPL1:def 9 :
for b₁ being BinOp of [.0,1.] holds
( b₁ = I_{-1} iff for x, y being Element of [.0,1.] holds b₁ . (x,y) = max ((1 - x),(min (x,y))) );

registration

cluster I_{-1} -> increasing_on_2nd 00-dominant 11-dominant 10-weak ;

coherence
( I_{-1} is increasing_on_2nd & I_{-1} is 00-dominant & I_{-1} is 11-dominant & I_{-1} is 10-weak )

proof end;

end;

definition

func I_{-2} -> BinOp of [.0,1.] means :I2Def: :: FUZIMPL1:def 10
for x, y being Element of [.0,1.] holds it . (x,y) = max (y,(min ((1 - x),(1 - y))));

existence
ex b₁ being BinOp of [.0,1.] st
for x, y being Element of [.0,1.] holds b₁ . (x,y) = max (y,(min ((1 - x),(1 - y))))

proof end;

uniqueness
for b₁, b₂ being BinOp of [.0,1.] st ( for x, y being Element of [.0,1.] holds b₁ . (x,y) = max (y,(min ((1 - x),(1 - y)))) ) & ( for x, y being Element of [.0,1.] holds b₂ . (x,y) = max (y,(min ((1 - x),(1 - y)))) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem I2Def defines I_{-2} FUZIMPL1:def 10 :
for b₁ being BinOp of [.0,1.] holds
( b₁ = I_{-2} iff for x, y being Element of [.0,1.] holds b₁ . (x,y) = max (y,(min ((1 - x),(1 - y)))) );

registration

cluster I_{-2} -> decreasing_on_1st 00-dominant 11-dominant 10-weak ;

coherence
( I_{-2} is decreasing_on_1st & I_{-2} is 00-dominant & I_{-2} is 11-dominant & I_{-2} is 10-weak )

proof end;

end;

definition

func I_{-3} -> BinOp of [.0,1.] means :I3Def: :: FUZIMPL1:def 11
for x, y being Element of [.0,1.] holds
( ( y < 1 implies it . (x,y) = 0 ) & ( y = 1 implies it . (x,y) = 1 ) );

existence
ex b₁ being BinOp of [.0,1.] st
for x, y being Element of [.0,1.] holds
( ( y < 1 implies b₁ . (x,y) = 0 ) & ( y = 1 implies b₁ . (x,y) = 1 ) )

proof end;

uniqueness
for b₁, b₂ being BinOp of [.0,1.] st ( for x, y being Element of [.0,1.] holds
( ( y < 1 implies b₁ . (x,y) = 0 ) & ( y = 1 implies b₁ . (x,y) = 1 ) ) ) & ( for x, y being Element of [.0,1.] holds
( ( y < 1 implies b₂ . (x,y) = 0 ) & ( y = 1 implies b₂ . (x,y) = 1 ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem I3Def defines I_{-3} FUZIMPL1:def 11 :
for b₁ being BinOp of [.0,1.] holds
( b₁ = I_{-3} iff for x, y being Element of [.0,1.] holds
( ( y < 1 implies b₁ . (x,y) = 0 ) & ( y = 1 implies b₁ . (x,y) = 1 ) ) );

registration

cluster I_{-3} -> decreasing_on_1st increasing_on_2nd non 00-dominant 11-dominant 10-weak ;

coherence
( I_{-3} is decreasing_on_1st & I_{-3} is increasing_on_2nd & not I_{-3} is 00-dominant & I_{-3} is 11-dominant & I_{-3} is 10-weak )

proof end;

end;

definition

func I_{-4} -> BinOp of [.0,1.] means :I4Def: :: FUZIMPL1:def 12
for x, y being Element of [.0,1.] holds
( ( x = 0 implies it . (x,y) = 1 ) & ( x > 0 implies it . (x,y) = 0 ) );

existence
ex b₁ being BinOp of [.0,1.] st
for x, y being Element of [.0,1.] holds
( ( x = 0 implies b₁ . (x,y) = 1 ) & ( x > 0 implies b₁ . (x,y) = 0 ) )

proof end;

uniqueness
for b₁, b₂ being BinOp of [.0,1.] st ( for x, y being Element of [.0,1.] holds
( ( x = 0 implies b₁ . (x,y) = 1 ) & ( x > 0 implies b₁ . (x,y) = 0 ) ) ) & ( for x, y being Element of [.0,1.] holds
( ( x = 0 implies b₂ . (x,y) = 1 ) & ( x > 0 implies b₂ . (x,y) = 0 ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem I4Def defines I_{-4} FUZIMPL1:def 12 :
for b₁ being BinOp of [.0,1.] holds
( b₁ = I_{-4} iff for x, y being Element of [.0,1.] holds
( ( x = 0 implies b₁ . (x,y) = 1 ) & ( x > 0 implies b₁ . (x,y) = 0 ) ) );

registration

cluster I_{-4} -> decreasing_on_1st increasing_on_2nd 00-dominant non 11-dominant 10-weak ;

coherence
( I_{-4} is decreasing_on_1st & I_{-4} is increasing_on_2nd & I_{-4} is 00-dominant & not I_{-4} is 11-dominant & I_{-4} is 10-weak )

proof end;

end;

definition

func I_{-5} -> BinOp of [.0,1.] means :I5Def: :: FUZIMPL1:def 13
for x, y being Element of [.0,1.] holds it . (x,y) = 1;

existence
ex b₁ being BinOp of [.0,1.] st
for x, y being Element of [.0,1.] holds b₁ . (x,y) = 1

proof end;

uniqueness
for b₁, b₂ being BinOp of [.0,1.] st ( for x, y being Element of [.0,1.] holds b₁ . (x,y) = 1 ) & ( for x, y being Element of [.0,1.] holds b₂ . (x,y) = 1 ) holds
b₁ = b₂

proof end;

end;

:: deftheorem I5Def defines I_{-5} FUZIMPL1:def 13 :
for b₁ being BinOp of [.0,1.] holds
( b₁ = I_{-5} iff for x, y being Element of [.0,1.] holds b₁ . (x,y) = 1 );

registration

cluster I_{-5} -> decreasing_on_1st increasing_on_2nd 00-dominant 11-dominant non 10-weak ;

coherence
( I_{-5} is decreasing_on_1st & I_{-5} is increasing_on_2nd & I_{-5} is 00-dominant & I_{-5} is 11-dominant & not I_{-5} is 10-weak )

proof end;

end;

definition

func Lukasiewicz_implication -> BinOp of [.0,1.] means :Luk: :: FUZIMPL1:def 14
for x, y being Element of [.0,1.] holds it . (x,y) = min (1,((1 - x) + y));

existence
ex b₁ being BinOp of [.0,1.] st
for x, y being Element of [.0,1.] holds b₁ . (x,y) = min (1,((1 - x) + y))

proof end;

uniqueness
for b₁, b₂ being BinOp of [.0,1.] st ( for x, y being Element of [.0,1.] holds b₁ . (x,y) = min (1,((1 - x) + y)) ) & ( for x, y being Element of [.0,1.] holds b₂ . (x,y) = min (1,((1 - x) + y)) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Luk defines Lukasiewicz_implication FUZIMPL1:def 14 :
for b₁ being BinOp of [.0,1.] holds
( b₁ = Lukasiewicz_implication iff for x, y being Element of [.0,1.] holds b₁ . (x,y) = min (1,((1 - x) + y)) );

registration

cluster Lukasiewicz_implication -> decreasing_on_1st increasing_on_2nd 00-dominant 11-dominant 10-weak ;

coherence
( Lukasiewicz_implication is decreasing_on_1st & Lukasiewicz_implication is increasing_on_2nd & Lukasiewicz_implication is 00-dominant & Lukasiewicz_implication is 11-dominant & Lukasiewicz_implication is 10-weak )

proof end;

end;

registration

cluster V1() V4([:[.0,1.],[.0,1.]:]) V5([.0,1.]) Function-like V29([:[.0,1.],[.0,1.]:],[.0,1.]) with_properties_of_fuzzy_implication for Element of bool [:[:[.0,1.],[.0,1.]:],[.0,1.]:];

existence
ex b₁ being BinOp of [.0,1.] st b₁ is with_properties_of_fuzzy_implication

proof end;

end;

registration

cluster Function-like V29([:[.0,1.],[.0,1.]:],[.0,1.]) with_properties_of_fuzzy_implication -> decreasing_on_1st increasing_on_2nd 00-dominant 11-dominant 10-weak for Element of bool [:[:[.0,1.],[.0,1.]:],[.0,1.]:];

coherence
for b₁ being BinOp of [.0,1.] st b₁ is with_properties_of_fuzzy_implication holds
( b₁ is decreasing_on_1st & b₁ is increasing_on_2nd & b₁ is 00-dominant & b₁ is 11-dominant & b₁ is 10-weak ) ;

cluster Function-like V29([:[.0,1.],[.0,1.]:],[.0,1.]) decreasing_on_1st increasing_on_2nd 00-dominant 11-dominant 10-weak 01-dominant -> with_properties_of_fuzzy_implication for Element of bool [:[:[.0,1.],[.0,1.]:],[.0,1.]:];

coherence
for b₁ being BinOp of [.0,1.] st b₁ is decreasing_on_1st & b₁ is increasing_on_2nd & b₁ is 00-dominant & b₁ is 01-dominant & b₁ is 11-dominant & b₁ is 10-weak holds
b₁ is with_properties_of_fuzzy_implication ;

cluster Function-like V29([:[.0,1.],[.0,1.]:],[.0,1.]) with_properties_of_classical_implication -> 00-dominant 11-dominant 10-weak 01-dominant for Element of bool [:[:[.0,1.],[.0,1.]:],[.0,1.]:];

coherence
for b₁ being BinOp of [.0,1.] st b₁ is with_properties_of_classical_implication holds
( b₁ is 00-dominant & b₁ is 01-dominant & b₁ is 11-dominant & b₁ is 10-weak ) ;

cluster Function-like V29([:[.0,1.],[.0,1.]:],[.0,1.]) 00-dominant 11-dominant 10-weak 01-dominant -> with_properties_of_classical_implication for Element of bool [:[:[.0,1.],[.0,1.]:],[.0,1.]:];

coherence
for b₁ being BinOp of [.0,1.] st b₁ is 00-dominant & b₁ is 01-dominant & b₁ is 11-dominant & b₁ is 10-weak holds
b₁ is with_properties_of_classical_implication ;

cluster Function-like V29([:[.0,1.],[.0,1.]:],[.0,1.]) with_properties_of_fuzzy_implication -> with_properties_of_classical_implication for Element of bool [:[:[.0,1.],[.0,1.]:],[.0,1.]:];

coherence
for b₁ being BinOp of [.0,1.] st b₁ is with_properties_of_fuzzy_implication holds
b₁ is with_properties_of_classical_implication

proof end;

end;

definition

mode Fuzzy_Implication is decreasing_on_1st increasing_on_2nd 00-dominant 11-dominant 10-weak BinOp of [.0,1.];

end;

definition

func FI -> set equals :: FUZIMPL1:def 15
{ f where f is Fuzzy_Implication : verum } ;

coherence
{ f where f is Fuzzy_Implication : verum } is set ;

end;

:: deftheorem defines FI FUZIMPL1:def 15 :
FI = { f where f is Fuzzy_Implication : verum } ;

definition

func Goedel_implication -> BinOp of [.0,1.] means :Goedel: :: FUZIMPL1:def 16
for x, y being Element of [.0,1.] holds
( ( x <= y implies it . (x,y) = 1 ) & ( x > y implies it . (x,y) = y ) );

existence
ex b₁ being BinOp of [.0,1.] st
for x, y being Element of [.0,1.] holds
( ( x <= y implies b₁ . (x,y) = 1 ) & ( x > y implies b₁ . (x,y) = y ) )

proof end;

uniqueness
for b₁, b₂ being BinOp of [.0,1.] st ( for x, y being Element of [.0,1.] holds
( ( x <= y implies b₁ . (x,y) = 1 ) & ( x > y implies b₁ . (x,y) = y ) ) ) & ( for x, y being Element of [.0,1.] holds
( ( x <= y implies b₂ . (x,y) = 1 ) & ( x > y implies b₂ . (x,y) = y ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Goedel defines Goedel_implication FUZIMPL1:def 16 :
for b₁ being BinOp of [.0,1.] holds
( b₁ = Goedel_implication iff for x, y being Element of [.0,1.] holds
( ( x <= y implies b₁ . (x,y) = 1 ) & ( x > y implies b₁ . (x,y) = y ) ) );

registration

cluster Goedel_implication -> decreasing_on_1st increasing_on_2nd 00-dominant 11-dominant 10-weak ;

coherence
( Goedel_implication is decreasing_on_1st & Goedel_implication is increasing_on_2nd & Goedel_implication is 00-dominant & Goedel_implication is 11-dominant & Goedel_implication is 10-weak )

proof end;

end;

definition

func Reichenbach_implication -> BinOp of [.0,1.] means :Reichen: :: FUZIMPL1:def 17
for x, y being Element of [.0,1.] holds it . (x,y) = (1 - x) + (x * y);

existence
ex b₁ being BinOp of [.0,1.] st
for x, y being Element of [.0,1.] holds b₁ . (x,y) = (1 - x) + (x * y)

proof end;

uniqueness
for b₁, b₂ being BinOp of [.0,1.] st ( for x, y being Element of [.0,1.] holds b₁ . (x,y) = (1 - x) + (x * y) ) & ( for x, y being Element of [.0,1.] holds b₂ . (x,y) = (1 - x) + (x * y) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Reichen defines Reichenbach_implication FUZIMPL1:def 17 :
for b₁ being BinOp of [.0,1.] holds
( b₁ = Reichenbach_implication iff for x, y being Element of [.0,1.] holds b₁ . (x,y) = (1 - x) + (x * y) );

registration

cluster Reichenbach_implication -> decreasing_on_1st increasing_on_2nd 00-dominant 11-dominant 10-weak ;

coherence
( Reichenbach_implication is decreasing_on_1st & Reichenbach_implication is increasing_on_2nd & Reichenbach_implication is 00-dominant & Reichenbach_implication is 11-dominant & Reichenbach_implication is 10-weak )

proof end;

end;

definition

func Kleene-Dienes_implication -> BinOp of [.0,1.] means :Kleene: :: FUZIMPL1:def 18
for x, y being Element of [.0,1.] holds it . (x,y) = max ((1 - x),y);

existence
ex b₁ being BinOp of [.0,1.] st
for x, y being Element of [.0,1.] holds b₁ . (x,y) = max ((1 - x),y)

proof end;

uniqueness
for b₁, b₂ being BinOp of [.0,1.] st ( for x, y being Element of [.0,1.] holds b₁ . (x,y) = max ((1 - x),y) ) & ( for x, y being Element of [.0,1.] holds b₂ . (x,y) = max ((1 - x),y) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Kleene defines Kleene-Dienes_implication FUZIMPL1:def 18 :
for b₁ being BinOp of [.0,1.] holds
( b₁ = Kleene-Dienes_implication iff for x, y being Element of [.0,1.] holds b₁ . (x,y) = max ((1 - x),y) );

registration

cluster Kleene-Dienes_implication -> decreasing_on_1st increasing_on_2nd 00-dominant 11-dominant 10-weak ;

coherence
( Kleene-Dienes_implication is decreasing_on_1st & Kleene-Dienes_implication is increasing_on_2nd & Kleene-Dienes_implication is 00-dominant & Kleene-Dienes_implication is 11-dominant & Kleene-Dienes_implication is 10-weak )

proof end;

end;

definition

func Goguen_implication -> BinOp of [.0,1.] means :Goguen: :: FUZIMPL1:def 19
for x, y being Element of [.0,1.] holds
( ( x <= y implies it . (x,y) = 1 ) & ( x > y implies it . (x,y) = y / x ) );

existence
ex b₁ being BinOp of [.0,1.] st
for x, y being Element of [.0,1.] holds
( ( x <= y implies b₁ . (x,y) = 1 ) & ( x > y implies b₁ . (x,y) = y / x ) )

proof end;

uniqueness
for b₁, b₂ being BinOp of [.0,1.] st ( for x, y being Element of [.0,1.] holds
( ( x <= y implies b₁ . (x,y) = 1 ) & ( x > y implies b₁ . (x,y) = y / x ) ) ) & ( for x, y being Element of [.0,1.] holds
( ( x <= y implies b₂ . (x,y) = 1 ) & ( x > y implies b₂ . (x,y) = y / x ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Goguen defines Goguen_implication FUZIMPL1:def 19 :
for b₁ being BinOp of [.0,1.] holds
( b₁ = Goguen_implication iff for x, y being Element of [.0,1.] holds
( ( x <= y implies b₁ . (x,y) = 1 ) & ( x > y implies b₁ . (x,y) = y / x ) ) );

registration

cluster Goguen_implication -> decreasing_on_1st increasing_on_2nd 00-dominant 11-dominant 10-weak ;

coherence
( Goguen_implication is decreasing_on_1st & Goguen_implication is increasing_on_2nd & Goguen_implication is 00-dominant & Goguen_implication is 11-dominant & Goguen_implication is 10-weak )

proof end;

end;

definition

func Rescher_implication -> BinOp of [.0,1.] means :Rescher: :: FUZIMPL1:def 20
for x, y being Element of [.0,1.] holds
( ( x <= y implies it . (x,y) = 1 ) & ( x > y implies it . (x,y) = 0 ) );

existence
ex b₁ being BinOp of [.0,1.] st
for x, y being Element of [.0,1.] holds
( ( x <= y implies b₁ . (x,y) = 1 ) & ( x > y implies b₁ . (x,y) = 0 ) )

proof end;

uniqueness
for b₁, b₂ being BinOp of [.0,1.] st ( for x, y being Element of [.0,1.] holds
( ( x <= y implies b₁ . (x,y) = 1 ) & ( x > y implies b₁ . (x,y) = 0 ) ) ) & ( for x, y being Element of [.0,1.] holds
( ( x <= y implies b₂ . (x,y) = 1 ) & ( x > y implies b₂ . (x,y) = 0 ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Rescher defines Rescher_implication FUZIMPL1:def 20 :
for b₁ being BinOp of [.0,1.] holds
( b₁ = Rescher_implication iff for x, y being Element of [.0,1.] holds
( ( x <= y implies b₁ . (x,y) = 1 ) & ( x > y implies b₁ . (x,y) = 0 ) ) );

registration

cluster Rescher_implication -> decreasing_on_1st increasing_on_2nd 00-dominant 11-dominant 10-weak ;

coherence
( Rescher_implication is decreasing_on_1st & Rescher_implication is increasing_on_2nd & Rescher_implication is 00-dominant & Rescher_implication is 11-dominant & Rescher_implication is 10-weak )

proof end;

end;

definition

func Yager_implication -> BinOp of [.0,1.] means :Yager: :: FUZIMPL1:def 21
for x, y being Element of [.0,1.] holds
( ( x = y & y = 0 implies it . (x,y) = 1 ) & ( ( x > 0 or y > 0 ) implies it . (x,y) = y to_power x ) );

existence
ex b₁ being BinOp of [.0,1.] st
for x, y being Element of [.0,1.] holds
( ( x = y & y = 0 implies b₁ . (x,y) = 1 ) & ( ( x > 0 or y > 0 ) implies b₁ . (x,y) = y to_power x ) )

proof end;

uniqueness
for b₁, b₂ being BinOp of [.0,1.] st ( for x, y being Element of [.0,1.] holds
( ( x = y & y = 0 implies b₁ . (x,y) = 1 ) & ( ( x > 0 or y > 0 ) implies b₁ . (x,y) = y to_power x ) ) ) & ( for x, y being Element of [.0,1.] holds
( ( x = y & y = 0 implies b₂ . (x,y) = 1 ) & ( ( x > 0 or y > 0 ) implies b₂ . (x,y) = y to_power x ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Yager defines Yager_implication FUZIMPL1:def 21 :
for b₁ being BinOp of [.0,1.] holds
( b₁ = Yager_implication iff for x, y being Element of [.0,1.] holds
( ( x = y & y = 0 implies b₁ . (x,y) = 1 ) & ( ( x > 0 or y > 0 ) implies b₁ . (x,y) = y to_power x ) ) );

registration

cluster Yager_implication -> decreasing_on_1st increasing_on_2nd 00-dominant 11-dominant 10-weak ;

coherence
( Yager_implication is decreasing_on_1st & Yager_implication is increasing_on_2nd & Yager_implication is 00-dominant & Yager_implication is 11-dominant & Yager_implication is 10-weak )

proof end;

end;

definition

func Weber_implication -> BinOp of [.0,1.] means :Weber: :: FUZIMPL1:def 22
for x, y being Element of [.0,1.] holds
( ( x < 1 implies it . (x,y) = 1 ) & ( x = 1 implies it . (x,y) = y ) );

existence
ex b₁ being BinOp of [.0,1.] st
for x, y being Element of [.0,1.] holds
( ( x < 1 implies b₁ . (x,y) = 1 ) & ( x = 1 implies b₁ . (x,y) = y ) )

proof end;

uniqueness
for b₁, b₂ being BinOp of [.0,1.] st ( for x, y being Element of [.0,1.] holds
( ( x < 1 implies b₁ . (x,y) = 1 ) & ( x = 1 implies b₁ . (x,y) = y ) ) ) & ( for x, y being Element of [.0,1.] holds
( ( x < 1 implies b₂ . (x,y) = 1 ) & ( x = 1 implies b₂ . (x,y) = y ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Weber defines Weber_implication FUZIMPL1:def 22 :
for b₁ being BinOp of [.0,1.] holds
( b₁ = Weber_implication iff for x, y being Element of [.0,1.] holds
( ( x < 1 implies b₁ . (x,y) = 1 ) & ( x = 1 implies b₁ . (x,y) = y ) ) );

registration

cluster Weber_implication -> decreasing_on_1st increasing_on_2nd 00-dominant 11-dominant 10-weak ;

coherence
( Weber_implication is decreasing_on_1st & Weber_implication is increasing_on_2nd & Weber_implication is 00-dominant & Weber_implication is 11-dominant & Weber_implication is 10-weak )

proof end;

end;

definition

func Fodor_implication -> BinOp of [.0,1.] means :Fodor: :: FUZIMPL1:def 23
for x, y being Element of [.0,1.] holds
( ( x <= y implies it . (x,y) = 1 ) & ( x > y implies it . (x,y) = max ((1 - x),y) ) );

existence
ex b₁ being BinOp of [.0,1.] st
for x, y being Element of [.0,1.] holds
( ( x <= y implies b₁ . (x,y) = 1 ) & ( x > y implies b₁ . (x,y) = max ((1 - x),y) ) )

proof end;

uniqueness
for b₁, b₂ being BinOp of [.0,1.] st ( for x, y being Element of [.0,1.] holds
( ( x <= y implies b₁ . (x,y) = 1 ) & ( x > y implies b₁ . (x,y) = max ((1 - x),y) ) ) ) & ( for x, y being Element of [.0,1.] holds
( ( x <= y implies b₂ . (x,y) = 1 ) & ( x > y implies b₂ . (x,y) = max ((1 - x),y) ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Fodor defines Fodor_implication FUZIMPL1:def 23 :
for b₁ being BinOp of [.0,1.] holds
( b₁ = Fodor_implication iff for x, y being Element of [.0,1.] holds
( ( x <= y implies b₁ . (x,y) = 1 ) & ( x > y implies b₁ . (x,y) = max ((1 - x),y) ) ) );

registration

cluster Fodor_implication -> decreasing_on_1st increasing_on_2nd 00-dominant 11-dominant 10-weak ;

coherence
( Fodor_implication is decreasing_on_1st & Fodor_implication is increasing_on_2nd & Fodor_implication is 00-dominant & Fodor_implication is 11-dominant & Fodor_implication is 10-weak )

proof end;

end;

definition

func I_{0} -> BinOp of [.0,1.] means :I0Impl: :: FUZIMPL1:def 24
for x, y being Element of [.0,1.] holds
( ( ( x = 0 or y = 1 ) implies it . (x,y) = 1 ) & ( x > 0 & y < 1 implies it . (x,y) = 0 ) );

existence
ex b₁ being BinOp of [.0,1.] st
for x, y being Element of [.0,1.] holds
( ( ( x = 0 or y = 1 ) implies b₁ . (x,y) = 1 ) & ( x > 0 & y < 1 implies b₁ . (x,y) = 0 ) )

proof end;

uniqueness
for b₁, b₂ being BinOp of [.0,1.] st ( for x, y being Element of [.0,1.] holds
( ( ( x = 0 or y = 1 ) implies b₁ . (x,y) = 1 ) & ( x > 0 & y < 1 implies b₁ . (x,y) = 0 ) ) ) & ( for x, y being Element of [.0,1.] holds
( ( ( x = 0 or y = 1 ) implies b₂ . (x,y) = 1 ) & ( x > 0 & y < 1 implies b₂ . (x,y) = 0 ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem I0Impl defines I_{0} FUZIMPL1:def 24 :
for b₁ being BinOp of [.0,1.] holds
( b₁ = I_{0} iff for x, y being Element of [.0,1.] holds
( ( ( x = 0 or y = 1 ) implies b₁ . (x,y) = 1 ) & ( x > 0 & y < 1 implies b₁ . (x,y) = 0 ) ) );

registration

cluster I_{0} -> decreasing_on_1st increasing_on_2nd 00-dominant 11-dominant 10-weak ;

coherence
( I_{0} is decreasing_on_1st & I_{0} is increasing_on_2nd & I_{0} is 00-dominant & I_{0} is 11-dominant & I_{0} is 10-weak )

proof end;

end;

definition

func I_{1} -> BinOp of [.0,1.] means :I1Impl: :: FUZIMPL1:def 25
for x, y being Element of [.0,1.] holds
( ( ( x < 1 or y > 0 ) implies it . (x,y) = 1 ) & ( x = 1 & y = 0 implies it . (x,y) = 0 ) );

existence
ex b₁ being BinOp of [.0,1.] st
for x, y being Element of [.0,1.] holds
( ( ( x < 1 or y > 0 ) implies b₁ . (x,y) = 1 ) & ( x = 1 & y = 0 implies b₁ . (x,y) = 0 ) )

proof end;

uniqueness
for b₁, b₂ being BinOp of [.0,1.] st ( for x, y being Element of [.0,1.] holds
( ( ( x < 1 or y > 0 ) implies b₁ . (x,y) = 1 ) & ( x = 1 & y = 0 implies b₁ . (x,y) = 0 ) ) ) & ( for x, y being Element of [.0,1.] holds
( ( ( x < 1 or y > 0 ) implies b₂ . (x,y) = 1 ) & ( x = 1 & y = 0 implies b₂ . (x,y) = 0 ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem I1Impl defines I_{1} FUZIMPL1:def 25 :
for b₁ being BinOp of [.0,1.] holds
( b₁ = I_{1} iff for x, y being Element of [.0,1.] holds
( ( ( x < 1 or y > 0 ) implies b₁ . (x,y) = 1 ) & ( x = 1 & y = 0 implies b₁ . (x,y) = 0 ) ) );

registration

cluster I_{1} -> decreasing_on_1st increasing_on_2nd 00-dominant 11-dominant 10-weak ;

coherence
( I_{1} is decreasing_on_1st & I_{1} is increasing_on_2nd & I_{1} is 00-dominant & I_{1} is 11-dominant & I_{1} is 10-weak )

proof end;

end;

definition

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

attr f is satisfying_(LB) means :: FUZIMPL1:def 26
for y being Element of [.0,1.] holds f . (0,y) = 1;

attr f is satisfying_(RB) means :: FUZIMPL1:def 27
for x being Element of [.0,1.] holds f . (x,1) = 1;

end;

:: deftheorem defines satisfying_(LB) FUZIMPL1:def 26 :
for f being BinOp of [.0,1.] holds
( f is satisfying_(LB) iff for y being Element of [.0,1.] holds f . (0,y) = 1 );

:: deftheorem defines satisfying_(RB) FUZIMPL1:def 27 :
for f being BinOp of [.0,1.] holds
( f is satisfying_(RB) iff for x being Element of [.0,1.] holds f . (x,1) = 1 );

theorem LBProp: :: FUZIMPL1:7

for fi being Fuzzy_Implication
for y being Element of [.0,1.] holds fi . (0,y) = 1

proof end;

theorem RBProp: :: FUZIMPL1:8

for fi being Fuzzy_Implication
for x being Element of [.0,1.] holds fi . (x,1) = 1

proof end;

registration

cluster Function-like V29([:[.0,1.],[.0,1.]:],[.0,1.]) decreasing_on_1st increasing_on_2nd 00-dominant 11-dominant 10-weak -> satisfying_(LB) satisfying_(RB) for Element of bool [:[:[.0,1.],[.0,1.]:],[.0,1.]:];

coherence
for b₁ being Fuzzy_Implication holds
( b₁ is satisfying_(LB) & b₁ is satisfying_(RB) ) by LBProp, RBProp;

end;

theorem :: FUZIMPL1:9

for fi being Fuzzy_Implication holds I_{0} <= fi

proof end;

theorem :: FUZIMPL1:10

for fi being Fuzzy_Implication holds fi <= I_{1}

proof end;