Constructing Examples of Fuzzy Implications within the Mizar Mathematical Library Adam Grabowski Institute of Informatics, University of Białystok Ciołkowskiego 1M, 15-245 Białystok, Poland adam@math.uwb.edu.pl Abstract The aim of our work is to show, by means of the Mizar system, how we can cope with the formalization of fundamental properties of fuzzy implications; we construct basic nine examples of these operators. This is the continuation of the formal approach to fuzzy sets within the Mizar Mathematical Library, with fuzzy numbers, fuzzy relations, triangular norms and conorms as building blocks of the theory. 1 Introduction Fuzzy sets [Zad65] is a well-known approach to incomplete or imprecise data, similar in some sense to Pawlak’s rough sets [GM15]; the definition of the notion of fuzziness allows for quite natural description in terms of ordinary set theory used by mathematicians and computer scientists. As contemporary mathematics uses more and more methods of computer verification of theorems and discovering their proofs, it is not very strange that also in this area we could observe growing usage of automated proof-assistants. We report on the progress of the development of the already well-established framework of fuzzy set theory within one of popular repositories of computerized mathematical knowledge – the Mizar Mathematical Library [BBG+ 18]. Even if the original formal background was created some ten years ago, and during that time it was thoroughly redesigned in order to increase its expressive power and to follow the evolution of the underlying proof language, we see the need for further modifications. In this work, we describe the recent continuation of the formalization of fuzzy logic – proving properties of fuzzy implications. We illustrate our development by examples taken from fully verified Mizar code. 2 Fuzzy Implications As it is well known, the implication operator plays a crucial role in the classical two-valued logic. Based on this logical connective, we can define the unary negation operator, and also the binary conjunction and disjunction. In the field of fuzzy logic, the notions of t-norm and t-conorm are an abstraction of classical connectives: conjunction and disjunction, respectively [Haj98]. Similarly, we can treat the notion of a fuzzy implication as a generalization of a classical implication. On the other hand, based on abstract properties, fuzzy implication can be defined as the real function which satisfies a set of axioms. The unified axiomatization was proposed by [BacJar08] and we follow closely this book. Copyright © by the paper’s authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0). In: C. Kaliszyk, E. Brady, J. Davenport, W.M. Farmer, A. Kohlhase, M. Kohlhase, D. Müller, K. Pąk, and C. Sacerdoti Coen (eds.): Joint Proceedings of the FMM and LML Workshops, Doctoral Program and Work in Progress at the Conference on Intelligent Computer Mathematics 2019 co-located with the 12th Conference on Intelligent Computer Mathematics (CICM 2019), Prague, Czech Republic, July 8–12, 2019, published at http://ceur-ws.org A function I : [0, 1]2 → [0, 1] is called a fuzzy implication if it satisfies, for all x, x1 , x2 , y1 , y2 ∈ [0, 1], the following conditions: if x1 ≤ x2 , then I(x1 , y) ≥ I(x2 , y), (I1) if y1 ≤ y2 , then I(x, y1 ) ≤ I(x, y2 ), (I2) I(0, 0) = 1, (I3) I(1, 1) = 1, (I4) I(1, 0) = 0. (I5) In the set of all fuzzy implications, denoted by FI, we have I0 and I1 as the least and the greatest elements (with the ordinary pointwise ordering of functions) defined for arbitrary x, y ∈ [0, 1] as 1, if x = 0 or y = 1  I0 (x, y) = 0, otherwise 1, if x < 1 or y > 0  I1 (x, y) = 0, otherwise Table 1: Nine basic fuzzy implications ([BacJar08], p. 4) Name Defining formula Łukasiewicz ILK (x, y) =min(1, 1 − x + y) 1, if x ≤ y Gödel IGD (x, y) = y, otherwise Reichenbach IRC (x, y) = 1 − x + xy Kleene-Dienes IKD (x, y) = max(1 − x, y) 1, if x ≤ y Goguen IGG (x, y) = y  x , otherwise 1, if x ≤ y Rescher IRS (x, y) = 0, if x > y if x = 0 and y = 0  1, Yager IYG (x, y) = y x ,  if x > 0 or y > 0 1, if x < 1 Weber IWB (x, y) = y, if x = 1 if x ≤ y  1, Fodor IFD (x, y) = max(1 − x, y), if x > y Four properties (together with the continuity) are considered very important in the theory: • (NP) – the left neutrality property (∀y∈[0,1] I(1, y) = y), • (EP) – the exchange principle (∀x,y,z∈[0,1] I(x, I(y, z)) = I(y, I(x, z))), • (IP) – the identity principle (∀x∈[0,1] I(x, x) = 1), • (OP) – the ordering property (∀x,y∈[0,1] I(x, y) = 1 ⇔ x ≤ y). Our idea was to put these into a formal framework. 3 The Formal Approach We assume some basic familiarity with the Mizar syntax [Gra15]. The fuzzy set theory was introduced in the Mizar Mathematical Library [BBG+ 18] rather early: in [MES01] fuzzy sets were defined as the corresponding membership functions of the form of [.0,1.]-valued Function of C, REAL, where C is a non-empty universe. This path was explored up to the definition and basic properties of fuzzy numbers [Gra13]. It is worth mentioning that, together with rough sets [GM15], these formalized frameworks are not only interesting extensions of the ordinary set theory, but offer also efficient tool for the reasoning under incomplete or inconsistent information. An interesting and simple example of the object showing this interconnections between all three is the classical characteristic function χ, defined formally in Mizar as follows: definition let A,X be set; func chi(A,X) -> Function means :: FUNCT_3:def 3 dom it = X & for x being object st x in X holds (x in A implies it.x = 1) & (not x in A implies it.x = 0); end; Obviously, chi(C,C) for non-empty universe C can be treated as a fuzzy membership function; for a discrete approximation space (that is, its indiscernibility relation is the identity relation, or, in other words, only identical objects are indiscernible), it is equal to the rough membership function MemberFunc. Such an approach makes basic operations on fuzzy sets just the modified operations of min and max on functions taken componentwise. Similarly, our properties under consideration were defined in the form of Mizar adjectives of the binary operation on the unit interval (BinOp of [.0,1.]). The functions satisfying equations (I3), (I4), and (I5) are called in our formalism, 00-dominant, 11-dominant, and 10-weak, respectively. They express the ordinary properties of the classical two-valued implication. definition let f be BinOp of [.0,1.]; attr f is 00-dominant means :: FUZIMPL1:def 3 f.(0,0) = 1; end; Additional technical synonyms in the form of satisfying_(I3) were also added, just for easier remembering. The properties (I1) and (I2) – decreasing_on_1st and increasing_on_2nd, can be of a little bit more general interest. Having defined all five characteristic attributes, we can defined a new type, Fuzzy_Implication, in the following manner: definition mode Fuzzy_Implication is decreasing_on_1st increasing_on_2nd 00-dominant 11-dominant 10-weak BinOp of [.0,1.]; end; Still however, in all places where it is possible, we formulated lemmas under the assumptions as general as we could (or, equivalently, with the least number of attributes). In order to cope with basic constructions present in the theory of fuzzy connectives, we had to define a number of examples of binary connectives. It is especially important to have some, because taking into account the expressive power of registrations of clusters in the Mizar system and the role of attributes, most of theorems are stated in the form of the abovementioned registrations. Having prepared such formal background, properties can be calculated automatically via the mechanism of the type expansion. Main aim of the Mizar article was to introduce formally nine important examples of fuzzy implications (see Table 1) and to characterize them in terms of four elementary properties [SM87]. We prepared an automatic counterpart for Table 2, which is actually the part of [BacJar08] (Table 1.4, p. 10), as the combination of cluster registrations in the Mizar article with MML identifier FUZIMPL2 [Gra18]. All nine implications were defined along the standard lines and proven to satisfy (I1) – (I5) in [Gra17b]. The mutual independence of the axioms was shown using five special operators – each one violating exactly one among properties (I1) – (I5) [Gra17b]. For example, ILK and IRS can be characterized as follows (the proofs are not quoted): registration cluster I_LK -> satisfying_(NP) satisfying_(EP) satisfying_(IP) satisfying_(OP); cluster I_RS -> non satisfying_(NP) non satisfying_(EP) satisfying_(IP) satisfying_(OP); end; Table 2: The properties of introduced fuzzy implications Fuzzy implication (NP) (EP) (IP) (OP) ILK + + + + IGD + + + + IRC + + − − IKD + + − − IGG + + + + IRS − − + + IYG + + − − IWB + + + − IFD + + + + In order both to simplify proofs and to make the net of interconnections among these properties more coherent, we added some more conditional registrations, for example stating that properties (EP) and (OP) together imply (I1), (I5), and (NP): registration cluster satisfying_(EP) satisfying_(OP) -> satisfying_(I1) satisfying_(I5) satisfying_(NP) for BinOp of [.0,1.]; end; After that, if one tries to formulate the existential registration of a cluster: registration cluster non satisfying_(NP) satisfying_(EP) satisfying_(IP) satisfying_(OP) for BinOp of [.0,1.]; end; the Mizar verifier will report an error “#95 Inconsistent cluster". At the moment, we were not focused on the continuity property of the implications; even if such property was studied extensively during the formalization of real function analysis, we had some type compatibility problems. In order to reuse the approach developed in the MML, starting with [RS90], we should either go through the type casting, or redesign the existing machinery to make it more general. The proofs of properties of the Yager implication (involving properties of exponential function) were a little bit too complex, just due to the lack of necessary lemmas (especially, the continuity at the endpoints of intervals can be a potential problem as the value of a function at the point outside its domain is zero). 4 Conclusions Together with the formal description of triangular norms and conorms (described in [Gra17a] and [GM18]) in- troducing fuzzy implications is a fundamental step towards defining fuzzy logic within the Mizar Mathematical Library. Some of the well-known examples of such connectives are of much more general interest, for example Łukasiewicz implication (1923) is essential for many-valued logics; it was studied years before Zadeh and his in- vention of fuzzy sets. The implication of Gödel was explored within the intuitionistic logic (1932). Furthermore, the formalization of the textbook on fuzzy implications [BacJar08] could be another interesting challenge. It is even more challenging to show how this fuzzy approach can generalize the existing formalization of classical predicate logic in Mizar [RT90]. Formal proofs of the independence of axioms are not widely present in Mizar for- malizations as it is usually connected with the construction of models which are outside of the core formalization. This is a more general observation that MML lacks many standard mathematical examples (and sometimes they are hidden in the proofs of existential registrations of clusters). Some of them, as the independence of parallel postulate in Tarski’s geometry (as started in [RGA14]) are just very labour-intensive in its formal version. References [BacJar08] Michał Baczyński and Balasubramaniam Jayaram: Fuzzy Implications, Springer (2008). doi: 10.1007/978-3-540-69082-5 [BBG+ 15] Grzegorz Bancerek, Czesław Byliński, Adam Grabowski, Artur Korniłowicz, Roman Matuszewski, Adam Naumowicz, Karol Pa̧k, and Josef Urban: Mizar: State-of-the-art and beyond. In Kerber, M. et al. (Eds.): Conference on Intelligent Computer Mathematics, CICM 2015, Lecture Notes in Computer Science, 9150, Springer, pp. 261–279 (2015). doi: 10.1007/978-3-319-20615-8_17 [BBG+ 18] Grzegorz Bancerek, Czesław Byliński, Adam Grabowski, Artur Korniłowicz, Roman Matuszewski, Adam Naumowicz, and Karol Pa̧k: The role of the Mizar Mathematical Library for interac- tive proof development in Mizar, Journal of Automated Reasoning, 61(1), pp. 9–32 (2018). doi: 10.1007/s10817-017-9440-6 [DubPra97] Didier Dubois and Henri Prade: Fuzzy Sets and Systems: Theory and Applications, Academic Press, Orlando (1997) [Gra13] Adam Grabowski: On the computer certification of fuzzy numbers. In Ganzha, M., Maciaszek, L., and Paprzycki, M. (Eds.): Proceedings of the 2013 Federated Conference on Computer Science and Information Systems (FedCSIS), pp. 51–54 (2013) [Gra17a] Adam Grabowski: Basic formal properties of triangular norms and conorms, Formalized Mathemat- ics, 25(2), pp. 93–102 (2017). doi: 10.1515/forma-2017-0009 [Gra17b] Adam Grabowski: Formal introduction to fuzzy implications, Formalized Mathematics, 25(3), pp. 241–248 (2017). doi: 10.1515/forma-2017-0023 [Gra18] Adam Grabowski: Fundamental properties of fuzzy implications, Formalized Mathematics, 26(4), pp. 271–276 (2018). doi: 10.2478/forma-2018-0023 [GM15] Adam Grabowski and Takashi Mitsuishi: Initial comparison of formal approaches to fuzzy and rough sets, Artificial Intelligence and Soft Computing, ICAISC 2015, Lecture Notes in Artificial Intelligence, 9119, pp. 160–171 (2015). doi: 10.1007/978-3-319-19324-3_15 [GM18] Adam Grabowski and Takashi Mitsuishi: Extending formal fuzzy sets with triangular norms and conorms, Proceedings of EUSFLAT 2017, Advances in Intelligent Systems and Computing, vol. 642, pp. 176–187 (2018). doi: 10.1007/978-3-319-66824-6_16 [Gra15] Adam Grabowski, Artur Korniłowicz, and Adam Naumowicz: Four decades of Mizar, Journal of Automated Reasoning, 55(3), pp. 191–198 (2015). doi: 10.1007/s10817-015-9345-1 [Haj98] Petr Hajek: Metamathematics of Fuzzy Logic, Kluwer (1998), doi: 10.1007/978-94-011-5300-3 [MES01] Takashi Mitsuishi, Noboru Endou, and Yasunari Shidama: The concept of fuzzy set and membership function and basic properties of fuzzy set operation, Formalized Mathematics, 9(2), pp. 351–356 (2001) [RS90] Konrad Raczkowski and Paweł Sadowski: Real function continuity, Formalized Mathematics, 1(4), pp. 787–791 (1990). [RGA14] William Richter, Adam Grabowski, and Jesse Alama: Tarski Geometry axioms, Formalized Math- ematics, 22(2), pp. 167–176 (2014). doi: 10.2478/forma-2014-0017 [RT90] Piotr Rudnicki and Andrzej Trybulec: A first order language, Formalized Mathematics, 1(2), pp. 303–311 (1990). [SM87] Philippe Smets and Paul Magrez: Implication in fuzzy logic, International Journal of Approximate Reasoning, 1(4), pp. 327–347 (1987). doi: 10.1016/0888-613X(87)90023-5 [Zad65] Lotfi Zadeh: Fuzzy sets, Information and Control, 8(3), pp. 338–353 (1965). doi: 10.1016/S0019- 9958(65)90241-X