Generalized Fuzzy Subalgebra Of Boolean Algebra And The Realization Of It In Mizar System

Based on the existing results of fuzzy subalgebra of Boolean algebra, the(∈,∈q)-Fuzzy subalgebra, fuzzy subalgebra with thresholds and direct product offuzzy subalgebra of Boolean algebra are discussed in this paper, which develop thebasic theorems of the fuzzy algebra system. And the Mizar definitions of the fuzzysubalgebra and (∈,∈∨q)-Fuzzy subalgebra and some important properties of themare realized in Mizar system, which enrich the content of Mizar Mathematical Library.The main results of this paper are listed as follows.1. The concept of (∈,∈∨q)-Fuzzy subalgebra and (∈,∈∨q)-Fuzzy idealof Boolean algebra and (∈,∈∨q)-Fuzzy quotient Boolean algebra are introduced byusing the 'belongs to' relation (∈) and 'quasi-coincident with' relation (q) between afuzzy point x_λand a fuzzy subalgebra R. A necessary and sufficient condition for afuzzy set of Boolean algebra to be a (∈,∈∑q)-Fuzzy sbualgebra is stated, and imagesand inverse-images of (∈,∈∨q)-Fuzzy subalgebra of Boolean algebra under Booleanalgebra homomorphism are studied, and R/I is Boolean algebra when I is(∈,∈∨q)-Fuzzy real ideal of Boolean algebra R are proved.2. Based on the existing results of fuzzy subalgebra and (∈,∈∨q)-Fuzzysubalgebra of Boolean algebra, the concept of fuzzy subalgebra with thresholds of Boolean algebra is introduced, and some relevant properties and the relation of thesefuzzy subalgebras are discussed.3. Some properties of the direct product of fuzzy subalgebra of Boolean algebraare discussed, and the sufficient and necessary condition which fuzzy subalgebra ofdirect product Boolean algebra can be decomposed as direct product of two fuzzysubalgebras are obtained. Then the direct product structure of fuzzy quotient Booleanalgebra is discussed.4. The Mizar definitions of fuzzy subalgebra and (∈,∈∨q) -Fuzzy subalgebra ofBoolean algebra are introduced in the Mizar system, and some relevant importantconclusions and theorems of them are written, and all of them have been checked byMizar system. So these fuzzy subalgebras of Boolean algebra are realized in Mizarsystem.