Formal Semantics in Modern Type Theories

3Formal Semantics in Modern Type Theories

This chapter studies formal semantics in modern type theories (MTT-semantics). In Chapter 1, section 1.4.1 in particular, we briefly described how some basic linguistic categories are interpreted in MTT-semantics. Now, after introducing some of the basic constructs of MTTs in the previous chapter, we are in a better position to study various key features of MTT-semantics. We shall do so in the following sections: the first of which, section 3.1, will continue section 1.4.1 to explain in more details how to interpret some of the basic linguistic categories.

Then, in section 3.2, we shall explicate several unique features of MTT-semantics that are different from Montague semantics, starting from the CNs-as-types paradigm (Ranta 1994; Luo 2012a). A common noun (CN) such as “student” can be interpreted as a collection. In Montague semantics, a set is used as its interpretation to represent the collection (e.g. “student” is interpreted as the set of those entities denoting students),¹ while in MTT-semantics, a type is used to denote its meaning (e.g. “student” is interpreted as a type Student that might either be a base type or a structured type defined by means of other types, depending on the current semantic interpretations). This CNs-as-types paradigm is introduced and elaborated in section 3.2.1: it relates the paradigm to the idea of identity criteria of CNs and the constructive notion of sets/types, shows that MTTs’ rich type structures ...