Fundamental Properties of Fuzzy Implications

In the article we continue in the Mizar system [8], [2] the formalization of fuzzy implications according to the monograph of Baczyński and Jayaram “Fuzzy Implications” [1]. We develop a framework of Mizar attributes allowing us for a smooth proving of basic properties of these fuzzy connectives [9]. We also give a set of theorems about the ordering of nine fundamental implications: Łukasiewicz (I_LK), Gödel (I_GD), Reichenbach (I_RC), Kleene-Dienes (I_KD), Goguen (I_GG), Rescher (I_RS), Yager (I_YG), Weber (I_WB), and Fodor (I_FD).

This work is a continuation of the development of fuzzy sets in Mizar [6]; it could be used to give a variety of more general operations on fuzzy sets [13]. The formalization follows [10], [5], and [4].