Stergios Chatzikyriakidis - Formal Semantics in Modern Type Theories

The study of MTT-semantics, especially its development in the last decade, is a part of a wider research endeavor by many researchers who have recognized the potential advantages of rich type structures in constructing formal semantics. For instance, besides work on MTT-semantics mentioned above, Retoré (2013) has employed the system F (Girard 1972; Reynolds 1974) to study how to use polymorphism in semantic constructions and Bekki (2014) has studied Dependent Type Semantics to discuss issues such as anaphoric expressions and underspecification in dependent type theories. 27 Besides these, there are also several pieces of very interesting work on linguistic semantics based on ideas of dependent typing, but not on formal type theories, including those by Asher (2012), Cooper (2005) 28 and Grudzińska and Zawadowski (2017), among others.

We contend that, as foundational semantic languages, MTTs are advantageous and MTT-semantics has unique merits, as compared with simple type theory and Montagovian semantics. Here, we outline some of its merits, organized below into two respects, which are further elaborated in the following chapters (and related papers). Please note that this is in no way to cover all, or even most, attractive aspects of MTT-semantics and it only serves the purpose of highlighting some notable features, hopefully making it easier to understand the following pages of the book.

Rich typing for semantic constructions . MTTs have a rich type structure: unlike simple type theory in which there are only the base types e and t and arrow types A → B (or A, B , in a traditional notation), there are many ways to form types including, for example, dependent types (e.g. Π-types and Σ-types), inductive types (e.g. types of numbers/lists/vectors/trees and disjoint union types), logical types for propositions (under the propositions-as-types principle) and type universes (types that contain types as objects). 29 As we mentioned briefly earlier, the typing judgments of the form a : A, intuitively saying that a is an object of type A , are very different from the set-theoretical membership statements of the form s ∈ S : for example, the typing judgment a : A is mechanically decidable, while the membership relation s ∈ S (expressing that s satisfies predicate S ) is a formula in the first-order logic and its truth is undecidable. Among other things, this decidability property is essential for any type theory to have a logic based on the propositions-as-types principle.

The rich typing disciplines also give us several advantageous points in semantic constructions. A simple advantage is that rich typing allows us to employ typing judgments, rather than membership statements, to deal with selectional restriction. In MTT-semantics, we can use the typing judgment j : Man to express that “John is a man” and this is different from Montague semantics where we use the formula man ( j ) to represent the meaning. Therefore, typing also offers us a means to deal with selectional restriction – to exclude meaningless sentences or phrases. This allows us to use typability as a formal criterion to judge whether a sentence is meaningful: for example, we would usually think (in a non-fictional world) that a sentence like “Tables talk” is meaningless with a category error – this is captured by means of typing in MTT-semantics: the MTT-interpretation of “Tables talk” is ill-typed (or an illegal expression). This is different from Montague semantics where the interpretation of “Tables talk” is just a false statement but it is a well-formed formula. (See section 3.1for a further explanation.)

The rich type structure in MTTs enables us to use types to play the role of representing various collections, 30 the role played by sets in the Montagovian set-theoretical semantics. Besides acting as logical propositions, types can also be used in various ways in semantic constructions. For example, this allows one to interpret common nouns as types rather than predicates (see the above, (Luo 2012a) and section 3.2.1); in section 3.3, we show how various adjectival modifications can be modeled by means of rich typing, with Σ-types for intersective modification, Π-types (and the associated polymorphism) for subsective modification, disjoint union types and Π-polymorphism for privative modification, and a logical modal collection operator for non-committal modification. We shall also show in Chapters 4and 5that the typing structure can be used to model more advanced linguistic features such as gradable adjectival modification and copredication.

As mentioned earlier, subtyping is not only essential for MTT-semantics, but also very useful in semantic constructions. For instance, coercive subtyping is employed in defining dot-types (Luo 2009c, 2012b) for giving adequate interpretations of sentences involving copredication, an example of which is the sentence in ( 1.16), where a delicious lunch refers to food and a lunch that took forever refers to a process. Such copredication phenomena have been studied by many researchers such as Pustejovsky (1995) and Asher (2012). For MTT-semantics, the second author has proposed to use dot-types to deal with copredication (Luo 2009c): for this example, lunch involves two aspects: that of being food and that being a process. This is formalized by means of the subtyping relationship ( 1.17). It is then straightforward to see that the formula in ( 1.18), which interprets ( 1.16), is well-typed because of the subtyping relation in ( 1.17), where l : Lunch is the interpretation of “the lunch”.

( 1.16) The lunch was delicious but took forever.

( 1.17) Lunch ≤ Food • Process

( 1.18) delicious(l) ∧ take_forever(l)

When defining dot-types such as Food • Process , coercive subtyping is used: we have, for example, Food • Process ≤ Food and Food • Process ≤ Process and therefore ( 1.18) is well-typed: both predicates delicious and take_forever can be applied to l : Lunch because both domains Food and Process are supertypes of Lunch . (For more formal details on subtyping, see section 2.4and 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. 31 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. 32 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. 33