:: Fundamental Properties of Fuzzy Implications
:: by Adam Grabowski
::
:: Received September 29, 2018
:: Copyright (c) 2018-2021 Association of Mizar Users

notation

synonym I_LK for Lukasiewicz_implication ;
synonym I_GD for Goedel_implication ;
synonym I_RC for Reichenbach_implication ;
synonym I_KD for Kleene-Dienes_implication ;
synonym I_GG for Goguen_implication ;
synonym I_RS for Rescher_implication ;
synonym I_YG for Yager_implication ;
synonym I_WB for Weber_implication ;
synonym I_FD for Fodor_implication ;

end;

Lemma00: for x, y being Element of [.0,1.] holds (x * y) + ((1 - x) * 1) in [.y,1.]

proof end;

LemmaHalf: (1 / 2) to_power (1 / 2) <> 1

proof end;

theorem :: FUZIMPL2:1

#R 1 = (AffineMap (1,0)) | (right_open_halfline 0)

proof end;

theorem LemmaAffine: :: FUZIMPL2:2

for a, b being Real holds
( AffineMap (a,b) is_differentiable_on REAL & ( for x being Real holds diff ((AffineMap (a,b)),x) = a ) )

proof end;

theorem :: FUZIMPL2:3

for x, y being Element of [.0,1.] st 0 < x & x < 1 & 0 < y & y < 1 holds
((#R x) + (AffineMap ((- x),(x - 1)))) | ].0,1.[ is increasing

proof end;

theorem :: FUZIMPL2:4

for x being Element of [.0,1.]
for u being Real st u in ].0,1.] holds
((#R x) + (AffineMap ((- x),(x - 1)))) . u = (((u to_power x) - 1) + x) - (x * u)

proof end;

theorem Lemma01: :: FUZIMPL2:5

for x, y being Element of [.0,1.] holds
( ( x <= y implies I_LK . (x,y) = 1 ) & ( x > y implies I_LK . (x,y) = (1 - x) + y ) )

proof end;

theorem :: FUZIMPL2:6

for x, y being Element of [.0,1.] holds
( ( x = 0 implies I_GG . (x,y) = 1 ) & ( x > 0 implies I_GG . (x,y) = min (1,(y / x)) ) )

proof end;

Lemma03: for x, y being Element of [.0,1.] holds max ((1 - x),y) in [.0,1.]

proof end;

Lemma11: for x, y being Element of [.0,1.] st x <> 0 holds
y <= y / x

proof end;

Lemacik1: for x, y being Element of [.0,1.] st x > y holds
(1 - x) + y >= y / x

proof end;

Lemma111: I_KD <= I_RC

proof end;

Lemma112: I_RC <= I_LK

proof end;

Lemma113: I_LK <= I_WB

proof end;

theorem :: FUZIMPL2:7

( I_KD <= I_RC & I_RC <= I_LK & I_LK <= I_WB ) by Lemma111, Lemma112, Lemma113;

Lemma121: I_RS <= I_GD

proof end;

Lemma122: I_GD <= I_GG

proof end;

Lemma123: I_GG <= I_LK

proof end;

theorem :: FUZIMPL2:8

( I_RS <= I_GD & I_GD <= I_GG & I_GG <= I_LK & I_LK <= I_WB ) by Lemma121, Lemma122, Lemma123, Lemma113;

Lemma132: I_RC <= I_LK

proof end;

theorem :: FUZIMPL2:9

( I_RC <= I_LK & I_LK <= I_WB ) by Lemma132, Lemma113;

Lemma141: I_KD <= I_FD

proof end;

Lemma142: I_FD <= I_LK

proof end;

theorem :: FUZIMPL2:10

( I_KD <= I_FD & I_FD <= I_LK & I_LK <= I_WB ) by Lemma141, Lemma142, Lemma113;

Lemma151: I_RS <= I_GD

proof end;

Lemma152: I_GD <= I_FD

proof end;

Lemma153: I_FD <= I_LK

proof end;

theorem :: FUZIMPL2:11

( I_RS <= I_GD & I_GD <= I_FD & I_FD <= I_LK & I_LK <= I_WB ) by Lemma151, Lemma152, Lemma153, Lemma113;

definition

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

attr I is satisfying_(NP) means :: FUZIMPL2:def 1
for y being Element of [.0,1.] holds I . (1,y) = y;

attr I is satisfying_(EP) means :: FUZIMPL2:def 2
for x, y, z being Element of [.0,1.] holds I . (x,(I . (y,z))) = I . (y,(I . (x,z)));

attr I is satisfying_(IP) means :: FUZIMPL2:def 3
for x being Element of [.0,1.] holds I . (x,x) = 1;

attr I is satisfying_(OP) means :: FUZIMPL2:def 4
for x, y being Element of [.0,1.] holds
( I . (x,y) = 1 iff x <= y );

end;

:: deftheorem defines satisfying_(NP) FUZIMPL2:def 1 :
for I being BinOp of [.0,1.] holds
( I is satisfying_(NP) iff for y being Element of [.0,1.] holds I . (1,y) = y );

:: deftheorem defines satisfying_(EP) FUZIMPL2:def 2 :
for I being BinOp of [.0,1.] holds
( I is satisfying_(EP) iff for x, y, z being Element of [.0,1.] holds I . (x,(I . (y,z))) = I . (y,(I . (x,z))) );

:: deftheorem defines satisfying_(IP) FUZIMPL2:def 3 :
for I being BinOp of [.0,1.] holds
( I is satisfying_(IP) iff for x being Element of [.0,1.] holds I . (x,x) = 1 );

:: deftheorem defines satisfying_(OP) FUZIMPL2:def 4 :
for I being BinOp of [.0,1.] holds
( I is satisfying_(OP) iff for x, y being Element of [.0,1.] holds
( I . (x,y) = 1 iff x <= y ) );

notation

let I be BinOp of [.0,1.];
synonym satisfying_(NC) I for 01-dominant ;
synonym satisfying_(I1) I for decreasing_on_1st ;
synonym satisfying_(I2) I for increasing_on_2nd ;
synonym satisfying_(I3) I for 00-dominant ;
synonym satisfying_(I4) I for 11-dominant ;
synonym satisfying_(I5) I for 10-weak ;

end;

theorem LemmaXA: :: FUZIMPL2:12

for I being BinOp of [.0,1.] st I is satisfying_(LB) holds
( I is satisfying_(I3) & I is satisfying_(NC) )

proof end;

registration

cluster Function-like V29(K17([.0,1.],[.0,1.]),[.0,1.]) satisfying_(LB) -> satisfying_(I3) satisfying_(NC) for Element of K16(K17(K17([.0,1.],[.0,1.]),[.0,1.]));

coherence
for b₁ being BinOp of [.0,1.] st b₁ is satisfying_(LB) holds
( b₁ is satisfying_(I3) & b₁ is satisfying_(NC) ) by LemmaXA;

end;

theorem LemmaVA: :: FUZIMPL2:13

for I being BinOp of [.0,1.] st I is satisfying_(RB) holds
( I is satisfying_(I4) & I is satisfying_(NC) )

proof end;

registration

cluster Function-like V29(K17([.0,1.],[.0,1.]),[.0,1.]) satisfying_(RB) -> satisfying_(I4) satisfying_(NC) for Element of K16(K17(K17([.0,1.],[.0,1.]),[.0,1.]));

coherence
for b₁ being BinOp of [.0,1.] st b₁ is satisfying_(RB) holds
( b₁ is satisfying_(I4) & b₁ is satisfying_(NC) ) by LemmaVA;

end;

theorem LemmaWA: :: FUZIMPL2:14

for I being BinOp of [.0,1.] st I is satisfying_(NP) holds
( I is satisfying_(I4) & I is satisfying_(I5) )

proof end;

registration

cluster Function-like V29(K17([.0,1.],[.0,1.]),[.0,1.]) satisfying_(NP) -> satisfying_(I4) satisfying_(I5) for Element of K16(K17(K17([.0,1.],[.0,1.]),[.0,1.]));

coherence
for b₁ being BinOp of [.0,1.] st b₁ is satisfying_(NP) holds
( b₁ is satisfying_(I4) & b₁ is satisfying_(I5) ) by LemmaWA;

end;

theorem LemmaZA: :: FUZIMPL2:15

for I being BinOp of [.0,1.] st I is satisfying_(IP) holds
( I is satisfying_(I3) & I is satisfying_(I4) )

proof end;

registration

cluster Function-like V29(K17([.0,1.],[.0,1.]),[.0,1.]) satisfying_(IP) -> satisfying_(I3) satisfying_(I4) for Element of K16(K17(K17([.0,1.],[.0,1.]),[.0,1.]));

coherence
for b₁ being BinOp of [.0,1.] st b₁ is satisfying_(IP) holds
( b₁ is satisfying_(I3) & b₁ is satisfying_(I4) ) by LemmaZA;

end;

theorem LemmaAA: :: FUZIMPL2:16

for I being BinOp of [.0,1.] st I is satisfying_(OP) holds
( I is satisfying_(I3) & I is satisfying_(I4) & I is satisfying_(NC) & I is satisfying_(LB) & I is satisfying_(RB) & I is satisfying_(IP) )

proof end;

registration

cluster Function-like V29(K17([.0,1.],[.0,1.]),[.0,1.]) satisfying_(OP) -> satisfying_(I3) satisfying_(I4) satisfying_(NC) satisfying_(LB) satisfying_(RB) satisfying_(IP) for Element of K16(K17(K17([.0,1.],[.0,1.]),[.0,1.]));

coherence
for b₁ being BinOp of [.0,1.] st b₁ is satisfying_(OP) holds
( b₁ is satisfying_(I3) & b₁ is satisfying_(I4) & b₁ is satisfying_(NC) & b₁ is satisfying_(LB) & b₁ is satisfying_(RB) & b₁ is satisfying_(IP) ) by LemmaAA;

end;

theorem LemmaAB: :: FUZIMPL2:17

for I being BinOp of [.0,1.] st I is satisfying_(EP) & I is satisfying_(OP) holds
( I is satisfying_(I1) & I is satisfying_(I3) & I is satisfying_(I4) & I is satisfying_(I5) & I is satisfying_(LB) & I is satisfying_(RB) & I is satisfying_(NC) & I is satisfying_(NP) & I is satisfying_(IP) )

proof end;

registration

cluster Function-like V29(K17([.0,1.],[.0,1.]),[.0,1.]) satisfying_(EP) satisfying_(OP) -> satisfying_(I1) satisfying_(I5) satisfying_(NP) for Element of K16(K17(K17([.0,1.],[.0,1.]),[.0,1.]));

coherence
for b₁ being BinOp of [.0,1.] st b₁ is satisfying_(EP) & b₁ is satisfying_(OP) holds
( b₁ is satisfying_(I1) & b₁ is satisfying_(I5) & b₁ is satisfying_(NP) ) by LemmaAB;

end;

registration

cluster I_LK -> satisfying_(NP) satisfying_(EP) satisfying_(IP) satisfying_(OP) ;

coherence
( I_LK is satisfying_(NP) & I_LK is satisfying_(EP) & I_LK is satisfying_(IP) & I_LK is satisfying_(OP) )

proof end;

cluster I_GD -> satisfying_(NP) satisfying_(EP) satisfying_(IP) satisfying_(OP) ;

coherence
( I_GD is satisfying_(NP) & I_GD is satisfying_(EP) & I_GD is satisfying_(IP) & I_GD is satisfying_(OP) )

proof end;

cluster I_RC -> satisfying_(NP) satisfying_(EP) non satisfying_(IP) non satisfying_(OP) ;

coherence
( I_RC is satisfying_(NP) & I_RC is satisfying_(EP) & not I_RC is satisfying_(IP) & not I_RC is satisfying_(OP) )

proof end;

cluster I_KD -> satisfying_(NP) satisfying_(EP) non satisfying_(IP) non satisfying_(OP) ;

coherence
( I_KD is satisfying_(NP) & I_KD is satisfying_(EP) & not I_KD is satisfying_(IP) & not I_KD is satisfying_(OP) )

proof end;

cluster I_GG -> satisfying_(NP) satisfying_(EP) satisfying_(IP) satisfying_(OP) ;

coherence
( I_GG is satisfying_(NP) & I_GG is satisfying_(EP) & I_GG is satisfying_(IP) & I_GG is satisfying_(OP) )

proof end;

cluster I_RS -> non satisfying_(NP) non satisfying_(EP) satisfying_(IP) satisfying_(OP) ;

coherence
( not I_RS is satisfying_(NP) & not I_RS is satisfying_(EP) & I_RS is satisfying_(IP) & I_RS is satisfying_(OP) )

proof end;

cluster I_YG -> satisfying_(NP) satisfying_(EP) non satisfying_(IP) non satisfying_(OP) ;

coherence
( I_YG is satisfying_(NP) & I_YG is satisfying_(EP) & not I_YG is satisfying_(IP) & not I_YG is satisfying_(OP) )

proof end;

cluster I_WB -> satisfying_(NP) satisfying_(EP) satisfying_(IP) non satisfying_(OP) ;

coherence
( I_WB is satisfying_(NP) & I_WB is satisfying_(EP) & I_WB is satisfying_(IP) & not I_WB is satisfying_(OP) )

proof end;

cluster I_FD -> satisfying_(NP) satisfying_(EP) satisfying_(IP) satisfying_(OP) ;

coherence
( I_FD is satisfying_(NP) & I_FD is satisfying_(EP) & I_FD is satisfying_(IP) & I_FD is satisfying_(OP) )

proof end;

end;

registration

cluster I_{0} -> non satisfying_(NP) satisfying_(EP) non satisfying_(IP) non satisfying_(OP) ;

coherence
( not I_{0} is satisfying_(NP) & I_{0} is satisfying_(EP) & not I_{0} is satisfying_(IP) & not I_{0} is satisfying_(OP) )

proof end;

cluster I_{1} -> non satisfying_(NP) satisfying_(EP) satisfying_(IP) non satisfying_(OP) ;

coherence
( not I_{1} is satisfying_(NP) & I_{1} is satisfying_(EP) & I_{1} is satisfying_(IP) & not I_{1} is satisfying_(OP) )

proof end;

end;