Formal Semantics in Modern Type Theories

Stergios Chatzikyriakidis, Zhaohui Luo

• Publisher: Wiley-ISTE
• Year: 2020
• Print ISBN: 9781786301284
• eBook ISBN: 9781119489214
• Edition: 1
• Topic: Sprachen & Linguistik
• Subtopic: Sprachliche Semantik

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.

1
Type Theories and Semantic Studies

The long history of the study of semantics has produced a number of theories of meaning. For example, the referential theory adopts a Platonic viewpoint and proposes that meanings are entities in the world; the internalist theory, such as that held by Chomsky, suggests that meanings are concepts in our minds, and the use theory, which is closely related to Wittgenstein’s slogan of “meaning is use”, advocates that meanings are embodied in the ways that language is used in social practice. Besides being very interesting themselves, these philosophical theories have had a profound impact on the ways in which researchers think of and approach formal semantics. For example, many semanticists have been influenced by the referential theory of meaning and believed that formal semantics should be model-theoretic (see, for instance, Portner (2005)), following Tarski’s ideas in model theory for logical systems and Montague’s ideas in set-theoretical semantics for natural language (Montague 1974). On the other hand, the use theory of meaning has convinced many others and has been substantially developed more recently, both by philosophers such as Dummett (1991) and Brandom (1994, 2000) on meaning theories in general and by logicians such as Gentzen (1935), Prawitz (1973, 1974) and Martin-Löf (1984, 1996) on proof-theoretic semantics for logical systems in particular.

This book studies formal semantics in modern type theories (MTT-semantics for short). We contend that MTT-semantics is both model-theoretic and proof-theoretic, a thesis that was first proposed by the second author in Luo (2014) and further elaborated in Luo (2019a), and will be explicated in this book. For natural language, both model-theoretic and proof-theoretic semantics have their own advantages and disadvantages, and it is not easy to imagine how one can combine them in a single semantic framework: in fact, up to now this has never been attempted, let alone done. We argue that MTT-semantics is the first framework with both characteristics: being model-theoretic, it provides powerful mechanisms to capture semantics for a wide range of linguistic features, and being proof-theoretic, it has a solid meaning-theoretic foundation and can be directly implemented by means of the current proof technology to support computer-assisted reasoning in natural language. This gives MTT-semantics unprecedented advantages over other semantic frameworks.

In this chapter, we shall start with a brief account of the historical development of type theory for the study of the foundations of mathematics – the simple type theory for classical mathematics and dependent (modern) type theories for constructive mathematics. Simple type theory was employed by Montague and his followers as an intermediate language for the study of model-theoretic semantics of natural language, where set theory is taken as the foundational language. In MTT-semantics, on the other hand, modern type theories (MTTs) are themselves foundational languages. The new logical concepts and rich typing mechanisms in MTTs make them adequate to serve as foundational languages for formal semantics. We shall introduce MTT-semantics briefly, which will be developed further in the book, and summarize its advantages.

1.1. Historical development of type theories

Type theories are computational logical systems that were originally developed for the foundations of mathematics. At the beginning of the 20th Century, Russell (1903) developed the theory of types to solve a foundational problem of mathematics exposed as a number of well-known paradoxical contradictions in Cantor’s naive set theory that are related to self-reference. Some researchers, including Russell himself, attributed such paradoxes to “vicious circles” in formations of logical formulae (“impredicativity”, in a technical jargon), which is what Russell’s Ramified Theory of Types (Whitehead and Russell 1925) was designed to circumvent.

However, Ramsey (1926) pointed out that it was the logical paradoxes such as Russell’s paradox, not the semantic paradoxes such as Liar’s paradox, that can (and should) be avoided in formulations of logical calculi and that Russell had mixed up these two kinds of paradoxes, leading to complications and problems in his ramified theory of types. As Ramsey argued, although impredicativity in formula formations is circular, it is not vicious. Based on this, Ramsey suggested¹ that the ramified theory of types can be “simplified” into Simple Type Theory, which was later formally formulated by Church (1940) using the λ-notation and used by Montague (1973) in his Intensional Logic (IL) to study the formal semantics of natural language.

The early developments of type theory, including those by Russell and Ramsey as mentioned above, were driven by the search for foundational languages for classical mathematics. In the 1970s, various logicians, notably Feferman, Friedman, Martin-Löf and Myhill, among others, studied foundational languages for constructive rather than classical mathematics. Besides other systems, Martin-Löf’s type theory (Martin-Löf 1975, 1984) stood out with several new ground-breaking concepts that were not present in traditional logical systems. It adopts the notions of context, judgment and definitional equality, and introduces powerful typing mec...

Table of contents

• Cover
• Table of Contents
• Title page
• Copyright
• Preface
• 1 Type Theories and Semantic Studies
• 2 Modern Type Theories
• 3 Formal Semantics in Modern Type Theories
• 4 Advanced Modification
• 5 Copredication and Individuation
• 6 Reasoning and Verifying NL Semantics in Coq
• 7 Advanced Topics
• Appendices
• References
• Index
• End User License Agreement