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


\subsection{Veltman's Test}
\label{sec:veltman}

In this section, we address the our first slogan, which encapsulates the context
dependency of epistemic modality upon the non modal facts taken to be common ground in the discourse.
  This intuition has proved useful in a number of areas of
semantics and epistemology.  For instance, it yields a simple formulation of
the Ramsey test semantics for conditionals.
It was Frank Veltman who brought this
feature of modals into contemporary discussions of epistemic modality with the examples we repeat below:
%\begin{itemize}
%\item First slogan: Epistemic modal facts are dependent on non modal
 % facts but not vice versa
%\end{itemize}
%We repeat Veltman's famous examples below:%
\examples{%
  \example{\label{easy-update}It might be sunny.  But it's not
    sunny.}%
  \example{\label{hard-update}\# It's not sunny.  But it might (for
    all I know) be sunny.}%
}%
Veltman observes that  \exref{easy-update} involves a smooth
discourse update, whereas the second does not.   To account for
his observation, he builds a semantics for a propositional modal
language in which all sentences define an update function on an
information state, which is modelled as a set of worlds or epistemic
possibilities.  The information state evolves as discourse proceeds.
All non modal sentences $\phi$ have a particularly simple update
$[\phi]$: $(s[\phi]) = \{w \in s \colon w \in \|\phi\|\}$.  
%Veltman accounts for this observation by making
%$\Diamond$ a test on the contextually given informational state ( a
%set of epistemic possibilities). 
Modal
sentences, however,
involve tests on the information state.  For a sentence of the form $\Diamond \phi$, we have:\footnote{
We define a Ramsey test semantics for conditionals,  according to which a conditional $\phi \Rightarrow \psi$ is true just in case updating ones
information state with $\phi$ and then with $\psi$ is equivalent to updating just with $\phi$,  as follows for a
  propositional language:.
\begin{equation}
s[\phi \Rightarrow \psi] = s\mbox{ iff } s[\phi][\psi] = s[\phi]
\end{equation}}
\begin{equation}
s[\Diamond \phi] = s \mbox{ iff } \exists w \in s \ w \in \| \phi \|
\end{equation}


Veltman's dynamic semantics is of a very different style from DRT or DPL, where sentences define dynamic
transitions over assignment functions or world assignment function pairs. \possciteauthor{degroote06}
CS picks a notion of left context appropriate for 
modelling DRT or DPL; but to recreate the sort of test behavior by modals in 
Veltman's  semantics, we need to have a different notion of left context.   As we said in the previous section, however, one of the principal virtues
of a continuation style semantics is that  a left context can  in principle be any sort of 
data structure without changing the basic set up of the semantics;  this is a feature that we exploit here in modelling Veltman's observations 
within CS. 
We will take 
a left context to be a \emph{theory} or collection of sentences; this theory models the 
information state and will evolve as discourse proceeds, just as the information state does
for Veltman.   We will then formulate the semantics of modals using a notion of a  test on such a state to capture
the behavior that Veltman noticed.
  

\subsubsection{Veltman modalities within continuation semantics}
\label{subsec:veltman}

In this section we provide a Veltman-inspired CS
for a propositional modal language $\mathfrak{L}$, containing propositional
variables, $\neg, \wedge$, and $\Diamond$.  To incorporate the notion of a test, modals of the form $\Diamond \phi$ permit a continuation
when the modal context $i_1$ is such that $i_1 \cap \| \phi
\| \neq 0$.   This is a presupposition that the incoming context must meet.  If the presupposition
is satisfied, then the update is defined and discourse processing can proceed.
If the discourse context does not satisfy the presupposition, there is no accommodation and no further
updating is possible.  

Veltman's idea of a test treats the semantic value of a formula as something other than a simple truth value.  Thus, our
type of proposition must reflect this; it will no longer be $t$, as in extensional versions of Montague grammar but rather some intensional 
type, which we will call here $\PROP$.  
We consider left contexts to be a theory, of type $\THEORY$, giving
the content of the discourse context (this could be a single formula or a set of formulas).  Just as in 
\cite{degroote06}, we also need the $::$ operator that updates the left context within information
from the formula under consideration.
The basic types of our variables $i$ (for left contexts), $k$ (for right contexts) and $::$ (for our update function) are:
$$
\begin{array}{rl}
  i & : \gamma \defin \THEORY \\
  k & : \THEORY \imp \Prop \\
  :: & \PROP \imp \THEORY \imp \THEORY  
