Stergios Chatzikyriakidis - Formal Semantics in Modern Type Theories

11 11This 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 12We shall deal with aspects of intensionality when discussing non-committal adjectives in section 3.3.4and intensional adverbs in section 4.5.4.

13 13In 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 14This constitutes the basis of dealing with selectional restriction by means of decidable typing, among many other things (more details later).

15 15In MTT-semantics, we also study judgmental interpretations of sentences and how to turn them into propositional forms – see section 3.2.3for an informal introduction and section 7.1for a formal treatment.

16 16In 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.2for 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 17Ranta (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.1and footnote 21 on p68 for more on this topic.

21 18In 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 2, especially section 2.1, section 2.4and section 2.5.

23 20One may consider the point of view (and we agree with it) that an impredicative type theory with an internal totality Prop of logical propositions is better suited for formal semantics – see Luo (2019b) on proof irrelevance for one of the arguments for this.

24 21In particular, it offers a satisfactory solution to Ranta’s multiple categorization problem as mentioned above and footnote 17 on p13, and hence overcomes the major obstacle for MTTs to be applied to formal semantics – for more on this, see section 3.2.2.

25 22Formally, the type theories in this book are extended with signatures (Luo 2019a) – see Chapter 2.

26 23For people familiar with type theory, it is worth mentioning that dot-types (Luo 2009c) are not ordinary inductive types, rather they are specially developed for dealing with copredication.

27 24The idea of using coercive subtyping for formal semantics was first proposed by the second author in Luo and Callaghan (1998), but it was not until much later (a decade later) when Luo (2009c) was published where coercive subtyping was employed in semantic interpretations of modified CNs and constructing dot-types for copredication.

28 25This problem with Σ playing a “double role” can be illustrated by considering ( 1.13), whose interpretation in Martin-Löf’s type theory would be ( 1.14), where “most” is interpreted by means of the quantifier Most defined in Sundholm (1989). (The second author thanks Justyna Grudziñska for a discussion about this example.)( 1.13) Most farmers who own a donkey beat it.( 1.14) Most z : (Σx:FarmerΣy:Donkey. own(x, y)). beat(π1(z),π1(π2(z)))

29 The interpretation ( 1.14) fails to respect correct counting because, with Σ, the proof objects of own(x, y) contribute to counting in a wrong and unintended way.

30 26As pointed out by the second author in Luo (2019b), in a type theory such as UTT where we can enforce proof irrelevance (see section 3.3.1and footnote 22 on p. 69), the donkey sentence ( 1.13) in the above footnote 25 can be given a satisfactory interpretation ( 1.15) by means of Σ and the weak propositional quantifier ∃, where the propositional quantifier Most is defined in UTT:

31 ( 1.15)

32 Note that ∃ and Σ are both traditional binding operators. Although we may not give an intended semantics to ( 1.13) using only either of them alone, it can be done if both are available. This implies that, in order to solve such a problem, we may not have to abandon traditional binding mechanisms to consider new mechanisms, a strategy adopted by proponents of dynamic semantics, such as Kamp (1981) and Groenendijk and Stokhof (1991). For example, dynamic predicate logic (Groenendijk and Stokhof 1991) is a non-standard logical system: among other things, it is non-monotonic and the notion of dynamic entailment fails to be reflexive or transitive – such a move seems to be paying too big a price that could have been avoided.

33 27DTS has two versions as far as the underlying type theory is concerned: Martin-Löf’s type theory in Bekki (2014) and some impredicative type system in Bekki and Mineshima (2017). In the DTS approach, CNs are interpreted as predicates as in the traditional Montagovian semantics and, because of this, we would not need the rich type structures and DTS mainly uses Π/Σ-types as logical operators. This means that it does not have the advantages in the CNs-as-types paradigm (see section 3.2.1), either.

34 28It may be worth clarifying that the system called Type Theory with Records (TTR) (Cooper 2005, 2017) is not a type theory, as the term is usually understood, but rather a set-theoretic notational framework, where a : T if, and only if, a is a member of the set whose name is T in set theory. Although it is set-theoretical, the development of TTR, especially in the early days, was influenced by the study of record types by Tasistro (1997) and Betarte (1998) in Martin-Löf’s logical framework.

35 29See Chapter 2, and sections 2.2 and 2.3 in particular, for more details.

36 30In this book, the word collection is used to refer to informal entities, rather than their formal representations such as sets or types.

37 31For details, see Chapter 2and related references for MTTs.

38 32It is worth remarking that even if a logical system is specified by proof-theoretic rules, it can still fail to have a proper proof-theoretic semantics. For example, to have a proof-theoretic semantics, the introduction and elimination rules for any logical operator or type constructor must be in harmony, as discussed by Dummett (1991) and others.