The Research On Logic And Algebraic Systems Based On Fuzzy Type Theory

Type theory is a higher order logic and the fuzzification of type theory is a fuzzy type theory.Therefore,the fuzzy type theory is the higher order fuzzy logic.EQ-algebras providing a more general truth-valued algebraic structures for the fuzzy type theory are also the truth-valued algebraic structures corresponding to the higher order fuzzy logic.In this thesis,the logical and algebraic systems based on the fuzzy type theory were studied including the theory of radicals of prefilters in EQ-algebras,the monadic EQ-algebras and its corresponding logic systems,and the equality propo-sitional logic and its extensions.The research results and innovations were briefly summarized as follows.1.We used the algebraic methods to deal with provable formula sets of fuzzy type theory.First,the definition of radicals of prefilters in EQ-algebras was introduced,namely the intersection of all maximal prefilters which contain prefilter F,that was denoted as Rad(F).Also,Rad(F)was characterized by the set of unary formulas in EQ-algebras.In particular,the relationships between prefilters and radicals of prefilters were discussed.It was got that if F and G are the filters of EQ-algebras A and B,respectively,then there exists a one-to-one correspondence between(A×B)/Rad(F×G)and A/Rad(F)×B/Rad(G).Finally,the concept of semi-maximal prefilters of EQ-algebras was given.And it was got that a maximal(implicative,obstinate)prefilter is a semimaximal prefilter.Also,it was demonstrated that F is a semimaximal filter of EQ-algebra E if and only if {1}/F is a semimaximal filter of E/F.2.We used the logical and algebraic methods to deal with predicate version of fuzzy type theory.First,the concept of monadic EQ-algebras was introduced,namely EQ-algebras with universal quantifiers and existential quantifiers.Then,the related properties of monadic EQ-algebras were studied.And it was obtained that the set of fixed points on monadic EQ-algebras can form a subalgebra.Moreover,the concepts of monadic prefilters(filters)in monadic EQ-algebras were introduced.It was proved that there exists a one-to-one correspondence between monadic filters and monadic congruences in good monadic EQ-algebras.Furthermore,an equivalent characteri-zation of minimal monadic prime prefilters was given.Also,the representable good monadic EQ-algebras were characterized by minimal monadic prime prefilters.Final-ly,monadic EQ-logic corresponding to monadic EQ-algebras was established and the soundness theorem and completeness theorem of this logic were proved.3.We used the logical methods to deal with logic version of fuzzy type theory First,the logic systems corresponding to equality algebras were established,namely equality propositional logic.And it was proved that this system has many better prop-erties,such as Modus Ponens rule(MP),Hypothetical Syllogism rule(HS),and etc..In particular,the completeness theorem of this system was demonstrated by two meth-ods.Moreover,two extended systems of equality propositional logic were introduced One is involutive equality propositional logic with double negation(corresponding to involutive equality algebras).The other is prelinear equality propositional logic with prelinearity(corresponding to prelinear equality algebras).Subsequently,the sound-ness theorems and completeness theorems of these logic were proved.Finally,the equality propositional logic was extended again.That is,? conjunction is equipped with ?-equality propositional logic.Additionally,the soundness theorem and com-pleteness theorem of this logic were proved.The above research results make a theoretical foundation for the development of fuzzy type theory and provide a theoretical support for the steady progress of artificial intelligence.