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.

MTTs are proof-theoretically specified.³¹ Usually, an MTT is presented as a natural deduction system where, in particular, every type constructor is specified by inference rules among which introduction rules are to declare how the type (formula) is inhabited (proved) and the elimination rules to specify what consequences can be derived under the assumption that the type (formula) is inhabited (proved). These rules are harmonious and, as an important consequence, MTTs themselves have proof-theoretic semantics, as studied by logicians such as Gentzen (1935), Prawitz (1974, 1973) and Martin-Löf (1984, 1996) and discussed by philosophers such as Dummett (1975, 1991) and Brandom (1994, 2000), among others.³² For example, Martin-Löf has studied and developed meaning theory and given a solid foundation for his type theory (Martin-Löf 1984). Therefore, MTT-semantics, the formal semantics in MTTs, is proof-theoretic in the sense that its foundational semantic languages have proof-theoretic meaning theory based on inferential uses.³³

      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).

That MTTs are proof-theoretically presented has led to a widely held view that formal semantics based on MTTs is only proof-theoretic and, in particular, it is not model-theoretic.³⁴ This is mistaken – MTT-semantics is also model-theoretic. First of all, it is necessary for us to make clear that, by MTT-semantics being model-theoretic, we do not mean that an MTT can be given a set-theoretical semantics (e.g. in some categorical framework); instead, we mean that an MTT itself can be employed as a meaning-carrying language to give model-theoretic semantics to natural language. That is, in MTT-semantics, an MTT plays the role of meaning-carrying language – in the traditional model-theoretic semantics, this is the role played by set theory. In other words, we argue that MTTs can well serve as a foundational semantic language to give meanings in themselves in a model-theoretic semantics.

      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.

The notion of signature in type theory, as far as we know, first appeared in Edinburgh Logical Framework (Harper et al. 1993), where signatures with membership entries are used to describe a logical system.³⁵ We shall introduce signatures that do not just have the usual membership entries of the form x : A but also contain two new forms of entries, subtyping entries and manifest entries (see section 2.4), which strengthen the power of signatures in representing (incomplete) possible worlds, even in cases where, for example, situations are infinite or involve more sophisticated phenomena. As shown in Lungu and Luo (2018) and section 2.5, extending MTTs with signatures, which may contain entries of the above new forms as well as the membership entries, preserves their nice meta-theoretic properties such as strong normalization (and hence logical consistency).

      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 СКАЧАТЬ