description operator

This paper is a study of fuzzy type theory (FTT) with partial functions. Out of several possibilities we decided tointroduce a special value ”∗” that represents ”undefined”. In the interpretation of FTT, this value lays outside of thecorresponding domain. In the syntax it can be naturally represented by the description operator acting on the empty(fuzzy) set, because choosing an element from its kernel gives no result. Among many results, we will show that if, in atheory T, ”∗” is defined or provable then T is contradictory. We will also show completeness in the sense any consistenttheory of FTT with partial functions has a model.