\end{array}
$$
We also have an exception $\HALT$ that when raised stops the evaluation, and a $\TEST$ operation that we define presently.
We now define the dynamic variants of the propositional connectives and modal operator, 
with a canonical
injection from the static to the dynamic case.
The basic $\lambda$-terms of this language are:
\begin{itemize}
\item for an atomic static formulas $p$ of type $\Prop$: $\lambda i\ k. p \land (k\ (p::i))$;
\item for $P$ a dynamic proposition (of type $\Omega \defin \gamma
  \imp (\gamma \imp \Prop) \imp \Prop)$), we define (with
  $\TRIVIAL\defin \abs i.\top$ the trivial continuation):
  \begin{itemize}
  \item the dynamic negation $\neg_d \defin \lambda P. \lambda i\ k.(\neg (P\ i \TRIVIAL)) \wedge (k\ ((\neg P\ i\ \TRIVIAL)::i))$;
  \item the dynamic conjunction: $\wedge_d \defin \lambda P\ Q.\lambda
    i\ k.P\ i\ (\lambda i'. Q\ i'\ k)$;
  \item the dynamic modality $\Diamond_d \defin \lambda P. \lambda i\
    k.(\TEST\ P)\ i\ (\lambda i'. (k\ i') \wedge (\Diamond (P\ i'\
    \TRIVIAL)))$ where $\Diamond$ is the classic static modality.
  \end{itemize}
\end{itemize}

To define $\TEST$, we need to evaluate the consistency of the claim under the
scope of the modal with the incoming context.  We use an
{\em evaluation} function $\EVAL$ from propositions to truth values, which we define in terms
of consistency or general satisfiability (relative to any model).\footnote{
We could also define $\EVAL$ relative to a particular model as does Veltman.  
But if the fixed model is somehow deficient
(doesn't for instance contain enough epistemic possibilities), the 
Test procedure may produce funny
results.  While one can stipulate a full model in cases where canonical model
constructions are possible, this is not always possible.  Our conception of $\EVAL$ does
not have this limitation.} 

\begin{equation}
  \label{eq:test-definition}
  \TEST\ P  = \abs i\ k. \texttt{if } (\EVAL\ P\ i\ \TRIVIAL) \texttt{ then } (k\ i) \texttt{ else } (\texttt{raise } \HALT)
\end{equation}
%Our definition of Test follows a conception of semantics according to which
%semantics is primarily responsible for providing a logical form that can support inferences via
%logical consequence defined across a range of models. 


$\Diamond_d$ yields a continuation iff there is at least one world that
verifies all the information in the discourse context together with
the content under the scope of the modal.  If not it raises an
exception $\HALT$, whose effect is to stop the evaluation.  This
captures Veltman's intuition that there is no possible continuation in
this case.  This use of exceptions resembles~\posscitet{degroote10} use of exceptions for presupposition
accomodation.  This is no surprise; Veltman's \textit{might} exhibits
presuppositional behavior, but with no possibility
of accommodation.


This set up makes the same predictions that Veltman's semantics does
for simple modal sentences, assuming the standard combination rule
(which actually is $land_d$).  We illustrate with
(\ref{easy-update}).  Beginning with the empty input context $\EMPTY$
and updating with 'It might be sunny' ($\Diamond_d S$ with $S = \abs
i\ k.  \semof{sunny} \land (k \ (\semof{sunny}::i))$) we get a
continuation because it is consistent to assume $S$ (and indeed any
propositional letter), that is $\EVAL\ S\ \EMPTY \ \TRIVIAL=\top$.
\begin{align*}
  (\Diamond_d S)\ \EMPTY & \betareduce  \lambda  k . (\TEST\ S)\ \EMPTY \ (\abs i'.(k\ i') \land (\Diamond (S\ i'\ \TRIVIAL)))\\
  & \betareduce k\ \EMPTY
\end{align*}
Integrating this with 'not sunny' or $\lambda i\ k. (\neg
\semof{sunny}) \wedge (k\ ((\neg \semof{sunny})::i))$ using
(\ref{degroote}) will then restrict future continuations to having a
discourse context in which it is not sunny as a left context.  But
reversing the order of these sentences gives us a different result.
Updating first with $\neg_d S$, gives us a discourse context such that
attempting to update with $\Diamond_d S$ will lead the Test to raise
$\HALT$ because the current theory to be tested will contain both
$\neg \semof{sunny}$ and $\semof{sunny}$ which makes it unsatisfiable.
This yields no continuations, and no further informative updates are
possible.  We thus predict that the discourse is malformed.  Veltman's account of update to test and its consequence are
straightforwardly captured in this CS.



