Description
Book SynopsisThis book studies formal semantics in modern type theories (MTTsemantics). Compared with simple type theory, MTTs have much richer type structures and provide powerful means for adequate semantic constructions. This offers a serious alternative to the traditional settheoretical foundation for linguistic semantics and opens up a new avenue for developing formal semantics that is both model-theoretic and proof-theoretic, which was not available before the development of MTTsemantics. This book provides a reader-friendly and precise description of MTTs and offers a comprehensive introduction to MTT-semantics. It develops several case studies, such as adjectival modification and copredication, to exemplify the attractiveness of using MTTs for the study of linguistic meaning. It also examines existing proof assistant technology based on MTT-semantics for the verification of semantic constructions and reasoning in natural language. Several advanced topics are also briefly studied, including dependent event types, an application of dependent typing to event semantics.
Table of ContentsPreface ix
Chapter 1. Type Theories and Semantic Studies 1
1.1. Historical development of type theories 2
1.2. Foundational semantic languages 4
1.3. Montague’s model-theoretic semantics 6
1.3.1. Simple type theory: a formal description 6
1.3.2. Montague semantics: examples and intensionality 9
1.4. MTT-semantics: formal semantics in modern type theories 10
1.4.1. A glance at MTT-semantics 10
1.4.2. MTTs as foundational semantic languages: historical notes 13
1.4.3. Merits of MTT-semantics 17
Chapter 2. Modern Type Theories 23
2.1. Judgments and contextual mechanisms 24
2.2. Type constructors 28
2.2.1. Π-Types of dependent functions 28
2.2.2. Σ-types of dependent pairs 30
2.2.3. Disjoint union types, unit types and finite types 32
2.3. Universes 33
2.3.1. Prop and logical propositions 33
2.3.2. Universes in linguistic semantics 35
2.3.3. Tarski-style and Russell-style universes 37
2.4. Subtyping 38
2.5. Formal presentation of type theories with signatures 43
Chapter 3. Formal Semantics in Modern Type Theories 47
3.1. Basic linguistic categories 48
3.2. Several unique features of MTT-semantics 51
3.2.1. Common nouns as types 51
3.2.2. Subtyping in MTT-semantics 54
3.2.3. Judgmental interpretations and their propositional forms 60
3.3. Adjectival modification: a case study 65
3.3.1. Intersective adjectives 67
3.3.2. Subsective adjectives 69
3.3.3. Privative adjectives 71
3.3.4. Non-committal adjectives 72
Chapter 4. Advanced Modification 75
4.1. The data 75
4.2. Gradable adjectives 80
4.3. Gradable nouns 84
4.3.1. Gradable nouns as Σ-types 85
4.4. Multidimensional adjectives 86
4.4.1. Multidimensional adjectives: going more fine-grained 87
4.5. Adverbial modification 90
4.5.1. Veridicality 91
4.5.2. Event adverbs: manner, agent-oriented and speech-act adverbs 91
4.5.3. Domain, evaluative adverbs 95
4.5.4. Intensional adverbs 96
4.6. Final remarks on modification: vagueness 98
Chapter 5. Copredication and Individuation 99
5.1. Copredication and individuation: an introduction 100
5.2. Dot-types for copredication: a brief introduction 104
5.3. Identity criteria: individuation and CNs as setoids 108
5.3.1. Inheritance of identity criteria: usual cases of individuation 110
5.3.2. Generic semantics of numerical quantifiers 112
5.3.3. Copredication with quantification 113
5.3.4. Verbs plus adjectives: more on copredication with quantification 117
5.4. Concluding remarks and related work 119
Chapter 6. Reasoning and Verifying NL Semantics in Coq 127
6.1. Proof assistant technology based on MTTs 128
6.1.1. Mathematical proofs 128
6.1.2. Software verification 128
6.2. A linguist friendly introduction to Coq 129
6.2.1. Basics of Coq: types, sorts, functions 130
6.2.2. The proof engine of Coq 132
6.2.3. Useful proof tactics in Coq 135
6.2.4. Inductive types and record types 139
6.3. MTT-semantics in Coq 142
6.3.1. Adjectival and adverbial modification 143
6.3.2. Copredication and individuation in Coq 146
6.3.3. Related work 149
Chapter 7. Advanced Topics 151
7.1. Propositional forms of judgmental interpretations: formal treatment 151
7.2. Dependent event types 157
7.3. Dependent categorial grammars 163
Appendices 173
Appendix 1. Simple Type Theory C 175
Appendix 2. Type Constructors 177
Appendix 3. Prop and Logical Operators in Impredicative MTTs 181
Appendix 4. And for Coordination 183
Appendix 5. Formal System LFΔ 187
Appendix 6. Rules for Dot-Types 191
Appendix 7. Coq Codes 193
References 209
Index 225
