fuzzy type theory; type theory; EQ-algebra

Fuzzy type theory (FTT) is a higher-order fuzzy logic that generalizes classical type theory (TT). Recall that the latter was established over 100 years ago by B. Russel. Its formalism was later well elaborated by A. Church and L. Henkin. In this theory, each formula A of the type \alpha is interpreted by some function. It was proved that FTT is complete w.r.t. general models. In some applications it is necessary to express syntactically also partial functions The solution (known also in TT) is to introduce the, so called, subtypes. In this paper we elaborate a new kind of fuzzy type theory extended by subtypes and prove completeness.