%----*- coding: utf-8 -*-

\subsection{Modal Subordination}

We turn now to our CS analysis of the interdependence of modal facts and MS.   Treating modality as a standard Kripke
operator in DRT makes bad predictions:
\examples{%
  \example{\label{wolf}A wolf might walk in.  It would growl.}%
  \example{\label{wolf'}A wolf might walk in. It *will growl}%
  \example{\label{wolf''}A wolf is outside.  He might growl.}}%
DRT predicts~\exref{wolf'} to be bad and~\exref{wolf''} to be good, as
intuitions warrant.  But it also predicts~\exref{wolf} is bad.  A straightforward
analysis of modality  in DRT produces two subDRSs in the main DRS, making the discourse referents
introduced under the scope of one modal inaccessible to
anaphoric conditions in the main DRS, or to conditions inside
the scope of the second model. This yields bad results.

To address this problem, \citet{roberts89} treats
$\Box$ and $\Diamond$ as generalized quantifiers whose unspecified restrictors can be accommodated in the context.  $\Box \phi$ is
in fact: $\Box(?, \phi)$, with $?$ a \emph{modal base} to be filled in
the context using a proposition within the scope of an appropriate
modal. 

In~\citep{roberts89}, ~\exref{wolf} yields the DRS (using the standard linear notation):
\begin{equation}
  \Diamond(?, [x \ | \ \semof{wolf}\ x \ldots]) 
  \wedge \Box ([ [x \ | \ x (\semof{wolf}\ x  \ldots],  [ \ | \  \semof{growl}\ x]])
\end{equation}
\possciteauthor{roberts89} account doesn't specify a direct anaphoric link between the
pronoun and the linguistically given antecedent in its own modal
context.  The discourse referent $x$ introduced by the first sentence
{\em remains} inaccessible to the pronoun introduced in the second.  But there is an inferential link added between the linguistic
antecedent in the first sentence and the pronoun; the second sentence in fact quantifies over
all elements in the appropriate domain that have the property
specified by the first sentence, and thus we can infer that whatever
the witness for $x$ in the first DRS, it will growl in every relevant
epistemic possibility.

\citep{geurts,frank96} criticize Roberts's account as being too
unconstrained.  They postulate a direct anaphoric link at the level of
sentence contents between the restrictor of the second modality and
the material under the in the nuclear scope of the first
modality.  The value assigned to $x$ in the first
sentence is linked to its interpretation of the second sentence in~\cite{frank97} because the assignments to $x$ are encoded
in the semantic value (the dynamic intension) of the material under
the scope of the $\Diamond$ and hence in the restrictor of the {\em
  would} modality.  This strategy shows that the discourse referent
$x$ is not functioning as an existentially quantified variable.

But in~\cite{frank97} the {\em would} modality disappears into the
conditional $\Rightarrow$.  They generate a very weak
modal logic, and their account is still too unconstrained~\citep{asher07}.  
%For
%example, it predicts (\ref{thiefb}) to be acceptable and that the
%antecedent of the second pronoun in (\ref{thiefc}) can be the wolf,
%contrary to intuitions.  \examples{%
%  \example{A thief might break in.  He might steal the silver.}%
%  \example{\label{thiefb}A thief might break in.  But that won't
 %   happen because the alarm system is good. *He might steal the
 %   silver. (OK in dialogue)}%
 % \example{\label{thiefc}A wolf might walk in.  He might eat you.  On
%    the other hand, a tiger might walk in.  He would definitely eat
%    you.}%
%}
Finally, (\ref{wolf17}) shows that a straightforward
interpretation of the modal structures above leads to trouble.%
\example{\label{wolf17}A wolf might walk in.  He would growl.  A
  second wolf might then walk in, but he wouldn't growl.}%
If the {\em would} modality is understood as a simple universal
quantification over all wolves that walk in, this discourse is
predicted to be contradictory, but it isn't.  This is a clearly
problem for Roberts' account.  Frank and Kamp
interpret the {\em would} modality relative to all those normal
epistemic possibilities satisfying the antecedent, and this may permit
them to avoid the prediction.  But this wiggle room
also further weakens the account's predictions---for instance, among
those epistemic possibilities validating (\ref{wolf}), there may
be epistemic possibilities where the wolf doesn't growl, contrary to
intuitions.%\footnote{For an extreme case, consider the following
 % dialogue:%
 % \example{%
 %   A: A wolf might walk in.  It would growl.\\%
 %   B: A wolf might walk in tonight, that's true.  But it might not
 %   growl.}%
 % A and B's contributions are incompatible intuitively.  But it's not
%  clear that the normal epistemic possibilities in which A's first
 % sentence are true are the same as those of B's first sentence, which
%  is what would have to be the case to predict the incompatibility.  }

\subsubsection{The Modal Context}

We first show how to make a modal context
accessible to further modalized continuations.  We interpret sentences and discourse as
described in~\exref{eq:omega-modal-context}, together with the sentence
combination rule of~\exref{eq:sentence-compo-modal-context}.
Table~\ref{tab:lexicon-1} then introduces the standard dynamic lexicon
we use. This lexicon uses the following notational convention:
syntactic constituents (basically trees in this paper) are represented
as $\const{word}$, to be read as \textit{word}. A sentence such as
\textit{a wolf might enter} is represented by its syntactic tree
$\const{might}\ \const{enter} \ (\const{a}\ \const{wolf})$. The latter
shows the application rules to be considered in compositionally
computing the semantic representation.

\begin{align}
  \label{eq:omega-modal-context}
  \inter{\SC}  & = \gamma \imp (\gamma \imp \Prop) \imp \Prop   & \defin \Omega\\
  \label{eq:sentence-compo-modal-context}
  \inter{S_1 . S_2 } & = \abs i k.\inter{S_1}\,i\,(\abs i'.S_2\,i'\,k) & : \Omega
\end{align}

\begin{table}[htbp]
$$  \begin{array}{rl}
    \inter{\const{enter}} & = \abs s. s\,(\abs x\,i\,k.(\semof{enter}\,x) \land (k\,i)) \\
    \inter{\const{growl}} & = \abs s. s\,(\abs x\,i\,k.(\semof{growl}\,x) \land (k\,i)) \\
    \inter{\const{wolf}} & = \abs x\,i\,k. (\semof{wolf}\,x) \land (k\,i)\\
    \inter{\const{a}} & = \abs P\,Q.\abs i\,k.\exists x.P\,x\,(x::i)\,(\abs i'.Q\,x\,i'\,k)\\
    \inter{\const{it}} & = \abs P\, i\, k.P\, (\sel \,i)\, i\, k\\
  \end{array}$$
  \caption{Basic dynamic lexicon}
  \label{tab:lexicon-1}
\end{table}

In order to deal with modalities, we introduce the interpretation for
\textit{might} as in~\exref{eq:might-modal-context}\footnote{This
  interpretation results in readings where modalities have scope over
  existentials. The interpretation $\inter{\const{might}'} =%
  \abs v\,s. \abs i\,k. v\,s\,i\,(\abs i'.  \Diamond (k\,i'))$ gives
  existentials scope over modals.}. The effect is simply to put the
content,the quantifiers and the predicates, under the scope of the modal operators.
\begin{align}
  \label{eq:might-modal-context}
  \inter{\const{might}} & =%
  \abs v\,s. \abs i\,k. \Diamond (v\,s\,i\,k)\\
  \inter{\const{would}} & =%
  \abs v\,s. \abs i\,k. \Box (v\,s\,i\,k)%
\end{align}
Then, with $t_0= \const{might}\ \const{enter} \ (\const{a}\
\const{wolf})$ and $t_1=\const{would}\ \const{growl}\ \const{it}$
$t_0.t_1$ represents~\exref{wolf} and we get:
$$
\begin{array}{rl}
  \inter{t_0} & = \abs i\, k. \Diamond (\exists x.(\semof{wolf}\,x) \land ((\semof{enter}\,x) \land (k\,(x::i))))\\
  \inter{t_1} & = \abs i\,k.\Box((\semof{growl}\,(\sel\,i)) \land (k\,i)) \\
  \inter{t_0\ .\ t_1} & = \abs i\, k. \Diamond (\exists x.(\semof{wolf}\,x) \land ((\semof{enter}\,x) \\ & \qquad \qquad \land (\Box ((\semof{growl}\,(\sel\,(x::i)))  \land (k\,(x::i))))))
\end{array}
$$
Our lexical entries also have the effect of embedding one modality within the other, making
discourse referents (here the wolf $x$) accessible for further modal
continuation such as \textit{it would growl}. The first sentence makes
this discourse referent explicitly available in the environment
($x::i$) of the next sentences.

This is not completely satisfactory because it
entails that from a world where a wolf $x$ enters the room, all the
accessible worlds verify that $x$ is growling. But $x$ might be a
tiger in one of these worlds; such worlds should not affect the evaluation of the {\em would} claim.  Below we introduce a \emph{modal base}
that restricts the epistemically relevant worlds in the right way.

\subsubsection{Introducing the Modal Base}

In section 3.1, we specified the atomic type $\gamma$ of
the context as a theory, and in section 2, we made
$\gamma$ a list structure, with the attendant
update function $:::\ent \imp \gamma \imp \gamma$
and access function $\sel : \gamma \imp \ent$.  We now combine these two ideas by considering $\gamma$ as a record:
\begin{equation}
  \gamma = \{ \referents : \gamma' ; \base : \Prop\}
%  \gamma = \modalbasetype{\gamma'}{\Prop}
\end{equation}
where $\gamma'$ provides a set of entities while the
$\base$ field contains the current modal base.

We overload the following functions using the previously defined
ones:
\begin{align}
  x::_b i & =\modalbase{x::(i.\referents)}{i.\base}\\
  \sel_b\,i & = \sel\,(i.\referents)\\
  p \land_b i & = \modalbase{(i.\referents)}{p \land (i.\base)}
\end{align}
and get the lexicon of Table~\ref{tab:lexicon-2}. Neither
the definition of the $\Omega$ type nor the sentence combination rule
change. But standard lexical entries now can add to the modal base
(the $k$ continuations are fed with $(\textit{pred} \land_b i)$
parameters) and the lexical entry for \textit{might} explicitly uses
the current modal base $i.\base$. The main operator for
computing the new modal base is conjunction. However, nothing prevents
us from having more complex computations such as various kinds of
inference in order to take into account \possciteauthor{roberts96}
analysis  of counterfactuals, which exploits consistency relations.\footnote{A better interpretation 
for $\const{it}$ would be
$$\abs P\, i\, k.\texttt{let } x = \sel_b \ i \texttt{ in } P\, x\, i\,
o$$ to ensure that the selected element remains the same in the modal
base and in the modal claim, as the derivations below show.  For simplicity, we don't do this here but we assume that the same element is selected in both places
without loss of generality.}
%where: ``accommodated material must be
%logically compatible with the local context to which it is
%accommodated'' \citep[p. 229]{roberts96}.

\begin{table}[htbp]
  $$  \begin{array}{rl}
    \inter{\const{enter}} & = \abs s. s\,(\abs x\,i\,k.(\semof{enter}\,x) \land (k\,((\semof{enter}\,x) \land_b i))) \\
    \inter{\const{growl}} & = \abs s. s\,(\abs x\,i\,k.(\semof{growl}\,x) \land (k\,((\semof{growl}\,x) \land_b i))) \\
    \inter{\const{wolf}} & = \abs x\,i\,k.(\semof{wolf}\,x) \land (k\,((\semof{wolf}\,x) \land_b i)) \\
    \inter{\const{a}} & = \abs P\,Q.\abs i\,k.\exists x.P\,x\,(x::i)\,(\abs i'.Q\,x\,i'\,k)\\
    \inter{\const{it}} & = \abs P\, i\, k.P\, (\sel_b \,i)\, i\, k \\
    \inter{\const{might}} & = \abs v\,s. \abs i\,k.  \Diamond (i.\base \wedge v\,s\,i\,k)\\
  \end{array}$$
  \caption{Modal context and modal base}
  \label{tab:lexicon-2}
\end{table}



Our lexical entries together with our binder rule in (\ref{degroote})
provide the following derivation for the basic example of
MS\footnote{We use the facts that $(p\land_b (x::_b i)).\base = p
  \land i.\base$ and that $(p\land_b (x::_b i)).\referents = x::
  i.\referents$. }:
\begin{align*}
  \inter{\const{might}\ \const{enter}} & = \abs s. \abs i\,k.  \Diamond ( i.\base \wedge s\,(\abs x\,i\,k.(\semof{enter}\,x) \land (k\,((\semof{enter}\,x) \land_b i)))) \\
  \inter{\const{a}\ \const{wolf}} &= \abs Q\,i\,k.\exists x.(\semof{wolf}\,x)\land(Q\,x\,(\semof{wolf}\,x)\land_b(x::_b i))\,k \\
  \inter{t_0} & =
  \abs i\,k.  \Diamond (i.\base \wedge \exists x.(\semof{wolf}\,x)\land((\semof{enter}\,x) \land (k\,((\semof{enter}\,x) \land_b (\semof{wolf}\,x)\land_b(x::_b i))))) \\
  \inter{t_1} & =
  \abs i\,k.  \Box (i.\base \Rightarrow (\semof{growl}\,(\sel_b  \,i)) \land (k\,((\semof{growl}\,(\sel_b  \,i)) \land_b i))) \\
  \inter{t_0\ . \ t_1} & = \abs i k . (\Diamond (i.\base
  \wedge\exists x.(\semof{wolf}\,x)\land((\semof{enter}\,x)  \\ & \qquad \land (\Box (((\semof{enter}\,x) \land_b
  (\semof{wolf}\,x)\land_b(x::_b i))).\base \Rightarrow (\semof{growl}\,(\sel_b  \,(x::_b i))) \\ %
& \qquad \qquad  \land (k\,((\semof{growl}\,(\sel \,(x::i.\referents))) \land_b ((\semof{enter}\,x) \land_b (\semof{wolf}\,x)\land_b(x::_b i))))))))\\
\end{align*}

Then with $\EMPTY=\modalbase{\nil}{\top}$ and $\TRIVIAL=(\lambda
i.\top)$, the empty parameters for starting a discourse, we get
\begin{align*}
  \inter{t_0\ . \ t_1}\,\EMPTY\,\TRIVIAL & = \Diamond (\top \wedge\exists x.(\semof{wolf}\,x)\land((\semof{enter}\,x)\\ & \qquad \land (\Box (((\semof{enter}\,x) \land (\semof{wolf}\,x)) \Rightarrow (\semof{growl}\,(\sel \,((x::\nil))))))))
\end{align*}

Our lexical entries again yield logical forms in which  the {\em would} claim is embedded under the {\em might}  claim, allowing us to link the anaphoric pronoun via binding to its antecedent
using a bound variable,
in contrast to~\citet{roberts89}.  To make the $\Box$
claims also hold of the relevant possibilities selected by the {\em
  might} sentence, however, we require a condition on our model theoretic
structures: we need an alternativeness relation for the epistemic
modality, which is at least secondarily reflexive so that the $\Box$
claims also hold of the relevant possibilities selected by the {\em
  might} sentence.  One might wonder whether the $\Box$ needs to be
evaluated in the actual world too; we evaluate it only at those worlds
picked out by the {\em might} claim.  To have the effect of the {\em
  would} claim holding of {\em all} epistemic possibilities, we must
stipulate the alternativeness relation to be Euclidean.

CS is flexible enough to allow other lexical entries inducing a wide scope reading for the existential over the modalities
and with the modalities unembedded.  This permits again a bound variable analysis of the anaphoric link across
 \emph{might} and  \emph{would} claims.
 %\footnote{We could avoid imposing secondary reflexivity and replace
%the $\Rightarrow$ with an $\land$ so that from the world selected by
%%the \textit{might} sentence, all the worlds are required to be such
%that the $x$ is still a wolf that walked in in these worlds and,
%moreover, that it is growling.}  
CS allows us to discuss various interpretations
without changing the theoretical framework: we interpret formulas in
the standard model theory of modal logic; it is then a matter of
lexical semantics to achieve the desired effects.



\subsubsection{Interactions Between Actual and Modal Contexts}

To integrate interactions between factual and modal information, we extend our records, our representations of
the left context in the previous section, to include the
factual information within the left context.  We do this by adding a
new field $\factreferents$ to the record that
will contain discourse referents introduced in the factual world:
\begin{equation}
  \gamma = \modfacttype{\gamma'}{\Prop}{\gamma'}
\end{equation}
Actually, we need this type to be a little bit more complex.  It must contain
another field encoding the current mode of the
sentence so that indefinites will be able to add the introduced
variables in $\referents$ when in a modal context
($\{\referents=x::i.\referents ; \factreferents=i.\factreferents\}$)
and in $\factreferents$ when in the actual context
($\{\referents=i.\referents ; \factreferents=x::i.\factreferents\}$).
The same holds for the pronoun that has to select either from the
factually introduced referents ($\sel\ i.\factreferents$) when in the
factual mood or from the union of the factually and modally introduced
referents ($\sel\ i.\referents \cup i.\factreferents$) when in a modal
mood.  To avoid expressing all the cases within our lexical semantics, we
consider a modal entry $\textit{a}^m$ and a factual entry
$\textit{a}^f$ for the indefinite \textit{a}, a modal entry
$\textit{it}^m$ and a factual entry $\textit{it}^f$ for the pronoun,
etc.

Our CS now will use two continuations: one containing facts about the
actual world, one containing facts about live possibilities the
discourse describes.  Instead of producing at the end the $\Prop$
type, sentences now produce a pair of claims: one for the epistemic
worlds, one for the factual world. We model the pair with the
higher-order type function of the type $( \Prop \imp \Prop \imp \Prop) \imp \Prop
$. It is important that the result itself is of type $\Prop$ and not of
type $(\Prop,\Prop)$, because otherwise quantifiers would be introduced either in
the first projection or in the second projection and hence bound
variables would never be accessible to both components.  But the variables
introduced by factual DPs have to be accessible to both components.

These changes induce a change in type for $\Omega$:
\begin{align}
  \inter{\SC} = \gamma \imp (\gamma \imp \Prop) \imp (\gamma \imp \Prop) \imp (\Prop \imp \Prop \imp \Prop) \imp \Prop & \defin \Omega
\end{align}

\begin{table}[htbp]
  $$  \begin{array}{rl}
    \inter{\const{enter}} & = \abs s. s\,(\abs x\,i\,k_1 k_2 f. f ((\semof{enter}\ x) \land (k_1\ (\semof{enter}\ x \land_b i)))\ ((\semof{enter}\ x) \land (k_2\ i)))\\
    \inter{\const{wolf}} & = \abs x\ i\ k_1\ k_2\ f.f ((\semof{wolf}\ x) \land (k_1\ (\semof{wolf}\ x \land_b i)))\ ((\semof{wolf}\ x) \land (k_2\ i))\\
    \inter{\const{a}^m} & = \abs P\,Q.\abs i\,k_1\ k_2\ f.f (\exists x.P\,x\,\{i \texttt{ with } \referents=x::i.\referents\}\,(\abs i'.Q\,x\,i'\,k_1\ k_2\ \Pi_1)\ k_2 \Pi_1)\ (k_2\ i)\\
    \inter{\const{a}^f} & = \abs P\,Q.\abs i\,k_1\ k_2\ f.\exists x.f[k_1\,\{i \texttt{ with } \factreferents=x::i\}] \\ & \qquad \qquad [P\,x\,\{i \texttt{ with } \factreferents=x::i\}\,k_1\,(\abs i'.Q\,x\,i'\,k_1\, k_2 \Pi_2)\ \Pi_2]\\
    \inter{\const{it}^m} & = \abs P\, i\, k_1 \ k_2\ f. P\, (\sel_b \,i.\referents \cup i.\factreferents)\, i\, k_1 \ k_2\ f \\
    \inter{\const{it}^f} & = \abs P\, i\, k_1 \ k_2\ f.P\, (\sel_b \, i.\factreferents)\, i\, k_1 \ k_2 f \\
    \inter{\const{might}} & = \abs v\,s. \abs i\,k_1 \ k_2 \ f. f (\Diamond (i.\base \wedge (v \, s \, i \, k_1 \ k_2 \Pi_1))) \ (k_2 \ i)\\
  \end{array}$$
  \caption{Modal and factual contexts}
  \label{tab:lexicon-3}
\end{table}

Together with the lexical entries of
Table~\ref{tab:lexicon-3}\footnote{$\Pi_1=\abs a\ b.a$ and $\Pi_2=\abs
  a\ b.b$ are the first and the second projection respectively.}, we get (with
$t_2=\const{will}\ \const{growl}\ \const{it}$):%
\begin{align*}
  \inter{t_0} & = \abs i\,k_1\ k_2 f. f [\Diamond (i.\base \wedge  \exists x.(\semof{wolf}\ x) \land ( (\semof{enter}\ x) \\ & \qquad  \land (k_1\
  \{i \texttt{ with } \referents=x::i.\referents \texttt{ and } \base = (\semof{wolf}\ x) \land (\semof{enter}\ x) \land i.\base\})))]\ [k_2\ i]\\
  \inter{t_1} & = \abs i\,k_1\ k_2 f. f [\Box (i.\base \Rightarrow
  ((\semof{growl}\ (\sel\ i.\referents \cup i.\factreferents)) \\ & \qquad \land
  (k_1\
  \{i \texttt{ with } \base= (\semof{growl}\ (\sel\ i.\referents \cup i.\factreferents)) \land i.\base\})))]\ [k_2\ i]\\
  \inter{t_2} & = \abs i\,k_1\ k_2 f. f [k_1\ i]\ [(\semof{growl}\ (\sel \
  i.\factreferents)) \land (k_2\ i)]
\end{align*}

To combine our more complex logical forms, we require a new binder rule:
\begin{align}
  \inter{S_1 \ . \ S_2} & = \abs i \ k_1 \ k_2 \ f.\inter{S_1}\ i\ (\abs i'. \inter{S_2}\ i'\ k_1\ k_2 \Pi_1) \ (\abs i'. \inter{S_2}\ i'\ k_1\ k_2 \Pi_2)\ f
\end{align}

To simplify, we interpret our examples with
empty environments ($\EMPTY=\modfact{\nil}{\top}{\nil}$), trivial
continuations ($\TRIVIAL=\lambda i.\top$).  Xonjunction of the two
components ($\CONJ=\lambda b_1 b_2.b_1 \land b_2$) yields the type $\Prop$.
This yields:
\begin{align*}
  \inter{t_0 \ . \ t_1}\ \EMPTY \ \TRIVIAL \ \TRIVIAL \ \CONJ & =
  [\Diamond (\top \wedge (\exists x. (\semof{wolf}\ x) \land ((
  \semof{enter}\ x) \\ & \qquad \land (\Box (((\semof{wolf}\ x) \land
  ( \semof{enter}\ x)) \\ & \qquad \quad \Rightarrow (\semof{growl}\
  (\sel \ ((x::\nil) \cup
  \nil))))))))] \land \top \\
  \inter{t_0 \ . \ t_2}\ \EMPTY \ \TRIVIAL \ \TRIVIAL \ \CONJ & =
  [\Diamond (\top \wedge (\exists x. (\semof{wolf}\ x) \land ((
  \semof{enter}\ x) \land \top)))] \\ & \qquad \land [\semof{growl}\ (\sel\ \nil)]
\end{align*}
In the first case, the $\sel$ function has access to $x$, so
(\ref{wolf}), represented by $t_0.t_1$, is predicted to be OK, but
(\ref{wolf'}), represented by $t_0.t_2$, is predicted to be bad,
because $x$ is not part of the accessible environment.
To illustrate the importance of pronouns within modal
environments selecting from both modal and factual contexts, consider again~\exref{wolf''}.%
\examples[l@{\hspace{0.5cm}}X]{%
  \exref{wolf''} & A wolf is outside.  He might eat you.%
}%
The
first indicative sentence yields upon $\beta$ reduction:%
\example{ $\lambda i \ k_1\ k_2 \ f.  \exists x.f[k_1 \{i \texttt{
    with } \factreferents=x::i.\factreferents\}] [ (\semof{wolf}\ x)
  \land ((\semof{Outside}\ x) \land (k_2 \ \{i \texttt{ with }
  \factreferents=x::i.\factreferents\}))]$}%
Now integrating the modalized second sentence, we get:%
\example{$\exists x.[\Diamond (\top \wedge (\semof{eat you}\
  (\sel \ \nil \cup (x::\nil))))] \land [ (\semof{wolf}\ x) \land
  ((\semof{Outside}\ x))]$}%
And this is just what we want.

Exploiting a compositional analysis of counterfactuals~\citep{asher07}, our approach can also treat anaphoric links across
counterfactuals:\footnote{The present formalism does not suffice to handle examples with
negation like%
\example{I didn't buy a refrigerator.  I wouldn't know what to do with
  it.}%
We follow ~\posscitet{asher07}
explanation in terms of discourse structure.}%
\example{If I had bought a refrigerator, I wouldn't know what to do
  with it.}%
%The counterfactual is analyzed via a revision operator R on the first
%left context ($R(i_1) \phi \rightarrow \Box \psi$).\


\subsubsection{Putting Everything Together}


Modal subordination phenomena of Veltman's observations
show that factual information is
accessible to modalized continuations. With a slight abuse of notation
(to avoid even longer $\lambda$-terms), we make a factual
sentence update the world context. This suffices to capture
Veltman modalities.\footnote{We ignore here some further subtleties, like those explored in~\citep{asher07}).}

So we now add to the context a field $\theory$ to the context that
will contain the theory under construction which is tested as in
Section~\ref{subsec:veltman} and we have $\gamma \defin \{\referents :
\gamma'; \base : \Prop ; \factreferents : \gamma' ; \theory : \THEORY
\}$

Our final lexical entry for \textit{might} is this:
\begin{equation}
  \begin{split}
    \inter{\const{might}} & = \abs v\,s. \abs i\,k_1 \ k_2 \ f. (\abs P.(\TEST\ P)\ i.\theory\\ & \qquad \quad (\abs i'\ o'_1\ o'_2\ f'. f' (\Diamond (i'.\base \wedge (P\ i'\ o'_1\ o'_2\ Pi_1)))))\ (v\ s)\ i\ k_1\ k_2\ f
  \end{split}
\end{equation}


We have now captured our two types of context sensitivity for
epistemic modals within a unified framework, revealing the power of the
CS approach.  We've added Veltman style modalities in conservative fashion to the externally
static but internally dynamic modalities needed to capture MS.  We've also shown how the choice of
lexical entries and binder rules determine features of modal contexts.

