Fuzzy type theory, EQ-algebra, types and subtypes, lambda-calculus with subtypes

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  is interpreted by some function M -> M. It was proved that FTT is complete w.r.t. general models, i.e., we may consider in them also sets M\subset  M^M . In some applications it is necessary to express syntactically also functions on M'  where M' is a subset of  M. The solution (known also in TT) is to introduce the, so called, subtypes. If a type  is a subtype then M' is a subset of M. In this paper we elaborate a new kind of fuzzy type theory extended by subtypes and prove completeness of it. This theory also opens the door to introduction of FTT with partial functions on all levels.