Resolving Modal Anaphora in Dependent Type Semantics

Abstract

This paper presents an analysis of modal subordination in the framework of Dependent Type Semantics, a framework of natural language semantics based on dependent type theory. Dependent types provide powerful type structures that have been applied to various discourse phenomena in natural language, yet there has been little attempt to produce an account of modality and its interaction with anaphora from the perspective of dependent type theory. We extend the framework of Dependent Type Semantics with a mechanism of handling explicit quantification over possible worlds, and show how modal anaphora and subordination can be handled within this framework.

These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

1 Introduction

Modal anaphora and subordination have been extensively studied within model-theoretic approaches to discourse semantics, including Discourse Representation Theory (DRT) and Dynamic Semantics (Roberts [13], Frank and Kamp [7], van Rooij [15], Asher and McCready [1]). In contrast, proof-theoretic approaches to natural language semantics have been developed within a framework of dependent type theory and have been applied to dynamic discourse phenomena (Sundholm [17], Ranta [12]). The proof-theoretic framework is attractive in that entailment relations can be directly computed without referring to models; it provides a foundation of computational semantics that can be applied to the problems of natural language inference and of recognizing textual entailment using modern proof assistants (Chatzikyriakidis and Luo [5]). However, there has been little attempt to produce an account of modality and its interaction with anaphora from the perspective of dependent type theory, or more generally, from a proof-theoretic perspective on natural language semantics. Here we provide such an account: we present an analysis of modal subordination (MS) within a framework of proof-theoretic natural language semantics called Dependent Type Semantics (DTS).

There are at least three possible approaches to treating modality in natural language from a proof-theoretic perspective. One is to construct a proof system for natural language inference that contains modal expressions as primitive; the program of natural logic (e.g. Muskens [11]) can be regarded as an instance of this approach. As far as we can see, however, the treatment of discourse phenomena such as anaphora and presupposition in this approach is underdeveloped; in particular, at the current stage it is not clear how to handle various discourse phenomena in a proof system based on the surface structure of natural language sentences, or, more generally, a variable-free proof system. Another approach is the one proposed by Ranta [12], according to which the notion of contexts in dependent type theory plays a central role in explaining modal constructions. A problem with this approach is that the single notion of context seems to be insufficient to account for various kinds of modal expressions in natural language, including epistemic and deontic modality as well as a variety of propositional attitudes. The third approach is to analyze modality in terms of explicit quantification over possible worlds using dependent type theory. This approach enables us to make use of the findings that have been accumulated in formal semantics of natural language over past half a century. We adopt this explicit approach to modal semantics and attempt to integrate these findings with the framework of DTS. This will enable us to handle modals, conditionals and attitude verbs in a unified framework and thereby to broaden the empirical coverage of DTS.

This paper is structured as follows. Section 2 motivates our proof-theoretic approach to the phenomena of MS. Section 3 provides an overview of the framework of DTS, and then, in Sect. 4, we extend it with modal semantics and present an analysis of MS in terms of dependent types. Section 5 extends our approach to the analysis of conditionals. Section 6 provides a dynamic lexicon and compositional analysis in a setting of categorial grammar.

2 Modal Subordination

The phenomena known as MS were first investigated by Roberts [13] in the framework of DRT. A characteristic of MS is that, as is exemplified in the contrast shown in (1), modal expressions like might introduce a proposition that is passed to a subsequent modal discourse but not to a discourse with factual mood.

Note that even if the indefinite a wolf in (1a) is interpreted as taking scope under the modal might, the modal would enables the pronoun it to pick up its antecedent. The intended reading of the second sentence in (1a) can be paraphrased as If a wolf entered, it would growl. The problem can be formulated as follows: how to explain the following valid pattern of inference under the intended reading?

Schematically, the problem can also be formulated as: how to derive $\mathsf {if}\, \varphi , \mathsf {modal_2}\, \psi$ from the discourse $\mathsf {modal_1}\, \varphi .\, \mathsf {modal_2}\, \psi$ in terms of some reasoning mechanism, where $\mathsf {modal_1}$ and $\mathsf {modal_2}$ are suitable modal expressions. A desirable account has to be powerful enough to provide such a derivation, while it must be suitably constrained so as to block the anaphoric link as shown in (1b).

MS also arises with presuppositions. Consider the following sentence with a classical example of presupposition trigger (van Rooij [15]).

Here the presupposition trigger stopped occurs in a modal environment, and carries a presupposition which is successfully satisfied by the proposition introduced by the antecedent clause having a modal force. Though there is a difference in the ways presupposition and anaphora are resolved (see e.g., Geurts [8]), henceforth we use “anaphora” as a cover term for both pronominal anaphora and presupposition.

Roberts [13, 14] developed an account based on accommodation of the antecedent clause $\mathsf {If}\ \varphi$ in the schematic representation mentioned above. Subsequent authors criticized this approach mainly on the grounds that the process of accommodation is too unconstrained and hence over-generates; since then, various theories of MS have been developed in a model-theoretic tradition, in particular, in the framework of DRT (Frank and Kamp [7]; Geurts [8]) and Dynamic Semantics (van Rooij [15]; Asher and McCready [1]).

