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.
Copyright © by the paper’s authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0).
A function I : [0; 1]2 ! [0; 1] is called a fuzzy implication if it satisfies, for all x; x1; x2; y1; y2 2 [0; 1]; the following conditions:
In the set of all fuzzy implications, denoted by F I; we have I0 and I1 as the least and the greatest elements (with the ordinary pointwise ordering of functions) defined for arbitrary x; y 2 [0; 1] as (I1) (I2) (I3) (I4) (I5) • (NP) – the left neutrality property (8y2[0;1]I(1; y) = y), • (EP) – the exchange principle (8x;y;z2[0;1]I(x; I(y; z)) = I(y; I(x; z))), • (IP) – the identity principle (8x2[0;1]I(x; x) = 1), • (OP) – the ordering property (8x;y2[0;1]I(x; y) = 1 , x y).
Our idea was to put these into a formal framework. 3
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);
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;
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.];
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.]; 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
Together with the formal description of triangular norms and conorms (described in [Gra17a] and [GM18]) introducing 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 invention 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 formalizations 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. 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 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 interactive 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) [BBG+15] [BBG+18]
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) Adam Grabowski: Basic formal properties of triangular norms and conorms, Formalized Mathematics, 25(2), pp. 93–102 (2017). doi: 10.1515/forma-2017-0009 Adam Grabowski: Formal introduction to fuzzy implications, Formalized Mathematics, 25(3), pp. 241–248 (2017). doi: 10.1515/forma-2017-0023 Adam Grabowski: Fundamental properties of fuzzy implications, Formalized Mathematics, 26(4), pp. 271–276 (2018). doi: 10.2478/forma-2018-0023 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 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 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) Konrad Raczkowski and Paweł Sadowski: Real function continuity, Formalized Mathematics, 1(4), pp. 787–791 (1990).
William Richter, Adam Grabowski, and Jesse Alama: Tarski Geometry axioms, Formalized Mathematics, 22(2), pp. 167–176 (2014). doi: 10.2478/forma-2014-0017