as intuitionistic inference (Luo 2007; Adams and Luo 2010). Also related is the recent work on homotopy type theory where Martin-Löf’s type theory is employed in such a way that the logic can be either intuitionistic or classical (HoTT 2013).4 4 Although the logic in IL can be used to describe a lot of linguistic features, there are many others still found very difficult, if not impossible, to be characterized in IL (or simple type theory); in the literature, these phenomena are rather studied in set theory directly – see such “direct interpretations” in, for example, Winter (2016). This is one of the reasons that, for Montague semantics, set theory itself is considered the foundational semantic language, rather than the intermediate language IL.
5 5 A remark may be necessary here: we are only emphasizing the similarities between type theory and set theory here. However, they are very different – for example, it is their difference that enables us to say that MTT-semantics is also proof-theoretic and can be successfully implemented on computers for natural language reasoning. For some readers, the difference will only be apparent later on, say, after reading Chapter 2 to become more familiar with MTTs.
6 6 Our description of simple type theory is formal and, in section 7.2, will be extended with dependent event types, one of the applications of dependent types in Davidsonian event semantics.
7 7 IL as described in Montague (1973) also contains a modal operator used to describe tense. As noted in Montague (1973), it can be considered as a special predicate symbol to be interpreted as intended. We omit it here.
8 8 For those who are unfamiliar with natural deduction rules, it may be worth remarking that the rules below define a natural deduction system whose sentences are called judgments. A judgment J is correct (formally called derivable) if there is a derivation of J, that is, a finite sequence of judgments J1, ..., Jn with Jn = J such that, for all 1 ≤ i ≤ n, Ji is the conclusion of an instance of some inference rule whose premises are in {Jk | k < i }.
9 9 Here, the names of the base types e and t follow the Montagovian tradition. In Church (1940), e and t are named ι and o, respectively.
10 10 As in λ-calculus, β-conversion holds: we have that (λx:A.b[x])(a) is convertible to b[a], notation (λx:A.b[x])(a) ≈ b[a], where b[a] is obtained from b[x] by substituting a for all free occurrences of x. In other words, these two expressions (λx:A.b[x])(a) and b[a] are computationally the same – the former computes to the latter, and the relation ≈ of β-conversion is the reflexive, symmetric and transitive closure of this basic computational relation.
11 11 This is slightly simpler than Montague’s treatment in IL (Montague 1973), although it gives the same power. For its justification, see Gallin’s work on TY2 (Gallin 1975).
12 12 We shall deal with aspects of intensionality when discussing non-committal adjectives in section 3.3.4 and intensional adverbs in section 4.5.4.
13 13 In predicative MTTs such as Martin-Löf’s type theory, one would use a predicative universe which is only a type of some propositions, not all of them. Although we may relate Prop to the type t of truth values in Church’s simple type theory, they have subtle differences. The differences between MTTs and Church’s simple type theory include whether the theory is classical or constructive and whether there are proof objects, among others. These are beyond the scope of our discussions here.
14 14 This constitutes the basis of dealing with selectional restriction by means of decidable typing, among many other things (more details later).
15 15 In MTT-semantics, we also study judgmental interpretations of sentences and how to turn them into propositional forms – see section 3.2.3 for an informal introduction and section 7.1 for a formal treatment.
16 16 In Martin-Löf’s type theory with propositions-as-types (the so-called PaT logic), existential quantification is represented by Σ, which is strong in the sense that an object of a Σ-type is a pair whose first component can be projected out as the witness of the truth of the existentially quantified sentence. For example, as shown in Sundholm (1986), the donkey sentence (1.11) can be interpreted as (1.12), where Farmer and Donkey are the types interpreting “farmer” and “donkey”, respectively:
17 (1.11) Every farmer who owns a donkey beats it.
18 (1.12) Πz : (Σx:FarmerΣy:Donkey. own(x, y)). beat(π1(z),π1(π2(z)))
19 Note that, in (1.12), πi’s are projection operators for Σ-types and, in particular, π1 projects out the witness of a proof of an existential formula represented by a Σ-type (see section 2.2.2 for more details). However, such a use of Σ-types as both existential quantifier and a structural mechanism causes problems such as counting – see the second last paragraph in this section and footnotes 25/26 on p.15/p.16 for an example and explanations.
20 17 Ranta (1994) discussed several possible solutions but failed to obtain a satisfactory solution and, in particular, he did not realize that subtyping should be employed to solve the problem. In fact, coercive subtyping (Luo 1999) which, unlike the ordinary subsumptive subtyping, is adequate for dependent type theories and can be used to rectify this – see section 3.3.1 and footnote 21 on p68 for more on this topic.
21 18 In this book, the phrases such as possible worlds and situations are used informally and, in particular, they do not refer to any of their formal meanings that have been used in the literature.
22 19 The type-theoretical notion of context is not quite proper to model situations since abstraction can always be done over entries in a context. A further development has been made in Luo (2014) as well as Lungu and Luo (2018) to introduce the notion of signature, which can be used to represent situations in a more adequate way. In this book, we shall use type theory with signatures – for more details, see Chapter
