On fuzzy type theory (Q703370)

Fuzzy logic was originally invented to describe human reasoning. The original fuzzy logic covered only propositional formulas. Later, quantifiers were added to fuzzy logic. However, an important part of human reasoning is still missing from fuzzy logic: arguments that usually require a higher-order logic. For example, we can say that \(X\) is a typical plant because it has all the properties that plants normally have. Such statements include quantifiers over all the properties; they are usually formalized in second-order logic. In the traditional (non-fuzzy) logic, one of the ways to describe higher-order logic is via a type theory. Type theory was originally designed to handle similar problems in set theory, where, in addition to sets of integers (i.e., in effect, properties of integers -- properties of first order), we also have sets of sets of integers (i.e., properties satisfied by properties of first order). To formalize higher-order-type statements in fuzzy logic, the author proposes a new formalism that extends type theory to the multi-valued case of fuzzy logic. He also proves properties of this fuzzy type theory, e.g., its completeness. Interestingly, it turns out that these results are only possible within an appropriate formalization of fuzzy logic: e.g., it is essential to include a hedge ``absolutely true'' -- defined as \(\Delta(a)=1\) if \(a=1\) and \(\Delta(a)=0\) otherwise -- into the set of basic fuzzy logic operations.