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