In addition to the general attractiveness of a proof-theoretic approach to natural language inference, let us mention an advantage of handling MS from the perspective emphasizing the role of inference in resolving anaphora. A problem with the treatment of anaphora in model-theoretic approaches including DRT and Dynamic Semantics is that they do not do justice to the fact that anaphora resolution often requires the hearer to perform inference. A typical example of such a case is one involving the so-called bridging inference (Clark [6]). The following is an example of the interaction of MS and bridging.

The definite description the front door in the second sentence does not have an overt antecedent, but a suitable antecedent is easily inferred using the commonplace assumption that a house has a front door. According to the standard account in DRT and Dynamic Semantics, the presupposed information is identified with some element present in the previous discourse or copied in a suitable place via accommodation. However, examples such as (4) suggest that resolving anaphora is not simply a matter of matching or adding information; rather, it crucially involves inferences with assumptions that are not directly provided in a discourse.¹ The proof-theoretic approach provides a well-developed proof system that accounts for the fact that inferences with implicit assumptions play a crucial role in identifying the antecedent of anaphora.

3 Dependent Type Semantics

DTS (Bekki [2]) is a framework of natural language semantics that extends dependent type theory with a mechanism of context passing to account for anaphora resolution processes and with a component to derive semantic representations in a compositional way.

The syntax is similar to that of dependent type theory [10], except it is extended with an @-term that can be annotated with some type $\varLambda$, written as $@_i^\varLambda$. The syntax for raw terms in DTS is specified as follows.²

We will often omit type $\tau$ in $(\lambda x : \tau ) M$ and abbreviate $(\lambda x_1)\ldots (\lambda x_n) M$ as $(\lambda x_1 \ldots x_n) M$.

The type constructor $\varSigma$ is a generalized form of the product type and serves as an existential quantifier. An object of type $(\varSigma x : A) B(x)$ is a pair (m, n) such that m is of type A and n is of type B(m). Conjunction (or, product type) $A \wedge B$ is a degenerate form of $(\varSigma x:A)B$ if x does not occur free in B. $\varSigma$-types are associated with projection functions $\pi _1$ and $\pi _2$ that are computed with the rules $\pi _1 (m, n) \equiv m$ and $\pi _2 (m, n) \equiv n$, respectively.

The type constructor $\varPi$ is a generalized form of functional type and serves as a universal quantifier. Implication $A \rightarrow B$ is a degenerate form of $(\varPi x:A)B$ if x does not occur free in B. An object of type $(\varPi x : A) B(x)$ is a function f such that for any object a of type A, f a is an object of type B(a). See e.g., Martin-Löf [10] and Ranta [12] for more details and inference rules for $\varPi$-types and $\varSigma$-types.

DTS is based on the paradigm of the Curry-Howard correspondence, according to which propositions are identified with types; the truth of a proposition is then defined as the existence of a proof (i.e., proof-term) of the proposition. In other words, for any (static) proposition P, we can say that P is true if and only if P is inhabited, that is, there exists a proof-term t such that t : P. In this paper, we will denote the type of (static) proposition by $\mathsf {prop}$.

A dynamic proposition in DTS is a function mapping a proof c of a static proposition $\gamma$, a proposition representing the preceding discourse, to a static proposition; hence it has type $\gamma \!\rightarrow \! \mathsf {prop}$. Such a proof c is called a context. For instance, a sentence a man entered is represented as

where $\mathsf {E}$ is a type of entities and c is a variable for a given context. In this case, the sentence does not have any anaphora or presupposition trigger; accordingly, the variable c does not appear in the body of the representation. A sentence containing an anaphoric element is represented using an @-term. For instance, the sentence he whistled is represented as $(\lambda c)\,\mathsf {whistle}(@_0\!^{\gamma _0 \rightarrow \mathsf {E}}c)$, where the annotated term $@_0^{\gamma _0 \rightarrow \mathsf {E}}$ corresponds to the pronoun he. Here $\gamma _0$ is the type of the context variable c. The term $@_0^{\gamma _0 \rightarrow \mathsf {E}}$ will eventually be replaced by some term A having the annotated type $\gamma _0 \!\rightarrow \! \mathsf {E}$, in which case, we say that the @-term is bound to A.

Two dynamic propositions are conjoined by dynamic conjunction, defined as:

Here the information from the left context, represented as a proof term c, is passed to the first conjunct M. Then the second conjunct N receives the pair (c, u), where the proof term u represents the information from M. As a result, an anaphoric element in N can refer to an object introduced in the left context as well as that introduced in M.

As an illustration, let us consider how to derive the following simple inference:

By dynamic conjunction, the semantic representations for a man entered and he whistled are merged into the following:

How to resolve the type $\gamma _0$ and the term $@_0^{\gamma _0 \rightarrow \mathsf {E}}$ can be inferred based on a type checking algorithm (see Bekki [2]). In the present case, given that $@_0^{\gamma _0 \rightarrow \mathsf {E}}$ takes the pair (c, v) as an argument, one can infer that $\gamma _0$ is set to

and that a term that can be substituted for $@_0^{\gamma _0 \rightarrow \mathsf {E}}$ is $\pi _1 \pi _1 \pi _2$. The resulting representation reduces to the following:

