{'fraction_non_alphanumeric': 0.05534675615212528, 'fraction_numerical': 0.016957494407158838, 'mean_word_length': 4.3844856661045535, 'pattern_counts': {'":': 0, '<': 0, '<?xml version=': 0, '>': 0, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 2, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Donkey Anaphora: Type-Theoretic Semantics with Both Strong and Weak Sums

Donkey sentences are among the challenging examples that present a difﬁcult problem in compositional logical semantics and their semantic treatment is one of the early applications of dependent type theory to linguistic semantics, where the strong sum Σ , rather than weak sums (as given by traditional existential quantiﬁers), is used for existential quantiﬁcation. However, it is known that this method is inadequate because it fails to deal with counting properly. In this paper, we propose to consider the semantics of donkey sentences in a type theory with both strong and weak sums and show that, with both sum operators, donkey sentences can be given adequate semantic interpretations which, in particular, take care of counting properly.


Introduction
Donkey sentences, as first studied by Geach (1962) and exemplified in (1), where an anaphoric expression refers to an existentially quantified entity, are among the challenging examples that present a difficult problem in compositional logical semantics.
(1) Every farmer who owns a donkey beats it.
Their studies (and that of trans-sentential anaphora) have led to the development of dynamic semantics such as DRT (Kamp, 1981) and DPL (Groenendijk and Stokhof, 1991) which, however, require one to consider substantial changes of the underlying logical systems. 1 (For a recent summary of the dynamic approach to donkey anaphora, see Brasoveanu and Dotlacil (2021).) In the mid-80s, as one of the early applications of dependent type theory in logical semantics, researchers such as Mönnich (1985) and Sundholm (1986) have proposed to use Martin-Löf's type theory (Martin-Löf, 1984) to deal with donkey anaphora, where Σ-types are employed to represent existentially quantified formulas. Σ-types Σx:A.P (x) are also called strong sums, as opposed to the traditional existentially quantified formulas ∃x:A.P (x) which are called weak sums, because from an object of the strong sum, one can obtain its witness, by means of a projection operation, while this is not possible for the weak sum. It is because of the availability of witness projection that an anaphoric reference can be obtained from an object of a Σ-type, while this is not possible for an existential quantification in the traditional case (and hence the problem in the first place). However, it is known that this approach of using Σ-types to deal with donkey anaphora suffers from a problem of counting (Sundholm, 1989;Tanaka, 2015) and fails to provide us an adequate solution. (See §2 for more details.) In this paper, we contend that the problem of the above type-theoretical approach has come from a double role played by Σ, as an existential quantifier, on the one hand, and as a structural mechanism to represent collections of objects, on the other. These two roles should be separate and played by different type constructors. But in traditional logics (firstorder logic or simple type theory) or in Martin-Löf's type theory, only either ∃ or Σ exists, not both, and therefore there is no way to consider such a separation. We show that, in a type theory with both strong and weak sums, donkey sentences can be given adequate semantics in which counting is taken into proper account.
Our proposal is also linked to the research on different readings of donkey sentences and, in particular, the strong and weak readings as studied by Chierchia (1990) and others. Also, donkey anaphora are closely related to (and, for some researchers, they are examples of) the so-called E-type anaphora, as first studied by Evans (1977Evans ( , 1980, which may be interpreted by means of descriptions (see, for example, Nouwen (2021) for a recent discussion). It is not surprising that Σ-types are essentially useful in semantic interpretations of donkey sentences since they have close links to descriptions (Martin-Löf, 1984;Carlström, 2005;Mineshima, 2013) and we shall give some brief discussions about this.
Combining strong and weak sums in type theory is a subtle matter that needs us to tread carefully, for otherwise we may easily slip into problems such as inconsistency. We shall discuss this briefly as well.
This is a short version of a paper we plan to write. In this paper, in particular, we shall focus on telling a complete story of this new treatment of donkey anaphora with both strong and weak sums, but shall be brief about or completely omit some related respects.

Strong and Weak Sums in Type Theory
In this section, we explain the concepts of weak sums (for example, traditional existential quantifiers) and strong sums (Σ-types) and, using the notion of the cardinality of a finite type, illustrate the counting problem when using only Σ-types to interpret donkey sentences.
Weak sums (existential quantifiers). Under the Curry-Howard propositions-as-types principle (Curry and Feys, 1958;Howard, 1980), traditional existentially quantified formulas are examples of weak sum types of the form ∃x.P (x). In firstorder logic, depending on whether it is intuitionistic or classical, the existential quantifier can be introduced directly or defined by means of the universal quantifier together with negation, respectively. In higher-order logic (or simple type theory) as used in Montague's semantics, where there is an impredicative type t of all formulas, it can be either directly introduced or defined by means of the universal quantifier as in (2).
It is known that, given a proof of ∃x.P (x), although one knows that there is an entity such that P holds, in the logical calculus one cannot find out which entity it is. It is because of this that an anaphoric reference to an existentially quantified entity becomes problematic. For example, in a traditional compositional semantics, the donkey sentence (1) would obtain (3) as its interpretation, which is not a well-formed formula since the variable y in beat(x, y) is out of the scope of the existential quantifier. ( This illustrates the original problem in interpreting donkey sentences, as mentioned at the beginning of Introduction. Strong sums (Σ-types). Σ is a dependent type constructor. If A is a type and B is a family of types that depend on objects of type A, then Σx:A.B(x) is a type, consisting of pairs (a, b) such that a is of type A and b is of type B(a). Σ-types are associated with the projection operators π 1 and π 2 so that, for (a, b) of type Σx:A.B(x), π 1 (a, b) = a and π 2 (a, b) = b. Formally, Σ-types are governed by the inference rules in Appendix A. Besides being useful mechanisms to organise structures in various applications, Σ-types may also play other roles. For example, in Martin-Löf's type theory, Σ also plays the role of existential quantifier in its logic 2 . Therefore, for instance, the donkey sentence (1) can be interpreted as (4), in which F Σ , as defined in (5), is the type intended to represent the collection of donkey-owning farmers, where F and D are the types that interpret farmer and donkey, respectively. 3 (4) ∀z : F Σ . beat(π 1 (z), π 1 (π 2 (z))) (5) F Σ = Σx:F Σy:D. own(x, y) Σ-types are strong in the sense that from a proof of Σx:A.P (x) one can preform the first projection operation to obtain the witness of this 'existentially' quantified formula and it is because of this, if Σ is used as existential quantifier, one can project out its witness from a proof term of the Σ-type, even outside its scope (the terms π 1 (z) and π 1 (π 2 (z)) in (4) are such examples).
The type F Σ above contains two occurrences of Σ and they play two different roles: the first acts as a structural mechanism to represent the collection of the farmers who own donkeys and the second as the existential quantifier to say that there exists a donkey owned by the farmer concerned. As we shall see below, using Σ to play this double role is problematic. In particular, F Σ is in fact representing a collection whose cardinality (the number of its objects) is different from that of the collection of donkey-owning farmers and, therefore, the semantic interpretation (4) of (1) is inadequate (Sundholm, 1989;. Counting and cardinality of finite types. When a type A is finite in the sense that it has finitely many objects, it is possible to define its cardinanity |A| as the number of its objects. Formally, a type is finite if, for some n, it is isomorphic to F in(n), the type with exactly n objects -see Appendix B. For example, the cardinality of a finite Σ-type is the number of pairs in the type.
The problem of counting can be illustrated by considering the sentence in (6), 4 where the quantifier Every in (1) is replaced by Most. Its formal semantics by means of Σ-types in Martin-Löf's type theory is given in (7), which can be seen obtained by replacing ∀ by the quantifier Most S , which is defined by Sundholm (1989) (S in Most S for Sundholm) so that, for a finite type A, Most S x:A.P (x) is true if, and only if, more than half of the objects in A satisfy P .
(6) Most farmers who own a donkey beat it.
(7) Most S z : F Σ . beat(π 1 (z), π 1 (π 2 (z))) Let us now consider the cardinality of F Σ , as defined in (5). Because of the second Σ in F Σ , |F Σ | is not that of the collection of donkey-owning farmers; instead, to calculate |F Σ |, we'd have to count every triple (x, y, p) of farmers x, donkeys y and proofs p that x owns y. For example, if there are ten farmers, one of whom owns twenty donkeys and beats all of them, and the other nine own one donkey each and do not beat their donkeys. Then, |F Σ | ≥ 29 (it is an inequality because, if farmer x owns donkey y, there may be more than one proof that x owns y), but the number of farmers who do not beat their donkeys is 9. Therefore, the above semantics (7) of (6) would be true in such a case, which is obviously incorrect. 5 3 Donkey Anaphora: a Type-Theoretical Solution with Both Σ and ∃ In this section, we shall first introduce a dependent type theory UTT (Luo, 1994), which has both strong and weak sums, and then show how donkey sentences like (1) and (6) can be interpreted type-theoretically, giving adequate treatments for different readings and taking care of counting in a proper way as well.

UTT: an impredicative type theory
The type structure of UTT (Unifying Theory of dependent Types) (Luo, 1994) consists of two parts: the world of data types and that of logical propositions (see Fig. 1). It contains various types such as dependent product types (Π-types), strong sum types (Σ-types), the type N of natural numbers, the universes T ype i , and many other types. UTT also contains an impredicative type universe P rop of logical propositions which provide means to describe the logical properties of objects of any type (see Appendix C). Formally, UTT can be considered as the combination of Martin-Löf's (intensional) type theory (Martin-Löf, 1975;Nordström et al., 1990) with Coquand-Huet's Calculus of Constructions (Coquand and Huet, 1988). In computer science, type theories such as UTT have been implemented in theorem proving systems (called proof assistants) for formalisation of mathematics and verification of programs, and recently, they have been used for formal reasoning based on linguistic semantics (see, for example, (Chatzikyriakidis and Luo, 2016)). 6 Note that UTT contains both strong sums Σx:A.B(x) (Σ-types, as 'data types') and weak sums ∃x:A.P (x) (existentially quantified types, as logical propositions), and this is essential when considering semantic interpretations of donkey sentences in §3.2 below.
Logic and proof irrelevance. In UTT, a type is a logical proposition if it is of type P rop. The type universe P rop is impredicative and, therefore, the other logical operators can be defined by means of the operator ∀ for universal quantification 7 . For example, the conjunction operator and the existential quantifier ∃ can be defined as in (8) and (9), respectively, and the definitions of the other operators can be found in Appendix C.
The principle of proof irrelevance says that any two proofs of the same logical proposition should be the same. For instance, it implies that, for farmer x and donkey y, any two proof terms of the proposition own(x, y) should be the same. It has been shown that, when employing a type theory for natural language semantics, proof irrelevance should be enforced (Luo, 2012(Luo, , 2019. Note that, because in UTT there is a clear distinction between logical propositions and other types (the former being those of type P rop), it is straightforward to introduce proof irrelevance by means of the following rule (Werner, 2008;Luo, 2012): P : P rop p : P q : P p = q : P Intuitively, it says that, if P is a logical proposition and if p and q are proof terms of P , then p and q are 6 There are several proof assistants based on type theories including Agda (Agda, 2008) based on Martin-Löf's type theory, Coq (Coq, 2010) implementing the type theory pCIC, and Lego/Plastic (Luo and Pollack, 1992;Callaghan and Luo, 2001) implementing UTT. It may be worth remarking that pCIC, implemented in the Coq proof assistant, is very similar to UTT -this is especially the case after Coq's universe Set became predicative in 2004 (it was impredicative in earlier versions). 7 The fact that other logical operators can be defined in higher-order logical systems by means of universal quantifier was discovered in the 60s by Prawitz (1965) (and several others, independently) and, this is the same in an impredicative type theory. the same. In particular, according to the above rule, every proposition of type P rop is either an empty type or a singleton type. In terms of cardinality, we have |P | ≤ 1 for every P : P rop and, therefore, if A is finite and Q : A → P rop is a predicate over A, then we have (10) |Σx:A.Q(x)| ≤ |A|.

Semantics of donkey anaphora in UTT
When a type theory has both strong and weak sums (Σ-types and ∃-propositions as in UTT), together with proof irrelevance, there is a new way to semantically interpret donkey sentences, which takes care of counting adequately. We'll use the example (6), which is repeated as (11) below, to explain.
(11) Most farmers who own a donkey beat it.
In §2, we have shown that, because in Martin-Löf's type theory Σ is used to play a double role, the semantic interpretation (7) of (11) is inadequate because it gets counting wrong. In that definition, we have used quantifier Most S defined in Martin-Löf's type theory and, here, we can define a semantic interpretation of the quantifier most in UTT in a similar fashion as in (Sundholm, 1989) but with a crucial difference: instead of Σ, we shall use ∃ as defined in (9) as the existential quantifier and, intuitively, for a finite A, Most x:A.P (x) also means that more than half of the objects in A satisfy P . Note that, Most S x:A.P (x) is a non-propositional type, but Most x:A.P (x) is a logical proposition of type P rop. (See Appendix D for details.) Having defined Most in UTT, we can now interpret the donkey sentence (11) as (12), in which F ∃ is defined in (13): ∀y : Σy:D.own(π 1 (z), y). beat(π 1 (z), π 1 (y )) (13) F ∃ = Σx:F. ∃y:D.own(x, y) Note that |∃y:D.own(x, y)| ≤ 1, that is, if ∃y:D.own(x, y) is true, the cardinality of the proposition is 1. Therefore, the type F ∃ correctly represents the collection of donkey-owning farmers, as intended, and the above semantics (12) is adequate and, in particular, it deals with counting correctly.
Researchers have studied different readings (in particular, strong and weak readings) of donkey anaphora, as studied by Chierchia (1990Chierchia ( , 1992 and others. For instance, the strong and weak readings of (11) are (14) and (15), respectively: (14) Most farmers who own a donkey beat the donkeys they own.
(15) Most farmers who own a donkey beat some donkeys they own.
The above interpretation (12) of (11) is a strong one, interpreting (14) directly: most donkey-owning farmers beat all donkeys they own. A weaker interpretation of its weak reading (15) would be (16), obtained from (12) by changing ∀ into ∃: (16) Most z : F ∃ . ∃y : Σy:D.own(π 1 (z), y). beat(π 1 (z), π 1 (y )) People have also considered more sophisticated examples where donkey anaphora are involved in various ways. For example, (17) is one of them, taken from Brasoveanu's thesis (Brasoveanu, 2007), in which the readings for the donkey anaphora are different ('a TV' having a strong reading and 'a credit card' a weak one). Its typetheoretical semantics with both strong and weak sums is given in (18).
(17) Every person who buys a TV and has a credit card uses it to pay for it.

E-type anaphora
Here, we discuss, albeit rather briefly, the so-called E-type anaphora to which donkey anaphora are closed related (and, for some researchers, donkey anaphora are examples of E-type anaphora). 8 Etype anaphora are first studied by Evans (1977Evans ( , 1980, and further discussed by many, including (Heim and Kratzer, 1998) among others. They can be interpreted by means of descriptions (Russell, 1905(Russell, , 1919) (see, for example, Nouwen (2021) for a recent discussion). An example, due to Evans,is (19). Note that the pronoun 'they' in (19) is not bound by 'Few' for otherwise the meaning is incorrect. A common conceptual answer, proposed by Evans (1977Evans ( , 1980, is that these pronouns are descriptive in that they can be paraphrased by means of descriptions as exemplified in (20) that paraphrases (19).
(19) Few congressmen admire Kennedy, and they are very junior.
(20) Few congressmen admire Kennedy, and the congressmen that do admire Kennedy are very junior.
As pointed out by Martin-Löf (1984), strong sum types (Σ-types) are related to descriptions, because he regards them as logical propositions as well. If you think that Σx:A.B(x) as the existentially quantified formula, it is strong and therefore its first projection operator π 1 gives us an internal means of obtaining the witness from a proof of the existentally quantified formula. As explained in §2, this is stronger than the traditional existential operator ∃ for which such a projection operator does not exist, and it is exactly because of this that Σ offers a form of description, as pointed out by Martin-Löf (1984) and further studied by Carlström (2005) and Mineshima (2013). For example, the Etype example (19) may be interpreted as (21), either in Martin-Löf's type theory or in UTT, where we assume that the quantifier F ew has been defined: (21) F ew x:C. admire(x, K) ∧ ∀z:[Σx:C.admire(x, K)].junior(π 1 (z)) However, it should be made clear that Σ-types are not the same as traditional existentially quantified formulas and, therefore, it is unclear how far one may go to analyse E-type anaphora by means of Σ-types. Actually, it would not go very far since, as analysed above, using Σ as existential quantifier does cause problems such as counting, which will show up in context of E-type anaphora as well.

Combining Strong and Weak Sums
It is worth mentioning that combining the strong sum (Σ) and the weak sum (∃) in type theory is a subtle matter and, if not careful, it is easy to get into problems. It would be interesting to note that UTT does not have 'Σ-propositions' because the socalled 'large Σ-propositions' would lead to inconsistency and the so-called 'small Σ-propositions' would make the weak sum types become strong. 9 Consider, for example, to add large Σ-types into the impredicative universe P rop by adding the following rule (together with those for its introduction and projections that we omit):

( * )
A type P : A → P rop Σx:A.P (x) : P rop It turns out that such Σ-propositions cannot be consistently added -if they were added using the above rule ( * ) (and related ones), the resulting type theory would be inconsistent in the sense that even the false proposition would become provable (Hook and Howe, 1986;Luo, 1994). One may want to add Σ-propositions (so-called small Σ-types) by a rule like the following, this time restricting A to be a proposition of type P rop: Although the resulting type theory may be consistent 10 , there is another problem: the addition of such small strong sum as propositions in P rop would make the weak sum proposition ∃x:A.P (x) become strong (rather unexpectedly!) in the sense that there is now an internal function in the type theory that, from a proof of ∃x:A.P (x), returns an object a : A such that P (a) holds. That would mean that the traditional existential quantifier is not weak anymore -such a side effect is of course problematic and would make the above interpretation method we have proposed fail to deal with counting correctly. Therefore, neither of the above large or small Σ is a viable possibility and, put in another way, the approach taken in UTT seems to be the only viable approach in combining strong and weak sums.

Concluding Remarks
As a concluding remark, we point out that, in this paper, we have studied a completely proof-theoretic approach. This is rather different from the modeltheoretic approaches that have been considered in the literature (see, for example, Brasoveanu and Dotlacil (2021)). Among other things, this has the advantage of clearer treatment, on the one hand, and enables the use of proof assistants in reasoning, on the other. n : N i : F in(n) succ(n, i) : F in(n + 1) The cardinality of a finite type A, notation |A|, is defined to be n if, and only if, A is isomorphic to F in(n), that is, in the type theory concerned, there is a bijective function between A and F in(n). In particular, |F in(n)| = n, since the identity function over F in(n) is bijective.

C Logic in UTT
The logic in UTT 11 consists of the impredicative universe P rop, specified by the following rules: (P ⇒ X) ⇒ (Q ⇒ X) ⇒ X ¬P = P ⇒ false ∃x : A.P (x) = ∀X : P rop.
(∀x : A.(P (x) ⇒ X)) ⇒ X (a = A b) = ∀P : A → P rop. P (a) ⇒ P (b) 11 One can find its definition in §9.2.1 of (Luo, 1994), where it is specified in terms of the logical framework LF.

D Most in UTT
Let A be a finite type with |A| = n A , P : A → P rop a predicate over A, and F in(n) the types with n objects defined in Appendix B. Then, in UTT, the logical proposition Most x:A.P (x) of type P rop is defined as follows, where inj(f ) is a proposition expressing that f is an injective function: Most x:A.P (x) = ∃k : N. (k ≥ n A /2 + 1) ∧ ∃f :F in(k) → A.