The article continues the formalization of the lattice theory (as structures with two binary operations, not in terms of ordering relations). In the Mizar Mathematical Library, there are some attempts to formalize prime ideals and filters; one series of articles written as decoding  proven some results; we tried however to follow , , and . All three were devoted to the Stone representation theorem  for Boolean or Heyting lattices. The main aim of the present article was to bridge this gap between general distributive lattices and Boolean algebras, having in mind that the more general approach will eventually replace the common proof of aforementioned articles.1
Because in Boolean algebras the notions of ultrafilters, prime filters and maximal filters coincide, we decided to construct some concrete examples of ultrafilters in nontrivial Boolean lattice. We proved also the Prime Ideal Theorem not as BPI (Boolean Prime Ideal), but in the more general setting.
In the final section we present Nachbin theorems , expressed both in terms of maximal and prime filters and as the unordered spectra of a lattice , . This shows that if the notion of maximal and prime filters coincide in the lattice, it is Boolean.
The notion of a rough set, developed by Pawlak , is an important tool to describe situation of incomplete or partially unknown information. In this article, which is essentially the continuation of , we try to give the characterization of approximation operators in terms of ordinary properties of underlying relations (some of them, as serial and mediate relations, were not available in the Mizar Mathematical Library). Here we drop the classical equivalence- and tolerance-based models of rough sets  trying to formalize some parts of  following also  in some sense (Propositions 1-8, Corr. 1 and 2; the complete description is available in the Mizar script). Our main problem was that informally, there is a direct correspondence between relations and underlying properties, in our approach however , which uses relational structures rather than relations, we had to switch between classical (based on pure set theory) and abstract (using the notion of a structure) parts of the Mizar Mathematical Library. Our next step will be translation of these properties into the pure language of Mizar attributes.
In the article the formal characterization of triangular numbers (famous from  and words “EYPHKA! num = Δ+Δ+Δ”)  is given. Our primary aim was to formalize one of the items (#42) from Wiedijk’s Top 100 Mathematical Theorems list , namely that the sequence of sums of reciprocals of triangular numbers converges to 2. This Mizar representation was written in 2007. As the Mizar language evolved and attributes with arguments were implemented, we decided to extend these lines and we characterized polygonal numbers. We formalized centered polygonal numbers, the connection between triangular and square numbers, and also some equalities involving Mersenne primes and perfect numbers. We gave also explicit formula to obtain from the polygonal number its ordinal index. Also selected congruences modulo 10 were enumerated. Our work basically covers the Wikipedia item for triangular numbers and the Online Encyclopedia of Integer Sequences (http://oeis.org/A000217). An interesting related result  could be the proof of Lagrange’s four-square theorem or Fermat’s polygonal number theorem .
In the article the formal characterization of square-free numbers is shown; in this manner the paper is the continuation of . Essentially, we prepared some lemmas for convenient work with numbers (including the proof that the sequence of prime reciprocals diverges ) according to  which were absent in the Mizar Mathematical Library. Some of them were expressed in terms of clusters’ registrations, enabling automatization machinery available in the Mizar system. Our main result of the article is in the final section; we proved that the lattice of positive divisors of a positive integer n is Boolean if and only if n is square-free.
We continue in the Mizar system  the formalization of fuzzy implications according to the book of Baczyński and Jayaram “Fuzzy Implications” . In this article we define fuzzy negations and show their connections with previously defined fuzzy implications  and  and triangular norms and conorms . This can be seen as a step towards building a formal framework of fuzzy connectives . We introduce formally Sugeno negation, boundary negations and show how these operators are pointwise ordered. This work is a continuation of the development of fuzzy sets ,  in Mizar  started in  and partially described in . This submission can be treated also as a part of a formal comparison of fuzzy and rough approaches to incomplete or uncertain information within the Mizar Mathematical Library .
We continue the formal development of rough inclusion functions (RIFs), continuing the research on the formalization of rough sets  – a well-known tool of modelling of incomplete or partially unknown information. In this article we give the formal characterization of complementary RIFs, following a paper by Gomolińska . We expand this framework introducing Jaccard index, Steinhaus generate metric, and Marczewski-Steinhaus metric space . This is the continuation of ; additionally we implement also parts of , , and the details of this work can be found in .
In this article, we continue the development of the theory of fuzzy sets , started with  with the future aim to provide the formalization of fuzzy numbers  in terms reflecting the current state of the Mizar Mathematical Library. Note that in order to have more usable approach in , we revised that article as well; some of the ideas were described in . As we can actually understand fuzzy sets just as their membership functions (via the equality of membership function and their set-theoretic counterpart), all the calculations are much simpler. To test our newly proposed approach, we give the notions of (normal) triangular and trapezoidal fuzzy sets as the examples of concrete fuzzy objects. Also -cuts, the core of a fuzzy set, and normalized fuzzy sets were defined. Main technical obstacle was to prove continuity of the glued maps, and in fact we did this not through its topological counterpart, but extensively reusing properties of the real line (with loss of generality of the approach, though), because we aim at formalizing fuzzy numbers in our future submissions, as well as merging with rough set approach as introduced in  and . Our base for formalization was  and .
In the article we present in the Mizar system the catalogue of nine basic fuzzy implications, used especially in the theory of fuzzy sets. This work is a continuation of the development of fuzzy sets in Mizar; it could be used to give a variety of more general operations, and also it could be a good starting point towards the formalization of fuzzy logic (together with t-norms and t-conorms, formalized previously).
In the article we present in the Mizar system ,  the catalogue of triangular norms and conorms, used especially in the theory of fuzzy sets . The name triangular emphasizes the fact that in the framework of probabilistic metric spaces they generalize triangle inequality .
After defining corresponding Mizar mode using four attributes, we introduced the following t-norms:
minimum t-norm minnorm (Def. 6),
product t-norm prodnorm (Def. 8),
Łukasiewicz t-norm Lukasiewicz_norm (Def. 10),
drastic t-norm drastic_norm (Def. 11),
nilpotent minimum nilmin_norm (Def. 12),
Hamacher product Hamacher_norm (Def. 13),
and corresponding t-conorms:
maximum t-conorm maxnorm (Def. 7),
probabilistic sum probsum_conorm (Def. 9),
bounded sum BoundedSum_conorm (Def. 19),
drastic t-conorm drastic_conorm (Def. 14),
nilpotent maximum nilmax_conorm (Def. 18),
Hamacher t-conorm Hamacher_conorm (Def. 17).
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).
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 , .
In the article we continue in the Mizar system ,  the formalization of fuzzy implications according to the monograph of Baczyński and Jayaram “Fuzzy Implications” . We develop a framework of Mizar attributes allowing us for a smooth proving of basic properties of these fuzzy connectives . We also give a set of theorems about the ordering of nine fundamental implications: Łukasiewicz (ILK), Gödel (IGD), Reichenbach (IRC), Kleene-Dienes (IKD), Goguen (IGG), Rescher (IRS), Yager (IYG), Weber (IWB), and Fodor (IFD).
This work is a continuation of the development of fuzzy sets in Mizar ; it could be used to give a variety of more general operations on fuzzy sets . The formalization follows , , and .