This gives the semantic representation after anaphora resolution (in terms of the substitution of $@_0$ for $\pi _1 \pi _1 \pi _2$) for the discourse which appears as a premise in (7). Let us assume that the conclusion of (7) is represented as:

Then, it is easily checked that given an initial context c, if the body of the representation in (10) is true, the proposition in (11) is true as well; in other words, from the given assumption, one can construct a proof-term for (11). In this way, we can derive the inference in (7).

To see how anaphora resolution interacts with inferences involving implicit assumptions, consider a simple example of bridging:

The second sentence can be represented as $(\lambda c) \mathsf {blue}\, \pi _1 (@_0^{\gamma _0 \rightarrow (\varSigma x: \mathsf {E})\, \mathsf {door}\,x}c)$, where the definite description the door is represented by the first projection of the annotated @-term applied to a given context c. The annotated type

$$\begin{aligned} \gamma _0 \rightarrow (\varSigma x: \mathsf {E})\, \mathsf {door}\, x \end{aligned}$$

means that the definite article the selects a pair having the type $(\varSigma x: \mathsf {E})\, \mathsf {door}\, x$ from a context of type $\gamma _0$. Such a pair consists of some entity x and a proof that x is a door, and its first projection, i.e., an entity x, is applied to the predicate $\mathsf {blue}$. This means that for the whole term to be typable, one needs to give a proof of the existence of a door. Intuitively, this captures the existence presupposition triggered by the definite description the door.

In the same way as (8) above, the two sentences in (12) are conjoined by dynamic conjunction and reduced to the following, with an initial context c:

Given that the annotated @-term takes a pair (c, v) as an argument, one can infer that $\gamma _0$ is $\gamma \wedge (\varSigma u\!:(\varSigma x\!:\mathsf {E})\, \mathsf {house}\, x)\, \mathsf {have}\, (\mathsf {j}, \pi _1 u)$. Thus given a term (c, v) of this type, the @-term requires to construct an object of type $(\varSigma x: \mathsf {E})\, \mathsf {door}\, x$. Let us assume that judgement $f : (\varPi x\!: \mathsf {E})(\mathsf {house}\, x \rightarrow (\varSigma y\!: \mathsf {E})(\mathsf {door}\, y \wedge \mathsf {have}(x,y)))$ is taken as an axiom in the global context that represents our commonplace knowledge. Let t be a term $f(\pi _1 \pi _1 \pi _2 (c,v))(\pi _2 \pi _1 \pi _2 (c,v))$. Then, it can be easily verified that t is of type $(\varSigma y\!: \mathsf {E})(\mathsf {door}\, y \wedge \mathsf {have}(\pi _1 \pi _1 v,y))$, and hence, $(\pi _1 t, \pi _1 \pi _2 t)$ has the required type $(\varSigma x: \mathsf {E})\, \mathsf {door}\, x$. By taking the first projection of this pair, one can eventually obtain the following proposition:

$$\begin{aligned} (\varSigma v\!:(\varSigma u\!:(\varSigma x\!:\mathsf {E})\, \mathsf {house}\, x)\, \mathsf {have}\, (\mathsf {j}, \pi _1 u))\, \mathsf {blue} (\pi _1 f (\pi _1 \pi _1 v)(\pi _2 \pi _1 v)). \end{aligned}$$

This can be read as A door of John’s house is blue, which captures correct information derivable from the discourse in (12).

4 Modality and Modal Subordination in DTS

To represent modal propositions in DTS, we parameterize propositions over worlds and contexts. Let $\mathsf {W}$ be a type of worlds and $\gamma$ a type of contexts. Then dynamic propositions have type $\mathsf {W} \rightarrow \gamma \rightarrow \mathsf {prop}$, abbreviated henceforth as $\kappa$. Let M, N be of type $\kappa$. We define $\Diamond$ (epistemic possibility), $\Box$ (epistemic necessity), ;  (dynamic conjunction), and $\triangleright$ (dynamic implication) as follows:

$$\begin{aligned} \Diamond M \equiv&\ (\lambda w c) (\varSigma w' : \mathsf {W}) (\mathsf {R_{epi}}\,ww' \wedge M w' c) \\ \Box M \equiv&\ (\lambda w c) (\varPi w' : \mathsf {W}) (\mathsf {R_{epi}}\,ww' \!\rightarrow \! M w' c)\\ M \, ; N \equiv&\ (\lambda w c) (\varSigma u : Mwc) N w (c,u) \\ M \triangleright N \equiv&\ (\lambda w c) (\varPi u : Mwc) N w (c,u) \end{aligned}$$

Since our focus is on the phenomena of MS, we take epistemic accessibility relation $\mathsf {R_{epi}}$ as primitive and remain neutral with respect to the particular analysis of it.³

