Formal Semantics in Modern Type Theories. Stergios Chatzikyriakidis

Чтение книги онлайн.

Читать онлайн книгу Formal Semantics in Modern Type Theories - Stergios Chatzikyriakidis страница 13

Formal Semantics in Modern Type Theories - Stergios Chatzikyriakidis

Скачать книгу

rel="nofollow" href="#ulink_cd85cbe5-1aba-5a14-8352-5601b8e896d4">section 2.4 and section 3.2.2, and for more about copredication and dot-types, see Chapter 5.)

      MTT-semantics is both model-theoretic and proof-theoretic. MTT-semantics has a unique important feature: it is both model-theoretic and proof-theoretic, as argued for in Luo (2014, 2019a), and this has made MTTs a particularly suitable framework for formal semantics. Being model-theoretic, MTT-semantics provides a wide coverage of various linguistic features and, being proof-theoretic, its foundational languages have proof-theoretic meaning theory based on inferential uses (appealing philosophically and theoretically) and it establishes a solid foundation for practical reasoning in natural languages on computers (appealing practically). Altogether, this strengthens the argument that MTT-semantics is a promising framework for formal semantics, both theoretically and practically.

      Furthermore, the fact that MTTs are proof systems with proof-theoretic semantics has another significant and practical consequence in natural language reasoning based on MTT-semantics. In particular, this makes it possible for MTTs to be implemented in proof assistants such as Agda (Agda 2008), Coq (Coq 2010) and Lego/Plastic (Luo and Pollack 1992; Callaghan and Luo 2001) – computer-assisted reasoning systems that computer scientists have developed and successfully used for the formalization of mathematics and verification of computer programs. Therefore, MTT-semantics can be directly implemented in proof assistants that implement MTTs: for example, the MTT-semantics in type theory UTT has been implemented in Coq (Chatzikyriakidis and Luo 2014; Luo 2011b) and Plastic (Xue and Luo 2012) and used for natural language reasoning (Chatzikyriakidis and Luo 2016) (see Chapter 6 for more details).

      We shall develop the theme that MTT-semantics is model-theoretic in two fronts: the first is to note that, like sets in Montague semantics, types in MTTs are employed to represent collections of objects (for example, semantic interpretations of common nouns), and the rich type structure in MTTs provides powerful means of representation for formal semantics. In other words, intuitively, types in MTTs are rich enough to play the role of representing collections, just as sets in Montague semantics.

      As mentioned above, MTTs have a rich type structure and, as to be demonstrated in Chapters 3, 4 and 5, in MTT-semantics these types play an important role in representing different kinds of collections such as those given by CNs modified by various kinds of adjectives. Such representations by means of types are not available for simple type theory, which has only base types and arrow types. Types in MTTs are powerful and can provide various different representations in semantic constructions. This is the first facet to explicate that MTT-semantics is model-theoretic.

      The second facet is that the contextual structures in MTTs, which are not available in traditional logical systems, provide very useful means in semantic constructions and, in particular, they offer effective support for model-theoretic descriptions of incomplete possible worlds. We shall describe the notion of signatures (Luo 2014) (see section 2.1) that allow MTTs to be more suitable to support model-theoretic descriptions.

      It is worth pointing out that foundational semantic languages that are both model-theoretic and proof-theoretic were not available before the development of MTT-semantics or, at least, people have not recognized that there is such a possibility (in particular, set theory is not such a language since it is not proof-theoretic). MTT-semantics is both model-theoretic and proof-theoretic and sheds a new light on the division between model-theoretic semantics and proof-theoretic semantics and allows us to study formal semantics from a new perspective.

      1 1 Attribution for the development of simple type theory should also go to the Polish logician Chwistek (see, for example, Linsky 2009).

      2 2 The term “modern type theory” is adopted to distinguish MTTs, as used in MTT-semantics, from Church’s simple type theory, as used in Montague semantics, and it appeared for the first time in Luo (2009c).

      3 3 In this respect, interested readers are referred to Logic-enriched Type Theories (LTTs), proposed by Aczel and Gambino in their study of type-theoretic interpretations of constructive set theory (Aczel and Gambino 2000; Gambino and Aczel 2006), and to the work by the second author and Adams on a type-theoretical framework of LTTs to support

Скачать книгу