2.1, section 2.4 and section 2.5.23 20 One 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 21 In 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 22 Formally, the type theories in this book are extended with signatures (Luo 2019a) – see Chapter 2.
26 23 For 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 24 The 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 25 This 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 26 As 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.1 and 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 27 DTS 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 28 It 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 29 See Chapter 2, and sections 2.2 and 2.3 in particular, for more details.
36 30 In this book, the word collection is used to refer to informal entities, rather than their formal representations such as sets or types.
37 31 For details, see Chapter 2 and related references for MTTs.
38 32 It 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.
39 33 Note that MTT-semantics itself is still denotational (and model-theoretic – see below) in the sense that the meaning of a natural language phrase/sentence is given by its denotation in an MTT, not directly by proof rules, although its foundational languages have a proof-theoretic meaning theory, as described above in the sense of “logical inferentialism” or “proof-theoretic semantics” (Kahle and Schroeder-Heister 2006). Can we extend logical inferentialism to natural language? For example, Francez and his colleagues (Francez 2015) have studied natural language semantics in a way that directly adopts the methodology of proof-theoretic semantics for logical systems and applies it to natural language. However, in order for such semantics to be adequate or viable for natural language, one would have to answer some difficult questions. For example, for a logical language, logicians have recognized that, to capture the meaning of a formula in the use theory, it is central for us to spell out two aspects of its use – how to prove it and how to derive consequences from it, as captured by introduction and elimination rules, respectively. Could this be generalized directly to natural language? This would be a big leap and, unfortunately, a convincing justification has not been forthcoming. In fact, philosophers such as Brandom