Let $\mathsf {rprop}$ be a subtype of propositions with the axiom $p : \mathsf {rprop} \rightarrow \mathsf {prop}$. Intuitively, $\mathsf {rprop}$ denotes a class of root propositions, i.e., propositions embedded under modal operators and introduced as hypothetical ones by modal sentences. Type $\mathsf {W} \!\rightarrow \! \gamma \!\rightarrow \! \mathsf {rprop}$ of parameterized root proposition will be abbreviated as $\widehat{\kappa }$. Then we have $(\lambda g w c) p(gwc) : \widehat{\kappa }\!\rightarrow \! \kappa$. The function $(\lambda g w c) p(gwc)$, which maps a parameterized root proposition to a parameterized proposition, will be abbreviated as $^{\downarrow }{(\cdot )}$. Now might A and would A, where A is of type $\kappa$, are defined as follows:⁴

$$\begin{aligned}{}[\![ might ]\!] (A)&= (\lambda wc)(\Diamond (^{\downarrow }{(}@_i c) \, ; A) wc \wedge (\varSigma P : \widehat{\kappa }) (^{\downarrow }{P} =_{\kappa }\,^{\downarrow }{(}@_i c) \,; A)) \\ [\![ would ]\!] (A)&= (\lambda wc)(\Box (^{\downarrow }{(}@_i c) \triangleright A) wc \wedge (\varSigma P : \widehat{\kappa }) (^{\downarrow }{P} =_{\kappa } \,^{\downarrow }{(}@_i c) \,; A)) \end{aligned}$$

For brevity, here and henceforth we usually omit the annotated type ending with $\widehat{\kappa }$ and write $@_i$ for $@_i ^ {\gamma \rightarrow \widehat{\kappa }}$.

As usual, might and would are analyzed as involving existential and universal quantification over worlds, respectively. One difference from the standard account is that modal operators involve an @-term that triggers anaphoric reference to an antecedent parameterized root proposition of type $\widehat{\kappa }$. This is because we have to take into account discourse meaning: if there is a root proposition of type $\widehat{\kappa }$ introduced in the previous modal context, it can be anaphorically picked up by the @-term and embedded in the restrictor of the modal operator, i.e., in the position before dynamic conjunction or dynamic implication. The right conjuncts of the definitions introduce such a root proposition of type $\widehat{\kappa }$ in terms of $\varSigma$ types. Thus, modal operators can both receive and introduce a hypothetical proposition. Together with the context-passing mechanism of DTS, this enables us to handle cross-sentential anaphora resolution.

To represent the empty modal context, we let $\mathbb {T} : \mathsf {rprop}$ and $f(\mathbb {T}) = \top$, where $\top$ is a unit type with the unique element $\star : \top$. Then we have $^{\downarrow }{(\lambda wc)\,\mathbb {T} =_{\kappa } (\lambda wc)\top }$, where $(\lambda wc)\top$ is used to represent the empty non-modal dynamic context and abbreviated as $\varepsilon$. If there is no appropriate antecedent for $@_i$, for example, if a sentence is uttered in a null context, $@_i$ can be bound to $(\lambda xwc)\, \mathbb {T}$ of type $\gamma \rightarrow \widehat{\kappa }$, and we can obtain $^{\downarrow }{(}@_i c) = \varepsilon$.

As an illustration, consider how to derive the basic inference in (2). The two sentences in the premise are conjoined as

where A is short for

and B for

both being of type $\kappa$. Note that the type of entities, $\mathsf {E}$, is parameterized over worlds. Thus, a one-place predicate, say $\mathsf {wolf}$, has the dependent function type $(\varPi w : \mathsf {W})(\mathsf {E}_w \rightarrow \gamma \rightarrow \mathsf {prop})$, instead of the function type $\mathsf {E} \rightarrow \gamma \rightarrow \mathsf {prop}$.

By binding the @-term occurring in $[\![ might ]\!]$ to the empty informational context, the representation can be reduced as follows:

$$\begin{aligned}&[\![ might ]\!] (A) \, ; \, [\![ would ]\!] (B) \\&\ \equiv \ (\lambda wc)(\varSigma u : (\Diamond (\varepsilon \,; A) wc \wedge (\varSigma P : \widehat{\kappa }) (^{\downarrow }{P} =_{\kappa } \,\varepsilon \,; A))) \\ {}&\qquad (\Box (^{\downarrow }{(}@_0 (c,u)) \triangleright \, B) w(c,u) \wedge (\varSigma Q : \widehat{\kappa }) (^{\downarrow }{Q} =_{\kappa } \,^{\downarrow }{(}@_0 (c,u)) \,; B)) \end{aligned}$$

Here $@_0$ can be bound to $\pi _1 \pi _2 \pi _2$, resulting in the following (parameterized) proposition:

$$\begin{aligned}&(\lambda wc)(\varSigma u \!:\! (\Diamond (\varepsilon \,; A) wc \wedge (\varSigma P : \widehat{\kappa }) (^{\downarrow }{P} =_{\kappa } \varepsilon \,; A))) \\&\qquad \qquad \quad (\Box (^{\downarrow }{(}\pi _1 \pi _2 u) \triangleright \, B) w(c,u) \wedge (\varSigma Q \!:\! \widehat{\kappa }) (^{\downarrow }{Q} =_{\kappa }\,\!\! ^{\downarrow }{(}\pi _1 \pi _2 u) \,; B)). \end{aligned}$$

