Towards Fuzzy Constructive Type Theories

In this paper, we explore combinations of Fuzzy Logic and Constructive Higher Order Type Theory. Although Fuzzy Logic is more than 60 years old, and Fuzzy Type Theories have been studied in the classical case of Church’s Theory of Types, there is yet no satisfactory understanding of how to deal with judgements of the shape Γ - M :d A, where d is a fuzzy degree of confidence. Addressing this issue is important in view of the growing interest in quantitative and non-idempotent type theories. To this end, we introduce fuzzy type assignment systems in order to investigate how minimal fuzzy formulæ behave as types, according to some fuzzy proposition-as-types paradigm. Moreover, we study a fuzzy version of intersection types. In both systems assumptions are multisets and d, in Γ - M :d A, is a formula of minimal propositional Fuzzy Logic. Evaluating d in a residuated lattice [0,1], endowed with a left-continuous T-norm, we can analyse how the degree of confidence propagates from the assumptions to the conclusion, thereby yielding new information on the derivation. The former system sheds light on the connection between minimal Fuzzy Logics and affine λ-calculus and permits to show that the tautologies in the BCK-logic amount to the simple types which are inhabited by BCK-combinators. The latter system keeps track of the number of times a given fuzzy assumption is made. We discuss the standard suite of metatheorems (inversion lemmata and subject-conversion) for the systems, and point to possible uses of the fuzzy formula attached to the membership construct.