This 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.
Author(s): Stergios Chatzikyriakidis, Zhaohui Luo
Series: Logic Linguistics and Computer Science Set 2
Publisher: ISTE / Wiley
Year: 2020
Language: English
Pages: 256
Cover
Title Page
Contents
Preface
1. Type Theories and Semantic Studies
1.1. Historical development of type theories
1.2. Foundational semantic languages
1.3. Montague’s model-theoretic semantics
1.4. MTT-semantics: formal semantics in modern type theories
2. Modern Type Theories
2.1. Judgments and contextual mechanisms
2.2. Type constructors
2.3. Universes
2.4. Subtyping
2.5. Formal presentation of type theories with signatures
3. Formal Semantics in Modern Type Theories
3.1. Basic linguistic categories
3.2. Several unique features of MTT-semantics
3.3. Adjectival modification: a case study
4. Advanced Modification
4.1. The data
4.2. Gradable adjectives
4.3. Gradable nouns
4.4. Multidimensional adjectives
4.5. Adverbial modification
4.6. Final remarks on modification: vagueness
5. Copredication and Individuation
5.1. Copredication and individuation: an introduction
5.2. Dot-types for copredication: a brief introduction
5.3. Identity criteria: individuation and CNs as setoids
5.4. Concluding remarks and related work
6. Reasoning and Verifying NL Semantics in Coq
6.1. Proof assistant technology based on MTTs
6.2. A linguist friendly introduction to Coq
6.3. MTT-semantics in Coq
7. Advanced Topics
7.1. Propositional forms of judgmental interpretations: formal treatment
7.2. Dependent event types
7.3. Dependent categorial grammars
Appendix 1: Simple Type Theory ?
Appendix 2: Type Constructors
Appendix 3: Prop and Logical Operators in Impredicative MTTs
Appendix 4: And for Coordination
Appendix 5: Formal System LF_Δ
Appendix 6: Rules for Dot-Types
Appendix 7: Coq Codes
References
Index