This gives the semantic representation for the premise in (2) after anaphora resolution. Given a world w and an initial context c, suppose that the proposition in the premise is true, i.e., there is a term t such that

$$\begin{aligned}&t : (\varSigma u \!:\! (\Diamond (\varepsilon \,; A) wc \wedge (\varSigma P : \widehat{\kappa }) (^{\downarrow }{P} =_{\kappa } \varepsilon \,; A))) \\&\qquad \qquad \quad (\Box (^{\downarrow }{(}\pi _1 \pi _2 u) \triangleright \, B) w(c,u) \wedge (\varSigma Q \!:\! \widehat{\kappa }) (^{\downarrow }{Q} =_{\kappa }\,\!\! ^{\downarrow }{(}\pi _1 \pi _2 u) \,; B)). \end{aligned}$$

Then we have

$$\begin{aligned} \pi _2 \pi _2 \pi _1\, t :\, ^{\downarrow }{(}\pi _1 \pi _2 \pi _1 t) =_{\kappa } \varepsilon \,; A \end{aligned}$$

and

$$\begin{aligned} \pi _1 \pi _2\, t : \Box (^{\downarrow }{(\pi _1 \pi _2 \pi _1 t)} \triangleright B) w (c, \pi _1 t). \end{aligned}$$

Thus we obtain $\pi _1 \pi _2\, t : \Box ((\varepsilon \,; A) \triangleright B) w (c, \pi _1 t)$. By unfolding $\Box$, $;\,$, $\triangleright$, A, and B, we obtain:

