Formal Semantics in Modern Type Theories. Stergios Chatzikyriakidis
in proof assistants and we have used the proof assistant Coq (Coq 2010) to implement MTT-semantics and performed various reasoning tasks and experiments based on such implementations (Luo 2011b; Chatzikyriakidis and Luo 2014, 2016) (see Chapter 6 for more details).
It is worth remarking that, when applied to formal semantics, whether a type theory is predicative or impredicative makes a difference. Although using Σ-types in a predicative type theory both as the existential quantifier and a structural mechanism solves the anaphora problem for simple donkey sentences (see footnote 16 on p13), such interpretations are inadequate when counting is involved (see, for example, those sentences involving “most” (Sundholm 1989; Tanaka 2015)).25 As proposed and discussed in Luo (2012a, 2019b), one would solve this problem by imposing proof irrelevance (i.e. all proofs of a logical proposition are the same); however, such an imposition is only OK for type theories that distinguish logical propositions from other types (as in UTT), not when they are identified (as in Martin-Löf’s type theory). With proof irrelevance in UTT, where both ordinary existential quantifier and Σ-types exist, a satisfactory semantics can be given to a sentence with both anaphora and counting.26 Such a solution is also available for predicative type theories as well: for example, as proposed and studied in Luo (2019b), we can employ MLTTh, an extension of Martin-Löf’s type theory with the h-logic studied by Voevodsky in the HoTT project (HoTT 2013), to obtain an adequate foundational semantic language, which accommodates both strong and weak quantifiers in a similar fashion.
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.
1.4.3. Merits of MTT-semantics
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
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.1 for 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 4 and 5 that 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)