From Classical to Fuzzy Type Theory

Abstract

Higher-order logic—the type theory (TT)—is a powerful formal theory that has various kinds of applications, for example, in linguistic semantics, computer science, foundations of mathematics and elsewhere. It was proved to be incomplete with respect to standard models. In fifties and sixties of the last century, L. Henkin proved that there is an axiomatic system of TT that is complete if we relax the concept of model to the, so called, generalized one. The difference is that domains of functions in generalized models need not contain all possible functions but only subsets of them. Henkin then proved that a formula of type o (truth value) of a special theory T of the theory of types is provable iff it is true in all general models of T. Mathematical fuzzy logic is a special many-valued logic whose goal is to provide tools for capturing the vagueness phenomenon via degrees. It went through intensive development and many formal systems of both propositional as well as first-order fuzzy logic were proved to be complete. This endeavor was crowned in 2005 when also higher-order fuzzy logic (called the Fuzzy Type Theory, FTT) was developed and its completeness with respect to general models was proved. The proof is based on the ideas of the Henkin’s completeness proof for TT. This paper addresses several complete formal systems of the fuzzy type theory. The systems differ from each other by a chosen algebra of truth values. Namely, we focus on three systems: the Core FTT based on a special algebra of truth values for fuzzy type theory—the EQ-algebra, then IMTL-FTT based on IMTLΔ-algebra of truth values and finally the Ł-FTT based on MVΔ-algebra of truth values.