$$\begin{aligned}&\pi _1 \pi _2\, t : (\varPi w' : \mathsf {W}) (\mathsf {R_{epi}}\,ww' \!\rightarrow \! (\varPi u : (\top \wedge (\varSigma x : \mathsf {E}_{w'}) (\mathsf {wolf}_{w'}\, x \wedge \mathsf {enter}_{w'}\, x))) \\&\qquad \qquad \quad \mathsf {growl}_{w'} (@_1^{\gamma _1 \rightarrow \mathsf {E}_{w'}}((c, \pi _1 t),u))). \end{aligned}$$

Here $@_1$ can be bound to $\pi _1 \pi _2 \pi _2$, thus we have

$$\begin{aligned}&\pi _1 \pi _2\, t : (\varPi w' : \mathsf {W}) (\mathsf {R_{epi}}\,ww' \!\rightarrow \! \\&\qquad \qquad \quad (\varPi u : (\top \wedge (\varSigma x : \mathsf {E}_{w'}) (\mathsf {wolf}_{w'}\, x \wedge \mathsf {enter}_{w'}\, x)))\, \mathsf {growl}_{w'} (\pi _1 \pi _2 u)). \end{aligned}$$

The resulting proposition can be read as If a wolf entered, it would growl. In this way we can derive the inference in (2).

An advantage of the present analysis is that no extension is needed to block anaphoric link as shown in (1b). In the discourse in (1b), the first sentence introduces an entity of type $\mathsf {E}_{w'}$, where $w'$ is a world accessible from the current world w. However, the pronoun in the second sentence has the annotated term $@_1^{\gamma _1 \rightarrow \mathsf {E}_w}$ that requires an entity of type $\mathsf {E}_w$ as an antecedent, and hence, it fails to be bound.

Another advantage is that the present analysis can be applied to modal subordination phenomena involving presupposition. For instance, in the case of (3), the object argument of stopped can be analyzed as involving the @-term annotated with the type that specifies the relevant presupposition, say, $\mathsf {used\_to}_w (\mathsf {smoke}_w\, x)$. Nested presuppositions and “quantifying in to presuppositions” (i.e., presuppositions containing a free variable) can also be dealt with in this approach.⁵ We leave a detailed analysis of presuppositional inferences for another occasion.

It is not difficult to see that the interaction of MS and bridging inferences as exemplified in (4) can be dealt with by combining the analysis given to the simple case in (12) and the mechanism to handle MS presented in this section. In the case of (4), the representation like (13) is embedded in the scope of modal operator would; then the @-term in its restrictor can find an antecedent root proposition introduced in the previous modal sentence. This ensures that the whole discourse implies that the proposition If John had a new house, the front door would be blue is true.

The analysis so far has been confined to epistemic modality, but it can be readily extended to other kinds of modal expressions, including attitude verbs, by giving suitable accessibility relations. For instance, using the deontic accessibility relation $\mathsf {R_{deon}}$, deontic modals can be analyzed along the following lines:

$$\begin{aligned}&[\![ should ]\!] (A) \\&= \, (\lambda wc)(\varPi w'\!:\mathsf {W})((\mathsf {R_{deon}}ww' \rightarrow (^{\downarrow }{(@_i c)} \triangleright A)w'c) \wedge (\varSigma P : \widehat{\kappa }) (^{\downarrow }{P} =_{\kappa } \,^{\downarrow }{(}@_i c) \,; A)) \\&[\![ may ]\!] (A) \\&= \, (\lambda wc)(\varSigma w'\!:\mathsf {W})((\mathsf {R_{deon}}ww' \wedge (^{\downarrow }{(@_i c)} \,; A)w'c) \wedge (\varSigma P : \widehat{\kappa }) (^{\downarrow }{P} =_{\kappa } \,^{\downarrow }{(}@_i c) \,; A)) \end{aligned}$$

Note that the present analysis does not prevent anaphoric dependencies (in terms of @-terms) from being made between different kinds of modalities. For example, a hypothetical proposition of type $\widehat{\kappa }$ introduced by a deontic modal can be picked up by the @-term in a subsequent sentence with an epistemic modal. Although the issues surrounding what kinds of modality support modal subordination are complicated, modal subordination phenomena can occur between different kinds of modality, as witnessed by the following example (Roberts [14]).

Here, an anaphoric dependency is made between deontic and epistemic modalities. The analysis presented above can capture this kind of dependency.

We agree with Roberts [14] that the infelicity of the example like (15b) is accounted for, not directly by entailment relations induced by attitude verbs, but by pragmatic considerations pertaining to anaphora resolution.

As is indicated by the treatment of bridging inferences, the proof-theoretic framework presented here is flexible enough to handle the interaction of entailment and anaphora resolution. We leave a detailed analysis of the interaction of attitude verbs and MS for another occasion.

5 Conditionals

The present analysis can be naturally extended to handle examples involving conditionals like (16):

Following the standard assumption in the literature (cf. Kratzer [9]), we assume:

• (i) A modal expression is a binary propositional operator having the structure $\mathsf {modal}\,(\varphi , \psi )$, where $\varphi$ is a restrictor and $\psi$ is a scope.

• (ii) if-clause contributes to a restrictor of a modal expression, i.e., $\mathsf {If}$ $\varphi$, $\mathsf {modal}$ $\psi$ is represented as $\mathsf {modal}\, (\varphi , \psi )$;

• (iii) If a modal expression is left implicit as in the first sentence in (16a), it is assumed by default that it has universal modal force: $\mathsf {If}$ $\varphi$, $\psi$ is represented as $\Box (\varphi , \psi )$.

Binary modal operators then are analyzed as follows.

$$\begin{aligned}&[\![ might ]\!] (A, B) \\&= (\lambda wc)(\Diamond ((^{\downarrow }{(}@_i c) \,; A) \, ; B) \, wc \, \wedge \, (\varSigma P : \widehat{\kappa }) (^{\downarrow }{P} =_{\kappa } (^{\downarrow }{(}@_i c) \,; A) ; B)) \\&[\![ would ]\!] (A, B) \\&= (\lambda wc)(\Box ((^{\downarrow }{(}@_i c) \,; A) \triangleright B) \, wc \, \wedge \, (\varSigma P : \widehat{\kappa }) (^{\downarrow }{P} =_{\kappa } (^{\downarrow }{(}@_i c) \,; A) ; B)) \end{aligned}$$

Both would and might introduce a (parameterized) propositional object P of type $\widehat{\kappa }$, which inherits the content of the antecedent A as well as the consequent B. This object is identified with $(^{\downarrow }{(}@_i c) \,; A) \,; B$. Now it is not difficult to derive the following pattern of inference under the current analysis.

A compositional analysis of conditionals will be provided in the next section.

According to the present analysis, the antecedent $\varphi _1$ in $\mathsf {If}$ $\varphi _1$, $\mathsf {would}$ $\varphi _2$ is passed to the first argument of the binary modal operator $[\![ would ]\!]$. Here it is worth pointing out an alternative analysis that attempts to establish the relationship between an if-clause and a modal expression in terms of @-operators. According to the alternative analysis, the semantic role of if-clause is to introduce a propositional object in terms of $\varSigma$-type:

$$\begin{aligned}{}[\![ if ]\!] (A) = (\lambda wc) (\varSigma P : \widehat{\kappa }) (^{\downarrow }{P} =_{\kappa }\,\! ^{\downarrow }{(}@_i c) \, ; A) \end{aligned}$$

Modal expressions are taken as unary operators: the definition is repeated here.

$$\begin{aligned}{}[\![ might ]\!] (A) =&(\lambda wc)(\Diamond (^{\downarrow }{(}@_i c) \, ; A) \, wc \, \wedge \, (\varSigma P : \widehat{\kappa }) (^{\downarrow }{P} =_{\kappa }\,\! ^{\downarrow }{(}@_i c) \, ; A)) \\ [\![ would ]\!] (A) =&(\lambda wc)(\Box (^{\downarrow }{(}@_i c) \triangleright A) \, wc \, \wedge \, (\varSigma P : \widehat{\kappa }) (^{\downarrow }{P} =_{\kappa }\,\! ^{\downarrow }{(}@_i c) \, ; A)) \end{aligned}$$

Then the if-clause and the main clause are combined by dynamic conjunction:

$$\begin{aligned}{}[\![ if \,A, \, would \, B ]\!] = [\![ if \, A ]\!] \, ; [\![ would \, B ]\!] \end{aligned}$$

The @-term in $[\![ would \, B ]\!]$ can be bound to the root proposition introduced in $[\![ if \, A ]\!]$, hence we can obtain the same result as the first approach. An advantage of this alternative approach is that it simplifies the semantics of modal expressions might and would by taking them as unary operators and reducing the role of restrictor arguments to @-operators. However, one drawback is that it allows the @-operator associated with a modal expression to be bound by a proposition other than the one introduced by the if-clause: the @-operator can in principle be bound by any proposition of type $\widehat{\kappa }$ appearing in a suitable antecedent context. According to the first approach, in contrast, the binary would has the representation $((^{\downarrow }{(}@_i c) \,; A) \triangleright B)$, where $@_i c$ is responsible for capturing the information given in a context and A for the information given in the if-clause. In this way, we can distinguish two aspects of the meaning of a conditional, i.e., grammatically determined meaning and contextually inferred meaning. For this reason, we adopt the first approach in this paper.

6 Compositional Analysis

In this section, we give a compositional analysis of constructions involving modal anaphora and subordination we discussed so far. To be concrete, we will adopt Combinatory Categorial Grammar (CCG) as our syntactic framework (see Steedman [16] for an overview). Generally speaking, categorial grammar can be seen as a framework based on the idea of direct compositionality, i.e., the idea of providing a compositional derivation of semantic representations based on surface structures of sentences. To provide a compositional analysis of modal constructions in such a setting is not a trivial task, since modal auxiliaries tend to take a scope that is unexpected from their surface position.

Consider again the initial example in (1a), repeated here as (18).

We are concerned with the reading of (18a) in which a wolf is interpreted as de dicto, i.e., as taking narrow scope with respect to the modal might. The issue of how to analyze the de re reading in which the subject NP takes scope over the modal seems to be orthogonal to the issue of how to handle modal subordination phenomena, so we leave it for another occasion.

A lexicon for the compositional analysis of (18) and related constructions is given in Table 1. Here we will write VP for $S\,\backslash NP$. In CCG, function categories of the form X / Y expect their argument Y to its right, while those of the form $X\backslash Y$ expect Y to their left. The forward slash  /  and the backward slash $\backslash$ are left-associative: for example, S / VP / N means (S / VP) / N.

Table 1. Dynamic lexicon of DTS for basic modal semantics

The lexical entries provided here yield the following derivation tree for (18a).

Given this derivation tree, the semantic representation for (18a) is derived in the following way.

$$\begin{aligned}&[\![ a_{nom} ]\!] ([\![ wolf ]\!]) \\&\equiv _\beta (\lambda vwc)(\varSigma u : (\varSigma x : \mathsf {E}_w)(\mathsf {wolf}_w x))(vw (\pi _1 u)(c,u)) \\&[\![ might^\mathrm{1} ]\!] ([\![ enter ]\!]) \\&\equiv _{\beta } (\lambda qwc)((\varSigma w' : \mathsf {W})(\mathsf {R_{epi}}\,ww' \wedge \, (^{\downarrow }{(}@_1 c) \, ; q(\lambda wxc)(\mathsf {enter}_w x))w'c) \\&\qquad \wedge (\varSigma P : \widehat{\kappa }) (^{\downarrow }{P} =_{\kappa } \,^{\downarrow }{(}@_1 c) \,; q(\lambda wxc)(\mathsf {enter}_w x))) \end{aligned}$$

Let $@_1$ be bound to the empty context, i.e., $^{\downarrow }{(}@_1 c) = \varepsilon$. For simplicity, henceforth we will omit $\varepsilon$ and $\top$ throughout this section.

$$\begin{aligned}&[\![ might^\mathrm{1} ]\!] ([\![ enter ]\!])([\![ a_{nom} ]\!] ([\![ wolf ]\!])) \\&\equiv _{\beta } (\lambda wc)((\varSigma w' : \mathsf {W})(\mathsf {R_{epi}}\,ww' \wedge \, (\varSigma u : (\varSigma x : \mathsf {E}_{w'})(\mathsf {wolf}_{w'} x))(\mathsf {enter}_{w'} (\pi _1 u))) \\&\qquad \wedge (\varSigma P : \widehat{\kappa }) (^{\downarrow }{P} =_{\kappa } \, (\lambda wc)(\varSigma u : (\varSigma x : \mathsf {E}_w)(\mathsf {wolf}_w x))(\mathsf {enter}_w (\pi _1 u)))) \end{aligned}$$

The derivation tree of (18b) is given as follows.

The semantic representation of (18b) is derived in a similar way. Note that the pronoun it here is interpreted, in a sense, as de dicto, taking scope under the modal would.

$$\begin{aligned}&[\![ would^\mathrm{2} ]\!] ([\![ growl ]\!])([\![ it^\mathrm{3}_{nom} ]\!]) \\&\equiv _{\beta } (\lambda wc)((\varPi w' : \mathsf {W})(\mathsf {R_{epi}}\,ww' \rightarrow \, (^{\downarrow }{(}@_2 c) \, ; (\lambda wc) (\mathsf {growl}_w (@_3^{\gamma \rightarrow \mathsf {E}_w}c))) w'c) \\&\qquad \wedge (\varSigma P : \widehat{\kappa }) (^{\downarrow }{P} =_{\kappa } \, ^{\downarrow }{(}@_2 c) \, ; (\lambda wc) (\mathsf {growl}_w (@_3^{\gamma \rightarrow \mathsf {E}_w}c))))) \end{aligned}$$

As is easily checked, combining the semantic representations for (18a) and (18b) by dynamic conjunction yields the same semantic representation as the one for (1a) presented in Sect. 4.

According to the lexicon given in Table 1, the object NP in a modal sentence is interpreted as taking scope under the modal. This enables us to handle the anaphoric dependency in the following discourse.

For the modal subordination reading to be derivable, the pronoun it in object position of (19b) has to be interpreted as taking scope under would. Our lexical entries yield the following derivation tree for (19b).

The semantic representation is derived as follows:

$$\begin{aligned}&[\![ would^\mathrm{1} ]\!]([\![ it^\mathrm{2}_{acc} ]\!]([\![ beat ]\!]))([\![ John ]\!]) \\&\equiv _{\beta } (\lambda wc)((\varPi w' : \mathsf {W})(\mathsf {R_{epi}}\,ww' \rightarrow \, (^{\downarrow }{(}@_1 c) \, ; (\lambda wc) (\mathsf {beat}_w (\mathsf {john},@_2^{\gamma \rightarrow \mathsf {E}_w}c))) w'c) \\&\qquad \wedge (\varSigma P : \widehat{\kappa }) (^{\downarrow }{P} =_{\kappa } \, ^{\downarrow }{(}@_1 c) \, ; (\lambda wc) (\mathsf {beat}_w (\mathsf {john}, @_2^{\gamma \rightarrow \mathsf {E}_w}c))))). \end{aligned}$$

In the same way as the derivation for (18) shown above, this yields the desired reading of the discourse in (19).

For the analysis of the interaction of modals and conditionals, we introduce lexical entries for if and binary modal operators would and might, which are shown in Table 2.

Table 2. Dynamic lexicon of DTS for conditionals

As an illustration, consider the following example.

The derivation tree of (20) is given as follows:

The semantic representation for a farmer owns a donkey is computed as follows:

$$\begin{aligned}&[\![ a_{nom} ]\!] ([\![ farmer ]\!])([\![ owns ]\!]([\![ a_{acc} ]\!]([\![ donkey ]\!])))\\&\equiv _\beta (\lambda wc)(\varSigma v:(\varSigma x:\mathsf {E}_w)( \mathsf {farmer}_w x))(\varSigma u:(\varSigma y:\mathsf {E}_w)(\mathsf {donkey}_w y))\, \mathsf {own}_w(\pi _1 v, \pi _1 u). \end{aligned}$$

Let us abbreviate this representation as A. Then the derivation tree above generates the following semantic representation:

$$\begin{aligned}&[\![ would^\mathrm{2} ]\!]([\![ it^\mathrm{3}_{acc} ]\!]([\![ beat ]\!]))([\![ he^\mathrm{1}_{nom} ]\!])([\![ if ]\!](A))\\&\equiv _\beta (\lambda wc)((\varPi w' : \mathsf {W})(\mathsf {R_{epi}}\,ww' \\&\quad \rightarrow \, ((^{\downarrow }{(}@_{2}c) \, ; A) \, \triangleright (\lambda wc)(\mathsf {beat}_w(@^{\gamma \rightarrow \mathsf {E}_w}_1c, @^{\gamma \rightarrow \mathsf {E}_w}_3c))) w'c)\\&\qquad \wedge \, (\varSigma P : \widehat{\kappa }) (^{\downarrow }{P} =_{\kappa } \,(^{\downarrow }{(}@_{2}c) \,; A)\, ;(\lambda wc)(\mathsf {beat}_w(@^{\gamma \rightarrow \mathsf {E}_w}_1c, @^{\gamma \rightarrow \mathsf {E}_w}_3c)))) \end{aligned}$$

The resulting semantic representation corresponds to the one presented in Sect. 5. Here, the dynamic proposition corresponding to the root sentence he beats it appears in the nuclear scope of the binary modal operator $would$. The dynamic proposition expressed by a farmer owns a donkey in the if-clause fills in the restrictor of would. It can be easily seen that this representation enables the pronouns he and it to establish the intended anaphoric relation to their antecedents.

The unary modal operators might and would shown in Table 1 can be regarded as a special case of the binary modal operators introduced here. We can assume that when modal expressions might and would appear without if-clauses, the restrictor position s in the semantic representation of a binary modal operator is filled by the empty context $\varepsilon$ (which needs to be syntactically realized by a silent element). Although the derivations for examples like (18) and (19) will become more complicated, we can get the desirable semantic representations for all the constructions we examined so far.

7 Conclusion

In this paper, we extended the framework of DTS with a mechanism to handle modality and its interaction with anaphora. In doing so, we integrated the findings of possible world semantics with a proof-theoretic formal semantics based on dependent type theory. This enabled us to give the semantic representations of modals and conditionals using the expressive type structures provided by dependent type theory, and thereby to broaden the empirical coverage of DTS.

There are other important constructions that are relevant to MS but are not discussed in this paper, including negation (Frank and Kamp [7]; Geurts [8]), the so-called Veltman’s asymmetry (Veltman [19]; Asher and McCready [1]), and generics (Carlson and Spejewski [4]). These issues are left for future work.