Basic Formal Properties of Triangular Norms and Conorms

In the article we present in the Mizar system [1], [8] the catalogue of triangular norms and conorms, used especially in the theory of fuzzy sets [13]. The name triangular emphasizes the fact that in the framework of probabilistic metric spaces they generalize triangle inequality [2].

After defining corresponding Mizar mode using four attributes, we introduced the following t-norms:and corresponding t-conorms:

minimum t-norm(Def. 6), minnorm

product t-norm(Def. 8), prodnorm

Łukasiewicz t-norm(Def. 10), Lukasiewicz_norm

drastic t-norm(Def. 11), drastic_norm

nilpotent minimum(Def. 12), nilmin_norm

Hamacher product(Def. 13), Hamacher_norm

maximum t-conorm(Def. 7), maxnorm

probabilistic sum(Def. 9), probsum_conorm

bounded sum(Def. 19), BoundedSum_conorm

drastic t-conorm(Def. 14), drastic_conorm

nilpotent maximum(Def. 18), nilmax_conorm

Hamacher t-conorm(Def. 17). Hamacher_conorm

Their basic properties and duality are shown; we also proved the predicate of the ordering of norms [], []. It was proven formally that drastic-norm is the pointwise smallest t-norm and minnorm is the pointwise largest t-norm (maxnorm is the pointwise smallest t-conorm and drastic-conorm is the pointwise largest t-conorm). 10 9

This work is a continuation of the development of fuzzy sets in Mizar [] started in [] and []; it could be used to give a variety of more general operations on fuzzy sets. Our formalization is much closer to the set theory used within the Mizar Mathematical Library than the development of rough sets [], the approach which was chosen allows however for merging both theories [], []. 6 11 3 4 5 7