Formal Semantics in Modern Type Theories. Stergios Chatzikyriakidis
Chapter 1, Type Theories and Semantic Studies, starts with an overview of the historical development of type theories and a discussion on how to use a type theory as a foundational language for formal semantics. We then briefly describe Montague semantics, which is based on simple type theory,1 and MTT-semantics, and compare them by means of some simple examples. This serves to introduce the basics of MTT-semantics in a very sketchy manner, together with some summary notes on its historical development, and allows us to outline several important merits of employing MTTs as a foundational semantic framework.
– Chapter 2, Modern Type Theories, consists of an informal but rigorous and precise introduction to MTTs, mainly for linguistic semanticists. In order to introduce the basic concepts in MTTs, we use explanatory examples to show how these may be employed in semantic constructions and, in most cases, we present their formal rules in appendices (mainly for completeness). Special attention is paid to several mechanisms that are particularly important for MTT-semantics, including coercive subtyping (Luo 1997), signatures (Luo 2014) and linguistic universes (Luo 2011b; Chatzikyriakidis and Luo 2012). We shall also give a complete formal presentation of the type theories used in this book, which is based on various studies (Luo 2014, 2019a), both for completeness and for reference in future work.
– Chapter 3, Formal Semantics in Modern Type Theories, is a central chapter that explicates several important features of MTT-semantics and shows that the MTT-semantic approach is viable and coherent, on the one hand, and provides flexible and powerful mechanisms for adequate semantic interpretations, on the other hand. Some features are discussed in depth: the CNs-as-types paradigm (Ranta 1994; Luo 2012a), subtyping in MTT-semantics (Luo 2009c, 2012b) and propositional forms of judgmental interpretations (Xue et al. 2018). As a case study for MTT-semantics, we study semantics of adjectival modification according to a traditional classification of adjectives into intersective, subsective, privative and non-committal adjectives, and investigate how such different adjectival modifications can be modeled adequately in the CNs-as-types paradigm.2 This case study, together with the next two chapters, illustrates how the rich type structure in MTTs provide fruitful tools for modeling various linguistic features.
– Chapter 4, Advanced Modification, studies more advanced issues in adjectival and adverbial modification based on various studies (Chatzikyriakidis 2014; Chatzikyriakidis and Luo 2017a, 2020). After studying adjectival modification in section 3.3, we delve deeper into further issues concerning the semantics of modification, traditionally regarded as more advanced. In particular, we shall look at both adjectival and adverbial modification and argue that the rich typing mechanisms in MTTs are fit to deal with a number of issues on modification: gradability; gradable nouns; and veridical, event and intensional adverbs.
– Chapter 5, Copredication and Individuation, studies how the issue of copredication can be dealt with in MTT-semantics. First, the notion of dot-types proposed in the MTT-semantic setting (Luo 2009c, 2012b) is reviewed and shown to offer satisfactory semantic solutions to copredication. Then, we consider a number of challenging examples where both copredication and quantification are involved and show that, as proposed and studied in (Luo 2012a; Chatzikyriakidis and Luo 2018), CNs are better be interpreted as types associated with their own identity criteria (i.e. setoids) and copredication in such sophisticated situations requires a form of double distinctness of individuation: we provide an account based on the view of CNs-as-setoids and show that this gives us the correct semantics with intended results.
– Chapter 6, Reasoning and Verifying NL Semantics in Coq, shows how existing proof assistants such as Coq can be used in natural language reasoning based on MTT-semantics (Luo 2011b; Chatzikyriakidis and Luo 2014, 2016) – a promising technology that becomes available because MTTs are proof-theoretic and hence can be directly implemented. In this chapter, we introduce one of the leading proof assistants, Coq, and provide implementations for most of the semantic phenomena covered in the previous chapters. We further check the correctness of the implementations by providing proofs of a number of inferences that should go through, verifying that correct semantic accounts are given for the phenomena in question.
– Chapter 7, Advanced Topics, reports on several more advanced or on-going research developments on MTT-semantics. It consists of the following three sections:1) in section 7.1, we conduct a formal study of propositional forms as informally introduced in section 3.2.3. It is shown that the relevant propositional forms can be introduced axiomatically by means of a negation operator and this extension can be justified (Xue et al. 2018) and, furthermore, semantic overgeneration by such propositional forms can be avoided (Luo and Xue 2020; Xue et al. 2020);2) in section 7.2, we study dependent event types (DETs) proposed by Luo and Soloviev (2017) in the Montagovian setting,3 showing that dependent types may play a useful role in refining types of events in event semantics and that the extension with DETs is conservative and hence preserves the nice properties of the original theory (Luo and Soloviev 2020);3) in section 7.3, we study how to extend traditional categorial grammars with dependent types, starting to study dependent categorial grammars (DCGs). The theoretical basis for DCGs was developed and studied by the second author in Luo (2015, 2018c), where it is shown how to consider dependent Lambek types as syntactic categories corresponding to MTT-semantic types. In this book, we investigate DCGs in several aspects as related to CNs-as-types and more refined syntactic categories, and consider future promising research directions.
The diagram in Figure P.1 indicates how each chapter depends on the preceding chapters, although we have two points to make clear: (1) For Chapter 2, you can first read it through in less detail and then come back to revisit it later when needed. (2) Chapter 6 depends on earlier chapters only partly – you may read and understand most of the chapter without studying Chapter 4 or 5 in detail.
The intended audience of the present book includes researchers in formal semantics, computational semanticists, logicians or theoretical computer scientists interested in linguistic semantics and postgraduate students in linguistics with a background in formal semantics. A preliminary background in logic and some basic knowledge about Montague Grammar may be useful.
Figure P.1. Dependency diagram for reading
Throughout our work on MTT-semantics, we have benefited from discussions and communications with many researchers to whom we are extremely grateful. Here is an incomplete list: Robin Adams, Nicholas Asher, Daisuke Bekki, Jean-Philippe Bernardy, Rasmus Blanck, Robin Cooper, David Corfield, Nissim Francez, Matthew Gotham, Justyna Grudziñska, Ruth Kempson, Shalom Lappin, Huimin Lin, Georgiana Lungu, Harry Maclean, Aleksandre Maskharashvili, Louise McNally, Koji Mineshima, Richard Moot, Glyn Morrill, Larry Moss, Bengt Nordström, Gabriele Paveri-Fontana, Aarne Ranta, Christian Retoré, Sergei Soloviev, Göran Sundholm, Ribeka Tanaka, Tao Xue, Yu Zhang and Colin Zwanziger.
SC