:: Formal Introduction to Fuzzy Implications
:: by Adam Grabowski
::
:: Received September 3, 2017
:: Copyright (c) 2017-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 NUMBERS, XXREAL_1, REAL_1, XXREAL_0, FUZIMPL1, SUBSET_1, CARD_1,
ARYTM_1, ARYTM_3, POWER, FUNCT_1, RELAT_1, FUNCT_7, ZFMISC_1, BINOP_1;
notations TARSKI, SUBSET_1, ORDINAL1, XCMPLX_0, XXREAL_0, ZFMISC_1, BINOP_1,
XREAL_0, POWER, FUNCT_1, RELSET_1, FUNCT_2, RCOMP_1, FUZNORM1;
constructors REAL_1, SEQ_4, TOPMETR, PREPOWER, POWER, FUZNORM1;
registrations XBOOLE_0, RELSET_1, XXREAL_0, XREAL_0, MEMBERED, ORDINAL1,
FUZNORM1;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
begin :: Preliminaries
theorem :: FUZIMPL1:1
for a,b being Element of [.0,1.] holds
max (b, min (1-a,1-b)) in [.0,1.];
theorem :: FUZIMPL1:2
for a,b being Element of [.0,1.] holds
min (1,1-a+b) in [.0,1.];
theorem :: FUZIMPL1:3
for a,b being Element of [.0,1.] holds
1 - a + a * b in [.0,1.];
theorem :: FUZIMPL1:4
for a,b being Element of [.0,1.] holds
max(1-a,b) in [.0,1.];
theorem :: FUZIMPL1:5
for a,b being Element of [.0,1.] st a > 0 or b > 0 holds
b to_power a in [.0,1.];
theorem :: FUZIMPL1:6
for a,b being Element of [.0,1.] st a > b holds
b / a in [.0,1.];
begin :: Basic Attributes Defining Fuzzy Implications
definition let f be BinOp of [.0,1.];
attr f is decreasing_on_1st means
:: 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
:: 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
:: FUZIMPL1:def 3
f.(0,0) = 1;
attr f is 11-dominant means
:: FUZIMPL1:def 4
f.(1,1) = 1;
attr f is 10-weak means
:: FUZIMPL1:def 5
f.(1,0) = 0;
attr f is 01-dominant means
:: FUZIMPL1:def 6
f.(0,1) = 1;
end;
:: 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 increasing_on_2nd
00-dominant 11-dominant 10-weak;
attr f is with_properties_of_classical_implication means
:: FUZIMPL1:def 8
f is 00-dominant 01-dominant 11-dominant 10-weak;
end;
begin :: Examples Showing Independence of Axioms
definition
func I_{-1} -> BinOp of [.0,1.] means
:: FUZIMPL1:def 9
for x,y being Element of [.0,1.] holds
it.(x,y) = max (1-x,min(x,y));
end;
registration
cluster I_{-1} -> :::non decreasing_on_1st
increasing_on_2nd 00-dominant 11-dominant 10-weak;
end;
definition
func I_{-2} -> BinOp of [.0,1.] means
:: FUZIMPL1:def 10
for x,y being Element of [.0,1.] holds
it.(x,y) = max (y, min (1-x,1-y));
end;
registration
cluster I_{-2} -> decreasing_on_1st :::non increasing_on_2nd
00-dominant 11-dominant 10-weak;
end;
definition
func I_{-3} -> BinOp of [.0,1.] means
:: 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);
end;
registration
cluster I_{-3} -> decreasing_on_1st increasing_on_2nd
non 00-dominant 11-dominant 10-weak;
end;
definition
func I_{-4} -> BinOp of [.0,1.] means
:: 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);
end;
registration
cluster I_{-4} -> decreasing_on_1st increasing_on_2nd
00-dominant non 11-dominant 10-weak;
end;
definition
func I_{-5} -> BinOp of [.0,1.] means
:: FUZIMPL1:def 13
for x,y being Element of [.0,1.] holds
it.(x,y) = 1;
end;
registration
cluster I_{-5} -> decreasing_on_1st increasing_on_2nd
00-dominant 11-dominant non 10-weak;
end;
begin :: Catalogue of Fuzzy Implications
definition
func Lukasiewicz_implication -> BinOp of [.0,1.] means
:: FUZIMPL1:def 14
for x,y being Element of [.0,1.] holds
it.(x,y) = min (1,1-x+y);
end;
registration
cluster Lukasiewicz_implication ->
decreasing_on_1st increasing_on_2nd 00-dominant 11-dominant 10-weak;
end;
registration
cluster with_properties_of_fuzzy_implication for BinOp of [.0,1.];
end;
registration
cluster with_properties_of_fuzzy_implication ->
decreasing_on_1st increasing_on_2nd 00-dominant
11-dominant 10-weak for BinOp of [.0,1.];
cluster decreasing_on_1st increasing_on_2nd 00-dominant 01-dominant
11-dominant 10-weak -> with_properties_of_fuzzy_implication
for BinOp of [.0,1.];
cluster with_properties_of_classical_implication ->
00-dominant 01-dominant 11-dominant 10-weak for BinOp of [.0,1.];
cluster 00-dominant 01-dominant 11-dominant 10-weak ->
with_properties_of_classical_implication for BinOp of [.0,1.];
cluster with_properties_of_fuzzy_implication ->
with_properties_of_classical_implication for BinOp of [.0,1.];
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
the set of all f where f is Fuzzy_Implication;
end;
definition
func Goedel_implication -> BinOp of [.0,1.] means
:: 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);
end;
registration
cluster Goedel_implication -> decreasing_on_1st increasing_on_2nd
00-dominant 11-dominant 10-weak;
end;
definition
func Reichenbach_implication -> BinOp of [.0,1.] means
:: FUZIMPL1:def 17
for x,y being Element of [.0,1.] holds
it.(x,y) = 1 - x + x * y;
end;
registration
cluster Reichenbach_implication -> decreasing_on_1st increasing_on_2nd
00-dominant 11-dominant 10-weak;
end;
definition
func Kleene-Dienes_implication -> BinOp of [.0,1.] means
:: FUZIMPL1:def 18
for x,y being Element of [.0,1.] holds
it.(x,y) = max (1 - x, y);
end;
registration
cluster Kleene-Dienes_implication -> decreasing_on_1st increasing_on_2nd
00-dominant 11-dominant 10-weak;
end;
definition
func Goguen_implication -> BinOp of [.0,1.] means
:: 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);
end;
registration
cluster Goguen_implication -> decreasing_on_1st increasing_on_2nd
00-dominant 11-dominant 10-weak;
end;
definition
func Rescher_implication -> BinOp of [.0,1.] means
:: 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);
end;
registration
cluster Rescher_implication -> decreasing_on_1st increasing_on_2nd
00-dominant 11-dominant 10-weak;
end;
definition
func Yager_implication -> BinOp of [.0,1.] means
:: FUZIMPL1:def 21
for x,y being Element of [.0,1.] holds
(x = y = 0 implies it.(x,y) = 1) &
(x > 0 or y > 0 implies it.(x,y) = y to_power x);
end;
registration
cluster Yager_implication -> decreasing_on_1st increasing_on_2nd
00-dominant 11-dominant 10-weak;
end;
definition
func Weber_implication -> BinOp of [.0,1.] means
:: 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);
end;
registration
cluster Weber_implication -> decreasing_on_1st increasing_on_2nd
00-dominant 11-dominant 10-weak;
end;
definition
func Fodor_implication -> BinOp of [.0,1.] means
:: 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));
end;
registration
cluster Fodor_implication -> decreasing_on_1st increasing_on_2nd
00-dominant 11-dominant 10-weak;
end;
begin :: Boundary Fuzzy Implications
definition
func I_{0} -> BinOp of [.0,1.] means
:: 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);
end;
registration
cluster I_{0} -> decreasing_on_1st increasing_on_2nd
00-dominant 11-dominant 10-weak;
end;
definition
func I_{1} -> BinOp of [.0,1.] means
:: 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);
end;
registration
cluster I_{1} -> decreasing_on_1st increasing_on_2nd
00-dominant 11-dominant 10-weak;
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;
theorem :: FUZIMPL1:7
for fi being Fuzzy_Implication,
y being Element of [.0,1.] holds
fi.(0,y) = 1;
theorem :: FUZIMPL1:8
for fi being Fuzzy_Implication,
x being Element of [.0,1.] holds
fi.(x,1) = 1;
registration
cluster -> satisfying_(LB) satisfying_(RB) for Fuzzy_Implication;
end;
theorem :: FUZIMPL1:9
for fi being Fuzzy_Implication holds
I_{0} <= fi;
theorem :: FUZIMPL1:10
for fi being Fuzzy_Implication holds
fi <= I_{1};