\documentstyle[a4wide]{article}
 
\title{Can we make an honest language out of situation theory?
\thanks{Research reported in this paper has been supported by DYANA, ESPRIT Basic Research Action project 3175 and FraCaS, LRE
project 62-051.  This is an abstract submitted to ITALLC96.}}
 
\author{Robin Cooper \\ \\ University of Gothenburg \\ and \\
University of Edinburgh} 
 
\date{January, 1995} 
 
\parindent = 0pt
\setlength{\parskip}{\baselineskip}

\newcommand{\ben}{\begin{enumerate}}
\newcommand{\een}{\end{enumerate}}
\newcommand{\spc}{\bigskip}
\newcommand{\bqt}{\begin{quote}}
\newcommand{\eqt}{\end{quote}}
\newcommand{\bit}{\begin{itemize}}
\newcommand{\eit}{\end{itemize}}
\newcommand{\bt}{\begin{tabbing}}
\newcommand{\et}{\end{tabbing}}
\newcommand{\bd}{\begin{description}}
\newcommand{\ed}{\end{description}}


\newenvironment{Bibliography}{\section*{References} 
\begin{enumerate}}{\end{enumerate}}

\renewcommand{\bibitem}[0]{\item[] \hspace*{-\leftmargin}}

\newcommand{\ignore}[1]{}

%%
%%  File: ekn.sty
%%
%%  LaTeX macros for Extended Kamp Notation (EKN) 
%%  Jon Barwise and Robin Cooper
%%  barwise@edu.indiana.phil, cooper@cogsci.ed.ac.uk
%%  
%%  (with some additions by Alan Black)
%%
%%  Aug,  28th 1991
%%

%% If you are working with a standard size LaTeX you will probably
%% need to use \sbox and \usebox in order to create larger ekn
%% structures.  \boxa thru \boxe are declared at the end of this file.

%% Comments on this file, problems and suggestions for improvement are
%% welcome.  The macros are still in development and we give no
%% guarantee that they will work in all cases.

\newcommand{\res}[2]{\mbox {$ #1 \mid \! \! \grave{} \; #2 $}}

%% \conjbox has one argument, a list of conditions, separated by \\s It
%% produces a box with the conditions inside.

\newcommand{\conjbox}[1]{
\begin{tabular}{|l|}\hline 
 \eknlist{#1}\\ \hline
\end{tabular} }

\newcommand{\subscbox}[2]{\begin{tabular}{@{}r@{}l}#1& \\
   &\{#2\}\end{tabular}}

\newcommand{\infon}[1]{\mbox {$\langle \! \langle$#1$\rangle \! \rangle$}}

% We include a macro with this name only for historical reasons.  It
% is identical with \resconjbox
\newcommand{\resinfonbox}[2]{
\begin{tabular}{|l||l|}\hline 
 \eknlist{#1} & \eknlist{#2} \\ \hline
\end{tabular} }

\newcommand{\resconjbox}[2]{
\begin{tabular}{|l||l|}\hline 
 \eknlist{#1} & \eknlist{#2} \\ \hline
\end{tabular} }

%% \relnbox has two arguments, a list of variable and a list of conditions
%% separated by \\s. It produces a window, with space at the top for the
%% variables, and the conditions in the lower pane.  These windows
%% represent relations obtained by abstraction over the
%% infon.

\newcommand{\relnbox}[2]{
\begin{tabular}{|l|}\hline
\ \ \ #1 \\ \hline
 \eknlist{#2}\\ \hline
\end{tabular} }

\newcommand{\tabrelnbox}[3]{
\begin{tabular}{lll|}
\cline{3-3}
\ \ \ & \ \ \ & \multicolumn{1}{|l|}{#1} \\
\hline
\multicolumn{3}{|l|}{\ #2} \\ \hline
 \multicolumn{3}{|l|}{\eknlist{#3}} \\ \hline
\end{tabular} }

\newcommand{\tabtabrelnbox}[4]{
\begin{tabular}{lll|}
\cline{3-3}
\ \ \ & \ \ \ & \multicolumn{1}{|l|}{#1} \\
\cline{3-3}
\ \ \ & \ \ \ & \multicolumn{1}{|l|}{#2} \\
\hline
\multicolumn{3}{|l|}{\ #3} \\ \hline
 \multicolumn{3}{|l|}{\eknlist{#4}} \\ \hline
\end{tabular} }

\newcommand{\resrelnbox}[3]{
\begin{tabular}{|l||l|}\hline
\multicolumn{2}{|l|}{\ \ \ #1 }\\ \hline
 \eknlist{#2} & \eknlist{#3} \\ \hline
\end{tabular}}

\newcommand{\tabresrelnbox}[4]{
\begin{tabular}{lll|}
\cline{3-3}
\multicolumn{2}{l}{} & \multicolumn{1}{|l|}{#1} \\
\hline
\multicolumn{3}{|l|}{\ #2 }\\ \hline
 \multicolumn{1}{|l}{\eknlist{#3}} & \multicolumn{2}{||l|}{\eknlist{#4}} \\
\hline \end{tabular}}

\newcommand{\tabtabresrelnbox}[5]{
\begin{tabular}{lll|}
\cline{3-3}
\multicolumn{2}{l}{} & \multicolumn{1}{|l|}{#1} \\
\cline{3-3}
\multicolumn{2}{l}{} & \multicolumn{1}{|l|}{#2} \\
\hline
\multicolumn{3}{|l|}{\ #3 }\\ \hline
 \multicolumn{1}{|l}{\eknlist{#4}} & \multicolumn{2}{||l|}{\eknlist{#5}} \\
\hline \end{tabular}}

%% \tabbox has two arguments, a list of parameters and a list of
%% conditions separated by \\s.  It produces a window with a tab at the
%% top containing the parameters. 


\newcommand{\tabbox}[2]{
\begin{tabular}{l|l|}\cline{2-2}
\ \ \ & #1 \\ \hline
\multicolumn{2}{|l|}{\eknlist{#2}}
 \\ \hline
\end{tabular} }

\newcommand{\restabbox}[3]{
\begin{tabular}{ll|l|}\cline{3-3}
\ \ \ & & #1 \\ \hline
\multicolumn{1}{|l} {\eknlist{#2}} 
      & \multicolumn{2}{||l|}{\eknlist{#3}} \\ \hline
\end{tabular}}

\newcommand{\reln}[2]{\mbox {[#1 $\mid$ #2 ]}}
 
%% \prpnbox has two arguments, a situation and a list of conditions
%% sepearted by \\'s. It produces a box with a tag for the situation.
%% These boxes represent propositions, the proposition that the
%% situation supports the infon represented by the condition.

\newcommand{\prpnbox}[2]{
\begin{tabular}{|c|l|}\hline 
\shrtlist{#1}  & \\  \cline{1-1} 
\multicolumn{2}{|l|}{\eknlist{#2}}\\ \hline
\end{tabular} }

\newcommand{\tabprpnbox}[3]{
\begin{tabular}{ll|l|}\cline{3-3}
\ \ \ & & #1 \\ \hline
\multicolumn{1}{|c|} {\shrtlist{#2}}  & \multicolumn{2}{l|}{} \\ 
\cline{1-1}  \multicolumn{2}{|l}{\eknlist{#3}} & \multicolumn{1}{l|}{}\\ \hline
\end{tabular} }

\newcommand{\resprpnbox}[3]{
\begin{tabular}{|c|l||l|}\hline 
\shrtlist{#1}  & & \\ 
\cline{1-1}
\multicolumn{2}{|l||}{\eknlist{#2}} & \eknlist{#3} \\ \hline
\end{tabular} }


\newcommand{\prpn}[2]{\mbox {$($#1$\models$#2$\;)$}}


%% \typebox has three arguments, a list of parameters, a situation, and a
%% list of conditions sepearted by \\'s. It produces a window with a tag
%% for the situation.  These situated windows represent types, the type
%% that is obtained by abstraction over the proposition
%% represented by the lower prpnbox.

\newcommand{\typebox}[3]{
\begin{tabular}{|c|l|}\hline
\multicolumn{2}{|l|}{ \ \ \ #1} \\ \hline 
#2  & \\ 
\cline{1-1}
\multicolumn{2}{|l|}{\eknlist{#3}}\\ \hline
\end{tabular} }

\newcommand{\tabtypebox}[4]{
\begin{tabular}{cll|}
\cline{3-3}
\multicolumn{2}{l|}{} & #1 \\
\hline
\multicolumn{3}{|l|}{ \ #2} \\ \hline 
\multicolumn{1}{|c|}{#3}  & & \\ 
\cline{1-1}
\multicolumn{3}{|l|}{\eknlist{#4}}\\ \hline
\end{tabular} }

\newcommand{\tabtabtypebox}[5]{
\begin{tabular}{cll|}
\cline{3-3}
\multicolumn{2}{l|}{} & #1 \\
\cline{3-3}
\multicolumn{2}{l|}{} & #2 \\
\hline
\multicolumn{3}{|l|}{ \ #3} \\ \hline 
\multicolumn{1}{|c|}{#4}  & & \\ 
\cline{1-1}
\multicolumn{3}{|l|}{\eknlist{#5}}\\ \hline
\end{tabular} }



\newcommand{\tabtabtabtypebox}[6]{
\begin{tabular}{cll|}
\cline{3-3}
\multicolumn{2}{l|}{} & #1 \\
\cline{3-3}
\multicolumn{2}{l|}{} & #2 \\
\cline{3-3}
\multicolumn{2}{l|}{} & #3 \\
\hline
\multicolumn{3}{|l|}{ \ #4} \\ \hline 
\multicolumn{1}{|c|}{#5}  & & \\ 
\cline{1-1}
\multicolumn{3}{|l|}{\eknlist{#6}}\\ \hline
\end{tabular} }

\newcommand{\restypebox}[4]{
\begin{tabular}{|c|l||l|}\hline
\multicolumn{3}{|l|}{\ \ \ #1 }\\ \hline
 #2 & & \\
\cline{1-1}
\multicolumn{2}{|l||}{\eknlist{#3}} & \eknlist{#4} \\ \hline
\end{tabular}}

\newcommand{\tabrestypebox}[5]{
\begin{tabular}{|c|l||l|}
\cline{2-3}
\multicolumn{1}{l}{} & \multicolumn{2}{|l|}{#1} \\
\hline
\multicolumn{3}{|l|}{\  #2 }\\ \hline
 #3 & & \\
\cline{1-1}
\multicolumn{2}{|l||}{\eknlist{#4}} & \eknlist{#5} \\ \hline
\end{tabular}}

\newcommand{\tabtabrestypebox}[6]{
\begin{tabular}{|c|l||l|}
\cline{2-3}
\multicolumn{1}{l}{} & \multicolumn{2}{|l|}{#1} \\
\cline{2-3}
\multicolumn{1}{l}{} & \multicolumn{2}{|l|}{#2} \\
\hline
\multicolumn{3}{|l|}{\  #3 }\\ \hline
 #4 & & \\
\cline{1-1}
\multicolumn{2}{|l||}{\eknlist{#5}} & \eknlist{#6} \\ \hline
\end{tabular}}


\newcommand{\type}[3]{\mbox {$[$#1$\mid ($#2 $\models$\infon{#3}$ \;) ]$}}

%% \anchenv has one argument a list of anchors separated by \\s (in any
%% form).  This produces a bracketed structure with the anchors on each
%% line.  -- awb

\newcommand{\anchenv}[1]{
$\left[ {\rm #1 } \right] $}


%% \anchor has two arguments.  These are realised with a small arrow 
%% between them.

\newcommand{\anchor}[2]{
#1 \rightarrow #2}

%% We have now decided to call things like this assignments.  Thus the
%% slightly different macros

\newcommand{\assignment}[1]{
$\left[  \mbox{\shrtlist{#1}}  \right] $}

\newcommand{\assign}[2]{
#1 $\rightarrow$ #2}

%% \restypebox has four arguments, a list of parameters, a list of prpnboxes
%% separarted by \\s, a situation, and a list of conditions, separated by
%% \\s.  It produces a window with the restrictions next to the variables
%% that are abstracted over, and the conditions below.  These represent
%% types obtain by abstracting over parameters subjected to restrictions.

% \newcommand{\restypebox}[4]{
%\begin{tabular}{|c|ll|}\hline
%\multicolumn{2}{|l}{ \ \ \ #1} & \begin{tiny} \begin{tabular}{@{}l} \\ #2 \\ \\
%\end{tabular} \end{tiny} \\ \hline  #3  & & \\ 
%\cline{1-1}
%\multicolumn{2}{|l}{\eknlist{#4}} & \\ \hline
%\end{tabular} }

 %\newcommand{\restypebox}[4]{\abst{#1}{\resprpnbox{#2}{#3}{#4}}}


\newcommand{\restype}[4]{\mbox {$[ $#1: #2$ \mid$ \prpn{#3}{#4}$ \;)]$}}


%% \resrelnbox has three arguments, a list of parameters, a list of
%% restrictions, and a list of conditions.  It produces a window with
%% with the restrictions listed to the right of the variables. It
%% represents a property obtained from abstracting over some restricted
%% parameters in an infon.
 
%\newcommand{\resrelnbox}[3]{
%\begin{tabular}{|c|ll|}\hline
%\multicolumn{2}{|l}{ \ \ \ #1} & \begin{tiny} \begin{tabular}{@{}l} \\ #2 \\ \\
%\end{tabular} \end{tiny} \\ \hline 
%\multicolumn{2}{|l}{\eknlist{#3}} & \\ \hline
%\end{tabular} }

\newcommand{\resreln}[3]{\mbox {$[ $#1: #2 $ \mid $\infon{#3} $ ]$}}

\newcommand{\eknlist}[1]{\begin{tabular}{l} \\ #1 \\ \\ \end{tabular}} 
\newcommand{\shrtlist}[1]{\begin{tabular}{@{}l@{}} #1 \end{tabular}}
\newcommand{\smalllist}[1]{\begin{tabular}{l}  \\ #1
                \smallskip \end{tabular}} 
 
\newcommand{\abst}[2]{
\begin{tabular}{|l|} \hline
\ \ \ #1\\ 
\multicolumn{1}{@{}l@{}}{#2} 
\end{tabular}}

%\newcommand{\resrelnbox}[3]{\abst{#1}{\resinfonbox{#2}{#3}}}

\newcommand{\dual}[1]{\overline{#1}}

\newsavebox{\boxa}
\newsavebox{\boxb}
\newsavebox{\boxc}
\newsavebox{\boxd}
\newsavebox{\boxe}


%
% Reference the next example in the text:
%
\newcommand{\nexteg}[1]{\addtocounter{examplectr}{1}(\arabic{examplectr}{#1})\addtocounter{examplectr}{-1}}
%
% Reference the previous example in the text:
%
\newcommand{\preveg}[1]{(\arabic{examplectr}{#1})}
%
% Reference examples by relative offsets:
%
\newcommand{\egnum}[2]{\addtocounter{examplectr}{#1}(\arabic{examplectr}{#2})\addtocounter{examplectr}{-#1}}
%
%
% ENVIRONMENTS
%
% Examples Environments
%
\newcounter{examplectr}
\newcounter{subexamplectr}[examplectr]
\renewcommand{\thesubexamplectr}{\alph{subexamplectr}}
%
% Sub-example Macro:
%
\newenvironment{subex}%
   {\begin{list}
       {\alph{subexamplectr}.}%
       {\setlength{\topsep}{0in}
	\setlength{\leftmargin}{0.25in}
	\setlength{\labelsep}{0.15in}
 \usecounter{subexamplectr}}
       }%
   {\end{list}}
%
% Single Example Macro
%
\newenvironment{ex}%
   { \refstepcounter{examplectr}
     \bigskip
     \begin{list}
       {
       (\arabic{examplectr})}%
       {%\setlength{\topsep}{0in}
	\setlength{\leftmargin}{0.75in}
	\setlength{\labelsep}{0.15in}
}
        \begin{minipage}[t]{4in} \item
   }%
   {\end{minipage}
    \end{list}}
%
% End of example macro
%

\newcommand{\subegref}[2]{(\ref{#1}\ref{#2})}

\newcommand{\beg}{\begin{ex}}
\newcommand{\eeg}{\end{ex}}
\newcommand{\bseg}{\begin{subex}}
\newcommand{\eseg}{\end{subex}}










%Macros for L_EKN
\newcommand{\fwedge}{\ \underline{\wedge}\ }
\newcommand{\fvee}{\ \underline{\vee}\ }
\newcommand{\frightarrow}{\ \underline{\rightarrow}\ }
\newcommand{\fleftrightarrow}{\ \underline{\leftrightarrow}\ }
\newcommand{\fneg}{\ \underline{\neg}\ }
\newcommand{\fexists}{\ \underline{\exists}\ }
\newcommand{\fforall}{\ \underline{\forall}\ }
\newcommand{\fcolon}{\ \underline{:}\ }
\newcommand{\fmodels}{\ \underline{\models}\ }
\newcommand{\fequals}{\ \underline{=}\ }
\newcommand{\funlhd}{\ \underline{\unlhd}\ }

\newcommand{\newterm}[1]{{\sc #1}}
\newcommand{\lingex}[1]{{\it #1}}

 
\begin{document} 
 
\bibliographystyle{egapa} 
 
\maketitle 
 
In this paper we will consider the development of a language $L_{\it
EKN\/}$ to serve as a basis for a computational semantic formalism
based on situation theory as characterized using Extended Kamp
Notation (EKN) in Barwise and Cooper (1991,1993) will consider
some important features of the language which distinguish it from some
more traditional semantic formalisms and sketch how these features can
be employed in three different approaches to semantics: Montague
semantics, discourse representation theory (DRT) and situation
semantics.  We will then give a syntax and set of axiom schemes for
the language.  We will argue that a language based on situation theory
is pregnant with possibilities for bringing together a number of
recent developments in natural language semantics including both type
theoretical approaches to DRT and structured approaches to
intensionality in meaning.  There is still an open question, however,
of what kind of model might be supplied for the language in order to
make it honest.

The three important features which make a semantic formalism based on situation
theory distinct from other semantic formalisms are:
Austinian propositions, simultaneous abstraction and restrictions.
We shall discuss each of these in turn in the following sections.

\section{Austinian propositions}

We will allow ourselves proposition terms of the form $(s:\sigma)$
(represented graphically as \prpnbox{$s$}{$\sigma$})
where $s$ is a situation and $\sigma$ is an infon. \ignore{An example is
given in \nexteg{}.
\beg
\label{ex100} 
\prpnbox{$s$}{hire(Jones,Smith,$t$)} 
\eeg 
This represents the proposition that Jones hired Smith at time $t$ in
situation $s$.  The infon 
\bqt
hire(Jones,Smith,$t$)
\eqt
is a persistent type of situations, that is, it is a type that will
hold of any situation of which $s$ is a part.  Thus the proposition
is a predication.  It is represents a type predicated of a situation.}

In addition to terms such as this we allow formulas in our language
which assert that $s$ is of a type $\sigma$.  We write this as $s\
\fcolon \
\sigma$ (or, following the standard tradition of situation theory
$s\fmodels \sigma$).\footnote{Connectives and other constructors which
are used to form formulae are underlined in order to distinguish them
from similar symbols which are used to construct terms.}  The relationship between the proposition terms
and these formulas is expressed by \nexteg{}.
\beg 
{\it true\/}(\prpnbox{$s$}{$\sigma$}) $\fleftrightarrow s\fmodels\sigma$ 
\eeg 

\paragraph{Austinian propositions in Montague semantics}

Austinian propositions are used in the recreation of Montague's
semantics to solve problems of granularity.  \ignore{In Montague's original
traditional possible worlds treatment, propositions are treated as
functions from world-time pairs to truth-values, or equivalently as
sets of world-time pairs.  This meant that any two sentences which
were logically equivalent would correspond to the same Montague
proposition.}  Austinian propositions can be equivalent without being
identical and thus do not suffer from the problem of the traditional
possible worlds approach.  \ignore{We can capture Montague's idea of making
propositions dependent on worlds and time by abstracting over the $s$
and $t$ in a proposition like (\ref{ex100}).  Thus the reconstruction
of a Montague proposition in the situation theoretic treatment is an
object which takes a situation/world and a time and returns an
Austinian proposition.}  \ignore{This is to be compared with Montague's
original proposition which took a world and a time and returned a
truth-value.}  The details of the situation-theoretic treatment are
given in Cooper(1993) and discussed in a forthcoming FraCaS deliverable..

\paragraph{Austinian propositions in DRT}

Austinian propositions are used in the situation theoretic
reconstruction of DRT (Cooper,1993, and a forthcoming FraCaS
deliverable) to represent conditions in DRSs that represent
constraints on events or states.  \ignore{Consider, for example, the
discourse in \nexteg{} discussed by Kamp (1990).
\beg
Last month a whale was beached near San Diego.  Three days later it was 
dead.
\eeg
His DRS for this makes crucial use of a discourse referent for the
event of the whale being beached and another discourse referent for
the state of the whale being dead and there is a condition relating
the temporal occurrence of the two.}  In standard DRS notation the
conditions on events and states are expressed as in \nexteg{}.
\beg
\item $e$ : \conjbox{beached($x$)}
\eeg
These conditions are represented in the situation theoretic
reconstruction of DRT as parametric Austinian propositions (the
parameters corresponding to discourse referents).  The Austinian
propositions are represented in \nexteg{}.\ignore{\footnote{The language
developed here does not distinguish between events and states but
rather lumps them together as certain kinds of situations.  In a
future deliverable we plan to indicate how these different kinds of
situations could be distinguished.}}\footnote{Here we do not
distinguish between those situations which are event and those which
are states, though it is possible to do this.}
\beg 
\item \prpnbox{$S_1$}{beached($X$)} 
\eeg 
[In the full version of the paper we will discuss two advantages of
using Austinian propositions over the classical DRT approach of a
Davidsonian event semantics.  1) It places a natural restriction on the
kind of DRS that can occur as an argument in a condition on events,
i.e. it must be a DRS without a domain corresponding to an infon.
This is borne out by much current practice within DRT.  2)  It allows
for a more powerful treatment of ``negative events'' (argued for in more
detail in Cooper, to appear).]

\ignore{
Treating these conditions as Austinian propositions makes a certain
prediction which seems to be borne out at least by the treatment
presented in Kamp and Reyle(1993). Austinian propositions are
constructed from a situation and a situation-type, in this particular
case a persistent situation type or infon, this places certain
restrictions on the kind of DRS that can be to the right-hand-side of
the colon in the DRS condition.  Only DRSs without domains correspond
to infons.  Thus the condition in \nexteg{a}, while potentially
allowable according to DRS syntax does not make any sense when
converted into the corresponding situation theoretic representation
\nexteg{b}.
\beg 
\bseg 
 
\item $e$ : \relnbox{$x$}{beached($x$)} 
 
\item \prpnbox{$S_1$}{\relnbox{$X$}{beached($X$)}} 
 
\eseg 
   
\eeg 
\preveg{b} is not well-formed because \relnbox{$X$}{beached($X$)} is a
property of individuals rather than a type of situations.

Another important difference concerns the treatment of negative
events.  Whereas the original DRT is based on a Davidsonian event
semantics, a situation theoretic treatment allows for a treatment of
negative events in terms of negative infons.    Thus if we are
representing the sentence \nexteg{a}, example 128 of D5, discussed on
p. 116 of deliverable D10,  it is natural to use an Austinian
proposition like that in \nexteg{b}.
\beg 
\bseg 
 
\item Smith did not travel by air 
 
\item \prpnbox{$S$}{$\neg$travel\_by\_air($X$)} 
 
\eseg 
   
\eeg 
\preveg{b} gives us an event $S$ which can be referred to subsequently
in the discourse, for example by a follow-up sentence like \nexteg{}.
\beg 
It was a terrible journey. 
\eeg 
In principle it would be possible formulate DRS syntax so as to allow
us to construct a corresponding negative DRS condition, as in
\nexteg{}.
\beg 
$e$ : $\neg$\conjbox{travel\_by\_air($x$)} 
\eeg 
However, it is difficult to see how to construe this in terms of the
Davidsonian semantics which has been proposed for traditional DRT.
Consider first the positive case.  The DRS condition \nexteg{a}
corresponds to the Davidsonian semantics \nexteg{b}.
\beg 
\bseg 
 
\item  $e$ : \conjbox{travel\_by\_air($x$)}
 
\item  travel\_by\_air($e,x$)
 
\eseg 
   
\eeg 
\preveg{b} is to be read intuitively as ``$e$ is an event of
travelling by air by $x$''.  When we consider the negative condition
(repeated in \nexteg{a}), it appears that the only possibility for
representing the negation in Davidsonian terms is \nexteg{b}.
\beg 
\bseg 
 
\item $e$ : $\neg$\conjbox{travel\_by\_air($x$)}
 
\item  $\neg$travel\_by\_air($e,x$) 
 
\eseg 
   
\eeg 
\preveg{b} says ``$e$ is not an event of travelling by air by $x$''.
But what the DRS suggests and the particular Austinian proposition
which corresponds to it gives us is ``$e$ is an event of not
travelling by air by $x$''.  This inner scope of the negation is made
possible by the fact that situation theory allows negative infons.  It
is impossible to obtain on a Davidsonian approach because there is
nothing correspond to an infon to be negated.  

The issue, then, is
whether we need to have the internal negation or not.
The answer is by no means clear.  On one view at
least, we seem to need
a theory of events which allows us to conclude that Smith's not
travelling by air refers to an event which has a positive type which
precludes Smith travelling by air, such as being an event of Smith's
travelling by train or staying home to get some work done.  To have
just the wide scope negation does not allow us to prescribe this
inference.  An event which is not an event of Smith travelling by air
could be one of him eating lunch, or indeed of somebody else eating
lunch, neither of which preclude it being an event of him travelling
by air, except, possibly, in special circumstances.
}

\paragraph{Austinian propositions in situation semantics}

We isolate two uses of Austinian propositions here:  resource
situations and event structure.  The idea behind resource situations
is that we can use Austinian propositions to  provide a situation
associated with a particular use of a noun-phrase in order to restrict
the range of the quantifier expressed by the noun-phrase (or determine
a referent for the noun-phrase in the case of a definite).  Arguments
are provided in Cooper(1995)
that resource
situations should be distinct from the situations described by
sentences.

Austinian propositions are the vehicle in situation semantics for
discussing event structure since they involve predication of
situations (including events).  \ignore{In the early situation semantics
literature the discussion of event structure centres around naked
infinitive perception complements and we have been working on
extending this to the analysis of event structure that is required for
the analysis of aspect and event anaphora.}

\section{Simultaneous abstraction}

The language $L_{\it EKN\/}$ has a version of simultaneous abstraction.
in Cooper(1993) the notion of
simultaneous abstraction as developed by Aczel and Lunnon (1991) and
Lunnon (1991, 1992) is
used and presented
in the context of situation theory.  However, there are now other
versions of simultaneous abstraction, notably that developed by Peter
Ruhrberg (1994).  \ignore{While the
Aczel-Lunnon version of simultaneous abstraction was developed
originally to support situation theory it is independent of it and the
central ideas of simultaneous abstraction can be seen as independent
of Aczel and Lunnon's particular development.}

\ignore{
On the Aczel-Lunnon approach,  abstracts are regarded as
a particular kind of object in a structured universe.  This contrasts
with the standard\footnote{at least for formal semanticists} view of
abstracts received from Montague's semantics as functions or rather 
$\lambda$-expressions which are interpreted as functions.  While this
is important for the situation theoretic approach there are two other
features of this kind of abstraction which are perhaps of more general
importance for a computational semantic formalism:
\bd
\item[simultaneous abstraction]  Any number of parameters in a
parametric object may be abstracted over simultaneously.  While in
standard $\lambda$-notations one may have expressions such as
\bqt
$\lambda x,y,z[\phi(x,y,z)]$
\eqt
this is to be construed as an abbreviation for
\bqt
$\lambda x[\lambda y[ \lambda z[\phi(x,y,z)]]]$
\eqt
In Aczel-Lunnon abstraction, however, it is the set which is
abstracted over.  Thus arguments to the abstract can be supplied
simultaneously and there is no required order.

\item[indexing]  This feature is closely related to the previous one.
Since abstraction over parameters results in an object in which those
parameters do not occur\footnote{This is important in order to achieve
$\alpha$-equivalence, i.e. $\lambda x[\phi(x)] = \lambda y[\phi(y)]$},
we have to have some way of determining how arguments are to be
assigned to the abstract in the case where more than one parameter has
been abstracted over.  Aczel and Lunnon achieve this by defining the
abstraction operation in terms of indexed sets of parameters, i.e.
one-one mappings from some domain (``the indices'') to the parameters
being abstracted over.  An important aspect of this for us is that we
can use any objects in the universe as the indices.
\ed
}

We introduce parameter constants (that is, intuitively, constants that
would denote parameters in a situation theoretic universe) into
$L_{\it EKN\/}$ and represent them by upper case letters.  We allow
terms of the form $\lambda$[\assign{$\rho_1$}{$X_1$},\ldots,\assign{$\rho_n$}{$X_n$}]($\alpha$)
(graphically,
\tabbox{\assign{$\rho_1$}{$X_1$},\ldots,\assign{$\rho_n$}{$X_n$}}{$\alpha$})
where $\rho_1,\ldots,\rho_n$ are role constants and $\alpha$ is a term
of any sort which contains the parameter constants $X_1,\dots,X_n$.  

\paragraph{Simultaneous abstraction in Montague semantics}

Simultaneous abstraction is not exploited in the situation theoretic
reconstruction of Montague semantics since Montague employs the
unary abstraction of the standard $\lambda$-calculus.  \ignore{It is used in
the particular treatment presented for the abstraction corresponding
to Montague's abstraction over world-time pairs, although this is not
a crucial use of simultaneous abstraction.}

\paragraph{Simultaneous abstraction in DRT}

The proposal for reconstructing DRSs in terms of situation theory is
that they are abstracts which are either relations or types.  (See
Cooper(1993,in press) for more detailed discussion.)  The idea is that a DRS 
can be represented as an abstract such as \nexteg{}.
\beg 
\relnbox{\assign{$i$}{$X$},\assign{$j$}{$Y$}}{man($X$) \\ donkey($Y$) \\ own($X,Y$)} 
\eeg 
\ignore{\preveg{b} in linear notation is given in \nexteg{}.
\beg 
$\lambda$[\assign{$i$}{$X$},\assign{$j$}{$Y$}](man($X$) $\wedge$
donkey($Y$) $\wedge$ own($X,Y$))
\eeg 
}

The parameters abstracted over correspond to the universe of the DRS.
The fact that we use simultaneous abstraction means that we can have a
single abstraction corresponding to the DRS and that this can be
embedded in further levels of abstraction for compositional purposes
in the style of Montague.  Thus we can have the effect of
$\lambda$-DRT (Pinkal, 1991) without having to introduce
special DRS objects into our semantic universe.  The fact that we are
using arbitrary indices enables us to compose DRSs and use coindexing
to achieve discourse anaphora.  By using different indices for the
``DRS''-abstractions and the ``compositional''-abstractions we are
able to treat both DRSs and Montague style compositionality within a
unified abstraction framework.

\paragraph{Simultaneous abstraction in situation semantics}

We use simultaneous abstraction in situation semantics to treat the
variable adicity of meanings.  The basic format for a meaning is given
in \nexteg{}.
\beg 
\tabbox{{\it context roles\/}}{{\it content\/}} 
\eeg 
This follows the Montague-Kaplan view that a meaning is applied to a
context (modelled as an assignment to the roles of an abstract) to
obtain a content (corresponding to what Montague would call an
intension).  The use of simultaneous abstraction allows meanings for
different phrases to have different numbers of context
roles and indeed for the same phrase to be ambiguous with
respect to the number of roles which depend on context, without this
having as a consequence that the different meanings are different
types (or sorts) or objects or that any ordering is implied among the
roles.  The context roles are related to the notion of universe in a
DRS and in a similar way to the treatment of DRT we are able to gather
all the context roles together ``in one bag'' while still using
different levels of abstraction within the same object for the
``compositional'' abstracts in the style of Montague.  This view of
the techniques makes the situation semantics and DRT approaches look
very similar.

\section{Restrictions}

Restrictions provide a way of backgrounding information and of
expressing presuppositions.  In terms of the language $L_{\it EKN\/}$ the idea behind restriction is as follows:  
\bit 
 
\item  if $\alpha$
is any kind of term and $\phi$ is a proposition term then
$\res{\alpha}{\phi}$ (graphically, \resconjbox{$\alpha$}{$\phi$}) is a term
 
\item $\res{\alpha}{\phi} \fequals \alpha$ if $\phi$ is
true

\item  $\res{\alpha}{\phi}$ is undefined if $\phi$ is false
 
\eit 
  
In the case
where $\phi$ contains parameters it will be neither true nor false, but
given an assignment to its parameters it can be anchored to become
true or false.  Thus in the parametric case the restriction can be
seen as representing a restriction on parameters returning $\alpha$
under an assignment just in case $\phi$ under the assignment is a true
proposition. 

\ignore{
Restrictions obey various identity conditions mainly having to do with
distribution.  Some examples are
\bit 
 
\item[] $\res{(\res{\alpha}{\phi})}{\psi} \fequals \res{\alpha}{(\phi\wedge \psi)}$ 
 
\item[] $(\res{\alpha}{\phi})\wedge\beta \fequals
\res{(\alpha\wedge\beta)}{\phi}$

And similarly for the other connectives 
 
\eit 
The only place where restrictions do not distribute is when they
contain parameters within the scope of a $\lambda$.  In this case the
restrictions cannot distribute beyond the scope of the $\lambda$ and
they represent appropriateness conditions on assignments to the
abstract represented.   
}

[The uses of restrictions will be discussed in the full version of the
paper.]

\ignore{
\paragraph{Restrictions in Montague semantics}  

The situation theoretic reconstruction of Montague semantics that was
presented in the DYANA project was exactly Montague's treatment of the
PTQ fragment.  Thus there was no treatment of presupposition or sortal
restrictions and restrictions were thus not used.  It would be an
interesting exercise to add restrictions to some basic extension of
the PTQ fragment and see what treatment of presuppositions emerges.

\paragraph{Restrictions in DRT}

In the treatment of situation theoretic DRT presented in DYANA
proper names $\alpha$ are treated as introducing a restriction of the form
\nexteg{}.
\beg 
\prpnbox{$S$}{named($X,\alpha$)} 
\eeg 
Because of the distribution laws these restrictions percolate up to
the level where the $X$ is abstracted over, i.e. the level of the
topmost DRS.\footnote{This is not strictly true, although it ought to
be.  Given the way the reduction rules are implemented a restriction
will not rise above any intermediate abstraction even if it does not
bind the parameters in the restriction. This needs some further
consideration.}  Thus by making the naming condition a restriction it
can be introduced arbitrarily low down in the compositional semantics
and ``rises'' to the appropriate place determined by the scope of the
parameter to which it is attached.

\ignore{
There are other potential uses for restrictions in a situation
theoretic version of DRT but they are not exploited in the fragment
presented in this work.
}

\paragraph{Restrictions in situation semantics}

Restrictions in situation semantics are used to express
presuppositions and appropriateness conditions.  
Restrictions are a useful tool for expressing constraints which
originate on particular constituents and become constraints associated
with a whole utterance because of their distributive properties
required by the situation theory.
}

\section{A situation theoretic language}

%\begin{small}

We characterize the language $L_{\it EKN\/}$. \footnote{I am extremely grateful to Peter Ruhrberg for
comments which led to a number of improvements in the definition of
this language.}

\subsection*{Sorts}
We introduce the following \newterm{basic sorts}:
\bqt
object, situation, infon, proposition, relation, type, assignment,
individual, time, role
\eqt
\newterm{Non-basic sorts}
\bqt
If $\alpha$ is a sort other than assignment or role, then
$\alpha$-abstract is a sort.  (That is, we allow abstraction over
every sort other than assignments and roles.)
\eqt

\begin{small}
We introduce a subsort relation, $\leq$, between sorts. If
$\alpha \leq \beta$ for two sorts $\alpha$ and $\beta$, then any expression of
sort $\alpha$ is also of sort $\beta$.  This relation is characterized
by the following:
\ben 
 
\item for any sort $\alpha$, $\alpha \leq$ object
 
\item infon $\leq$ type

\item infon-abstract $\leq$ relation

\item proposition-abstract $\leq$ type 
 
\een 
\end{small}  

We call the set of sorts thus defined {\it Sorts\/}.

\begin{small}
We define two functions, {\it roles\/} and {\it sorts\/}, which have
as domain expressions of sorts relation, type and $\alpha$-abstract
(for any sort $\alpha$)
which are not parameter constants or variables.
Intuitively, if $\gamma$ is an expression of one of these sorts, then
{\it roles\/}($\gamma$) is the set of roles associated with $\gamma$
and {\it sorts\/}($\gamma$) is a set of functions with domain {\it
roles\/}($\gamma$) which yield an assignment of sorts to the roles of
$\gamma$.  In many cases {\it sorts\/}($\gamma$) will just be a
singleton set.  For example, suppose that $\gamma$ is an expression of
sort type and {\it roles\/}($\gamma$) is $\{\rho\}$, i.e. $\gamma$ has
a single role $\rho$.  Then {\it sorts\/}($\gamma$) might be
$\{\{<\rho,\mbox{situation}>\}\}$, that is, the singleton set
containing the function which
assigns the sort situation to the role $\rho$.  This would indicate
that $\gamma$ represents what  we normally call a situation type.
As a second example, suppose that $\gamma$ is a relation with two roles, $\rho_1$
and $\rho_2$, both of which may be assigned properties or both of
which may be assigned propositions.\footnote{A potential natural
language example of this is the English word \lingex{means} where it
is possible to say
\ben
\item[i.] going to the movie means taking the car

\item[ii.] that he went to the movie means that he took the car
\een
but not normally
\ben
\item[iii.] going to the movie means that he took the car

\item[iv.] that he went to the movie means taking the car
\een
}  In this case {\it sorts\/}($\gamma$) would be $\{\{<\rho_1,
property>,<\rho_2,property>\},\{<\rho_1,proposition>,<\rho_2,proposition>\}\}$.

The functions {\it roles\/} and {\it sorts\/} are required to meet the
constraints placed on them in the individual clauses below.
\end{small}

\subsection*{Variables}
We introduce denumerably many variables of each sort.  {\small We use the
following letters for variables over the basic sorts.

\begin{tabular}{ll}
$o,o_1,o_2, \ldots$ & variables over objects \\
$s,s_1,s_2, \ldots$ & variables over situations \\
$\sigma, \tau, \sigma_1, \tau_1, \sigma_2,\tau_2,\ldots$ & variables
over infons \\
$\phi,\psi, \phi_1,\psi_1,\phi_2,\psi_2, \ldots$ & variables over
propositions \\ 
$r,r_1,r_2, \ldots$ & variables over relations \\
$\zeta, \xi, \zeta_1, \xi_1, \zeta_2, \xi_2, \ldots$ & variables over
types \\
$f,g,f_1,g_1,f_2,g_2, \ldots$ & variables over assignments \\
$x,y,z,x_1,y_1,z_1,x_2,y_2,z_2,\ldots$ & variables over individuals \\
$t,t_1,t_2,\ldots$ & variables over times \\
$\rho, \rho_1,\rho_2,\ldots$ & variables over roles
\end{tabular}
}

We assume variables to range over objects of the
appropriate sort.

\subsection*{Constants}
We introduce constants of each sort.  In particular we introduce
denumerably many constants denoting parameters of each sort.  \ignore{We use the
following letters for parameter constants for the basic sorts.

\begin{tabular}{ll}
$O,O_1,O_2, \ldots$ & parameters over objects \\
$S,S_1,S_2, \ldots$ & parameters over situations \\
$\Sigma,  \Sigma_1, \Sigma_2,\ldots$ & parameters
over infons \\
$\Phi,\Psi, \Phi_1,\Psi_1,\Phi_2,\Psi_2, \ldots$ & parameters over
propositions \\ 
$R,R_1,R_2, \ldots$ & parameters over relations \\
$\Xi,  \Xi_1,  \Xi_2, \ldots$ & parameters over
types \\
$F,G,F_1,G_1,F_2,G_2, \ldots$ & parameters over assignments \\
$X,Y,Z,X_1,Y_1,Z_1,X_2,Y_2,Z_2,\ldots$ & parameters over individuals \\
$T,T_1,T_2,\ldots$ & parameters over times 
\end{tabular}
}

\begin{small}
Intuitively, parameter constants denote parameters and other constants
denote non-parametric objects of the appropriate sort.

If $\alpha$ is a relation or type constant, then {\it roles\/}($\alpha$) is a
set of role constants associated with $\alpha$, representing the set
of $\alpha$'s roles.

If $\alpha$ is a relation or type constant, then {\it
sorts\/}($\alpha$) is a set of functions with domain {\it
roles\/}($\alpha$) and range included in {\it Sorts\/}.

\end{small}

\subsection*{Terms}
\ben 

\item[]{\bf Basic terms}
 
\item If $\alpha$ is a variable or constant of sort $\gamma$, then
$\alpha$ is a term of sort $\gamma$. 

\item[]{\bf Assignment terms}

\item If $\alpha_1,\ldots,\alpha_n$ are role terms and
$\beta_1,\ldots,\beta_n$ are terms of any sort, then $[\alpha_1
\rightarrow \beta_1,\ldots,\alpha_n \rightarrow \beta_n]$ is an
assignment term with \newterm{domain} $\{\alpha_1,\ldots,\alpha_n\}$
and \newterm{range} $\{\beta_1,\ldots,\beta_n\}$.  The \newterm{value}
of $[\alpha_1 \rightarrow \beta_1,\ldots,\alpha_i \rightarrow
\beta_i,\ldots,\alpha_n \rightarrow \beta_n]$ at $\alpha_i$ is
$\beta_i$.

\begin{small}
If $\alpha_1,\ldots,\alpha_n$ are an initial segment of the natural
numbers beginning with 1, then we abbreviate $[\alpha_1
\rightarrow \beta_1,\ldots,\alpha_n \rightarrow \beta_n]$ as $[
\beta_1,\ldots, \beta_n]$. We further abbreviate $[\beta]$ as $\beta$
when it is clear from the context that an assignment is meant.

An assignment term $\beta$ is {\it syntactially appropriate\/} to a
relation or type term $\alpha$ iff 
\bqt
{\bf either} $\alpha$ is a parameter constant or variable

{\bf or}  {\it roles\/}($\alpha$) is included in the
domain of $\beta$ and there is
some $\gamma$ in {\it sorts\/}($\alpha$) that satisfies:  
\bqt
for each $\delta$ in the domain of $\beta$, the value of $\beta$ at
$\delta$ is a term of sort $\gamma(\delta)$.
\eqt
\eqt

We say that $\beta$ is {\it syntactically exactly appropriate\/} to
$\alpha$ if it is syntactically appropriate and in case $\alpha$ is
not a parameter constant or variable, $\beta$ has domain {\it
roles\/}($\alpha$) (i.e. $\beta$ is defined on exactly the
roles of $\alpha$, which is to say that it does not provide values for
roles which are not roles of $\alpha$)

\end{small}

\item[] {\bf Infon terms}

\item If $\alpha$ is a relation term and $\beta$ an assignment term
which is syntactically exactly appropriate to $\alpha$, then $\alpha(\beta)$
and $\neg\alpha(\beta)$ are terms of sort infon.

\item If $\alpha$ and $\beta$ are terms of sort infon, then
$\alpha\wedge\beta$ (\conjbox{$\alpha$ \\ $\beta$}) and
$\alpha\vee\beta$ (\conjbox{$\alpha\vee\beta$}) are terms of sort infon.

\item[] If $\alpha$ is a term of sort infon, then {\it
roles\/}($\alpha$) = \{1\} and {\it sorts\/}($\alpha$) = $\{\gamma\}$
where $\gamma$(1) = situation.  I.e., an infon is a ``situation
type''.

\item[] {\bf Proposition terms}

\item If $\alpha$ is a type term and $\beta$ an assignment term which
is syntactically exactly appropriate to $\alpha$, then $(\beta : \alpha)$
(\prpnbox{$\beta$}{$\alpha$}) is a term of sort proposition.

\item If $\alpha$ and $\beta$ are terms of sort proposition, then
$\alpha\wedge\beta$ (\conjbox{$\alpha$ \\ $\beta$}),
$\alpha\vee\beta$ (\conjbox{$\alpha\vee\beta$}) and $\neg\alpha$
(\conjbox{$\neg\alpha$}) are terms of sort proposition.

\item[] {\bf Restricted terms}

\item If $\alpha$ is a term of sort $\gamma$ (where $\gamma$ is some
sort other than role) and $\beta$ is a term of sort proposition, then
$\res{\alpha}{\beta}$ (\resconjbox{$\alpha$}{$\beta$}) is a term of
sort $\gamma$.

\item[] {\bf Abstract terms}

\item If $\alpha$ is a term of sort $\gamma$ and $\beta$ is an
assignment term whose range is a set of parameter constants occuring free
in $\alpha$, then $\lambda\beta(\alpha)$ (\tabbox{$\beta$}{$\alpha$})
is a term of sort $\gamma$-abstract.  {\it
roles\/}($\lambda\beta(\alpha)$) is the domain of $\beta$.  {\it
sorts\/}($\lambda\beta(\alpha)$) is $\{\delta\}$ where $\delta$ is
that function which returns for each term $\epsilon$ in the domain of
$\beta$ the minimal\footnote{according to the ordering `$\leq$' on sorts} sort of the parameter which is the value of $\beta$ at
$\epsilon$.

We say that in $\lambda\beta(\alpha)$ the parameter constants in the range of
$\beta$ are \newterm{bound}.  Otherwise occurrences of parameter constants are
said to be \newterm{free}.  A term which contains no free parameter constants
is said to be \newterm{closed}.

In the graphical notation we normally write infon and proposition
abstract terms of the form $\lambda\beta(\alpha)$ as
\relnbox{$\beta$}{$\alpha$} rather than \tabbox{$\beta$}{$\alpha$}.

\item[] {\bf Application terms}

\item If $\alpha$ is a term of sort $\gamma$-abstract and $\beta$ is
an assignment term which is syntactically appropriate to $\alpha$,
then $\alpha . \beta$ is a term of sort $\gamma$.

 
\een 

\subsection*{Formulae}
\ben 

\item[] We write connectives and other formula constructors such as
`$\fwedge$' and `$\fcolon$' with an underline to distinguish
them from similar symbols such as `$\wedge$'and `:' which are used in
the construction of terms.
 
\item If $(\alpha : \beta)$ is a proposition term, then $\alpha
\fcolon \beta$ is a formula.

In the special case where $\alpha$ is an infon and $\beta$ is of the
form $[1 \rightarrow \gamma]$ where $\gamma$ is a situation, we
normally write $[1 \rightarrow \gamma] \fmodels \alpha$ or more
standardly, using the abbreviated form of the assignment, $\gamma
\fmodels \alpha$.
 
\item If  $\alpha$ is a proposition term, then {\it true\/}($\alpha$)
is a formula.

\item If $\alpha$ is a term, then {\it parametric\/}($\alpha$) is a formula. 

\item If $\alpha$ and $\beta$ are terms, then $\alpha \fequals \beta$ is a
formula.

\item If $\alpha$ and $\beta$ are situation terms, then $\alpha \funlhd
\beta$ is a formula.

\item If $\alpha$ and $\beta$ are formulae and $v$ is a variable
occuring in $\alpha$, then $\alpha \fwedge \beta$, $\alpha\fvee\beta$,
$\alpha\frightarrow\beta$, $\alpha\fleftrightarrow\beta$, $\fneg\alpha$,
$\fexists v [\alpha]$, $\fforall v[\alpha]$ are all
formulae. 
 
\een 

We call a formula a sentence if it contains no free variables.

\subsection*{Axiom Schemes}

\ben

\item[] {\bf Parametric objects}

\item If $\alpha$ is a term, then {\it parametric\/}($\alpha$) is a true
formula just in case $\alpha$ contains free parameter constants.

\item $\fforall f,\zeta[f \fcolon \zeta \frightarrow \fneg {\it parametric\/}(f)
\fwedge \fneg {\it parametric\/}(\zeta)]$

\item[]{\bf Propositions}

\item If $(f:\zeta)$ is a proposition term and $\zeta$ is an abstract
term, then ${\it true\/}((f:\zeta)) \fleftrightarrow {\it true\/}(\zeta.f)$

\item $\fforall f_1,f_2,\zeta_1,\zeta_2[(f_1:\zeta_1) \fequals (f_2:\zeta_2)
\fleftrightarrow f_1 \fequals f_2 \fwedge \zeta_1 \fequals \zeta_2]$
 
\item $\fforall f,\zeta[{\it true\/}((f:\zeta)) \fleftrightarrow f
\fcolon \zeta]$ 
 
\item $\fforall \phi [\phi \wedge \phi \fequals \phi]$

\item $\fforall \phi [\phi \vee \phi \fequals \phi]$

\item $\fforall \phi, \psi [\phi\wedge \psi \fequals \psi\wedge\phi]$

\item $\fforall \phi, \psi [\phi\vee \psi \fequals \psi\vee\phi]$ 

\item $\fforall \phi_1,\phi_2,\phi_3 [(\phi_1\wedge\phi_2)\wedge\phi_3
\fequals \phi_1\wedge(\phi_2\wedge\phi_3)]$

\item $\fforall \phi_1,\phi_2,\phi_3 [(\phi_1\vee\phi_2)\vee\phi_3
\fequals \phi_1\vee(\phi_2\vee\phi_3)]$

\item $\fforall \phi,\psi [{\it true\/}(\phi\wedge\psi) \fleftrightarrow
{\it true\/}(\phi) \fwedge {\it true\/}(\psi)]$

\item $\fforall \phi,\psi [{\it true\/}(\phi\vee\psi) \fleftrightarrow
{\it true\/}(\phi) \fvee {\it true\/}(\psi)]$ 

\item $\fforall \phi [ {\it true\/}(\neg(\phi)) \frightarrow
\fneg{\it true\/}(\phi)] $

\item $\fforall \phi[{\it false\/}(\phi) \fleftrightarrow \fneg {\it
parametric\/}(\phi) \fwedge \fneg {\it true\/}(\phi)]$


\item[]{\bf Infons}

\ignore{
\item $\fforall \sigma [\sigma = \lambda[\nu]((\nu\ :\ \sigma))]$,
where $\nu$ is a parameter constant of sort situation not occurring
freely in $\sigma$.\footnote{This may be dropped if there are
complications with non-well-foundedness.}
}

\item $\fforall f_1,f_2,r_1,r_2[r_1(f_1) \fequals r_2(f_2)
\fleftrightarrow f_1 \fequals f_2 \fwedge r_1 \fequals r_2]$

\item $\fforall f_1,f_2,r_1,r_2[\neg r_1(f_1) \fequals \neg r_2(f_2)
\fleftrightarrow f_1 \fequals f_2 \fwedge r_1 \fequals r_2]$

\item $\fforall \sigma [\sigma \wedge \sigma \fequals \sigma]$

\item $\fforall \sigma [\sigma \vee \sigma \fequals \sigma]$

\item $\fforall \sigma,\tau [\sigma\wedge\tau \fequals \tau\wedge\sigma]$

\item $\fforall \sigma,\tau [\sigma\vee\tau \fequals \tau\vee\sigma]$

\item $\fforall \sigma_1,\sigma_2,\sigma_3 [(\sigma_1\wedge\sigma_2)\wedge\sigma_3
\fequals \sigma_1\wedge(\sigma_2\wedge\sigma_3)]$

\item $\fforall \sigma_1,\sigma_2,\sigma_3 [(\sigma_1\vee\sigma_2)\vee\sigma_3
\fequals \sigma_1\vee(\sigma_2\vee\sigma_3)]$

\item[]{\bf Situations}

\item $\fforall s_1, s_2,  [ \fforall \sigma (s_1 \fmodels \sigma \fleftrightarrow
s_2 \fmodels \sigma) \frightarrow s_1 \fequals s_2]$

\item $\fforall s,\sigma,\tau[s \fmodels \sigma\wedge\tau
\fleftrightarrow s \fmodels \sigma \fwedge s \fmodels \tau]$

\item $\fforall s,\sigma,\tau[s \fmodels \sigma\vee\tau
\fleftrightarrow s \fmodels \sigma \fvee  s \fmodels \tau]$

\item $\fforall s,\sigma[s \fmodels \neg\sigma \frightarrow \fneg s
\fmodels \sigma]$

\item $\fforall s_1,s_2[ s_1 \funlhd s_2 \fleftrightarrow \fforall \sigma
[s_1 \fmodels \sigma \frightarrow s_2 \fmodels \sigma] ]$

\item $\fforall s_1,s_2 \fexists s [s_1 \funlhd s \fwedge s_2 \funlhd s]$

\item[]{\bf Restrictions}

\item $\fforall o,\phi[ {\it true\/}(\phi) \frightarrow \res{o}{\phi} \fequals o]$

\ignore{
\item $\forall o,\phi[ {\it false\/}(\phi) \rightarrow \res{o}{\phi} = *]$
}

\item $\fforall o,\phi_1,\phi_2[\res{(\res{o}{\phi_1})}{\phi_2} \fequals \res{o}{\phi_1\wedge
\phi_2}]$

\item $\fforall \alpha_1,\ldots,\alpha_n,o_1,\ldots,o_n, \phi[[\alpha_1
\rightarrow o_1,\ldots,\alpha_i
\rightarrow \res{o_i}{\phi},\ldots,\alpha_n \rightarrow o_n] \fequals $ \\
$\res{[\alpha_1
\rightarrow o_1,\ldots,\alpha_i
\rightarrow o_i,\ldots,\alpha_n \rightarrow o_n]}{\phi}]$

\item $\fforall r,f,\phi[(\res{r}{\phi})(f) \fequals \res{r(f)}{\phi} \fwedge
r(\res{f}{\phi}) \fequals \res{r(f)}{\phi}]$

\item $\fforall r,f,\phi[\neg(\res{r}{\phi})(f) \fequals \res{\neg r(f)}{\phi} \fwedge
\neg r(\res{f}{\phi}) \fequals \res{\neg r(f)}{\phi}]$

\item $\fforall \sigma, \tau,\phi [(\res{\sigma}{\phi}) \wedge \tau \fequals
\res{(\sigma\wedge\tau)}{\phi}]$

\item $\fforall \sigma, \tau,\phi [(\res{\sigma}{\phi}) \vee \tau \fequals
(\res{(\sigma\vee\tau)}{\phi}]$

\item $\fforall f, \zeta, \phi [((\res{f}{\phi})\ : \ \zeta) \fequals \res{(f\ :\
\zeta)}{\phi} \fwedge (f\ :\ \res{\zeta}{\phi}) \fequals \res{(f\ :\
\zeta)}{\phi}]$

\item $\fforall \psi_1, \psi_2,\phi [(\res{\psi_1}{\phi}) \wedge \psi_2 \fequals
\res{(\psi_1\wedge\psi_2)}{\phi}]$

\item $\fforall \psi_1, \psi_2,\phi [(\res{\psi_1}{\phi}) \vee \psi_2 \fequals
\res{(\psi_1\vee\psi_2)}{\phi}]$

\ignore{
\item If $\gamma$ contains no variables and no free parameter constants in the range of $\beta$,
then $\lambda\beta(\res{\alpha}{\gamma}) \fequals
\res{\lambda\beta(\alpha)}{\gamma}$\footnote{This intuitively correct
requirement is usually left out because it seems to cause complications,
e.g. in computing normal forms}
}

\item[] {\bf Abstracts and application}

Let $\alpha^\nu_\mu$ represent the result of substituting $\mu$ for
$\nu$ in $\alpha$.

\item If $\lambda\beta(\alpha)$ is an abstract term containing no
variables, $\nu$ is a parameter constant in the range of $\beta$ and
$\mu$ is a parameter constant which doesn't occur, either bound or
free, in $\alpha$, then $\lambda\beta(\alpha) =
\lambda\beta(\alpha)^\nu_\mu$.

\item If $\lambda\beta(\alpha)$ is an abstract term containing no
variables and with roles
$\rho_1,\ldots,\rho_n$ (i.e. this is the domain of $\beta$), the range
of $\beta$ is $\nu_1,\ldots,\nu_n$ such that  the value of $\beta$ at
$\rho_i$ is $\nu_i$, $\delta$ is an assignment with domain including
$\rho_1,\ldots,\rho_n$ and range including $\mu_1,\ldots,\mu_n$ such
that the value of $\delta$ at $\rho_i$ is $\mu_i$ and
$\lambda\beta(\alpha) . \delta$ is an application term, then
$\lambda\beta(\alpha) . \delta \fequals \alpha^{\nu_1,\ldots,\nu_n}_{\mu_1,\ldots,\mu_n}$
 
\een 
       
\ignore{
\subsection*{Implementation and the computation of reduced forms}

Only the term part of the language has been implemented with parameter
constants but without variables.  Reduced forms are computed according
to the rules given below.  This does not strictly speaking yield a
normal form, even for the term sublanguage without variables, since
there are certain terms for which $\beta$-conversion does not result
in a reduction.  Such terms do not arise in the semantic treatments we
have implemented.  For a general discussion of the characterization of
infinite reduction paths in the untyped $\lambda$-calculus see
S{\o}rensen (1995).  The reduced forms which are computed can be
obtained by applying the following rules to variable free terms:

\ben 

\item[] {\it Distribute conjunction and disjunction in Austinian
propositions\/} 
 
\item $(s\ :\ \sigma) \wedge (s\ :\ \tau) \Rightarrow (s\ :\
\sigma\wedge\tau) $\footnote{This reduction is not supported by an
identity, but the propositions are required to be equivalent.} 
 
\item $(s\ :\ \sigma) \vee (s\ :\ \tau) \Rightarrow (s\ :\
\sigma\vee\tau) $\footnote{This reduction is not supported by an
identity, but the propositions are required to be equivalent.}

\item[] {\it Apply $\beta$-conversion\/}

\item If $\lambda\beta(\alpha)$ is an abstract with roles
$\rho_1,\ldots,\rho_n$ (i.e. this is the domain of $\beta$), the range
of $\beta$ is $\nu_1,\ldots,\nu_n$ such that  the value of $\beta$ at
$\rho_i$ is $\nu_i$, $\delta$ is an assignment with domain including
$\rho_1,\ldots,\rho_n$ and range including $\mu_1,\ldots,\mu_n$ such
that the value of $\delta$ at $\rho_i$ is $\mu_i$ and
$\lambda\beta(\alpha) . \delta$ is an application term, then
$\lambda\beta(\alpha) . \delta \Rightarrow
\alpha^{\nu_1,\ldots,\nu_n}_{\mu_1,\ldots,\mu_n}$

\item[] {\it Distribute restrictions to have the widest possible scope
over a term\/}

\item $\res{(\res{o}{\phi_1})}{\phi_2} \Rightarrow \res{o}{\phi_1\wedge
\phi_2}$

\item $[\alpha_1
\rightarrow o_1,\ldots,\alpha_i
\rightarrow \res{o_i}{\phi},\ldots,\alpha_n \rightarrow o_n] \Rightarrow \res{[\alpha_1
\rightarrow o_1,\ldots,\alpha_i
\rightarrow o_i,\ldots,\alpha_n \rightarrow o_n]}{\phi}$

\item $(\res{r}{\phi})(f) \Rightarrow \res{r(f)}{\phi}$

\item $r(\res{f}{\phi}) \Rightarrow \res{r(f)}{\phi}$

\item $\neg(\res{r}{\phi})(f) \Rightarrow \res{\neg r(f)}{\phi}$

\item $\neg r(\res{f}{\phi}) \Rightarrow \res{\neg r(f)}{\phi}$

\item $(\res{\sigma}{\phi}) \wedge \tau \Rightarrow
\res{(\sigma\wedge\tau)}{\phi}$

\item $\sigma \wedge (\res{\tau}{\phi}) \Rightarrow
\res{(\sigma\wedge\tau)}{\phi}$

\item $(\res{\sigma}{\phi}) \vee \tau \Rightarrow
\res{(\sigma\vee\tau)}{\phi}$

\item $\sigma \vee (\res{\tau}{\phi}) \Rightarrow
\res{(\sigma\vee\tau)}{\phi}$

\item $(\res{f}{\phi}\ : \ \zeta) \Rightarrow \res{(f\ :\
\zeta)}{\phi}$
 
\item $(f\ :\ \res{\zeta}{\phi}) \Rightarrow \res{(f\ :\
\zeta)}{\phi}$

\item $(\res{\psi_1}{\phi}) \wedge \psi_2 \Rightarrow
\res{(\psi_1\wedge\psi_2)}{\phi}$

\item $\psi_1 \wedge (\res{\psi_2}{\phi}) \Rightarrow
\res{(\psi_1\wedge\psi_2)}{\phi}$

\item $(\res{\psi_1}{\phi}) \vee \psi_2 \Rightarrow
\res{(\psi_1\vee\psi_2)}{\phi}$

\item $\psi_1 \vee (\res{\psi_2}{\phi}) \Rightarrow
\res{(\psi_1\vee\psi_2)}{\phi}$

\ignore{
\item  If $\phi$ contains no free parameters in the range of $\beta$,
then $\lambda\beta(\res{\alpha}{\phi}) \Rightarrow
\res{\lambda\beta(\alpha)}{\phi}$\footnote{This rule is usually left out because it seems to cause complications
in computing normal forms}
}
\een 
}

%\end{small}

\section{Making an honest language of $L_{\it EKN\/}$}

The difficulties in making an honest language of this lie in providing
an appropriate model for it.  The subtle combination of a version of
the untyped $\lambda$-calculus, simultaneous abstraction and
restrictions (with their distributive properties and interaction with
truth) seems to provide a challenge to model theorists which is
painful, though not obviously impossible (I surmise) to overcome.  We
seem to need the Aczel-Lunnon theory of abstracts as non-sets, but it
apparently has a reputation for being very difficult among peope who
are not directly involved with it. 

I believe that there is great potential here for unifying a number of
approaches within natural language semantics and that it is quite
close to a number of similar proposals which currently use type-theory as a
means of expression.  I am thinking, for example, of Muskens' (1995)
work on recasting DRT in terms of type theory.  What the situation
theory offers us that is not currently offered by type-theoretic
approaches is a treatment of intensionality  within structured
semantic universes.  I believe that this is a prize which is worth the
investment of a model theorist's effort.  [In fact, I would be
overjoyed if somebody were to provide a model between now and the
final version of this paper, or explain why there is no model.]

\begin{Bibliography}

\bibitem
Aczel, Peter, David Israel, Yasuhiro Katagiri and Stanley Peters (ed.)
{\it Situation Theory and its Applications, Volume 3\/}, CSLI,
Stanford.
\bibitem
Aczel, Peter and Rachel Lunnon (1991) Universes and
Parameters, in {\it Situation Theory and its Applications, Vol. 2} ed.
by Jon Barwise, Jean Mark Gawron, Gordon Plotkin and Syun Tutiya, CSLI

\bibitem
Barwise, Jon and Robin Cooper (1991) Simple Situation Theory and
its Graphical Representation, Indiana University Logic Group Preprint
No. IULG-91-8 and in Seligman (1991)
\bibitem
Barwise, Jon and Robin Cooper (1993) 
Extended Kamp Notation: a Graphical Notation for Situation Theory, in
Aczel, Israel, Katagiri and Peters (1993),  pp. 29--54.
\bibitem
Cooper, Robin (1993), ed., {\it Integrating Semantic Theories\/},
DYANA-2 Report R2.1.A, available from ILLC/Department of Philosophy,
University of Amsterdam and \\ {\tt ftp://illc-sun.illc.uva.nl/pub/dyana}
\bibitem
Cooper, Robin (1995) The Role of Situations in Generalized Quantifiers, in {\it
Handbook of Contemporary Semantic Theory\/}, ed. by S. Lappin,
Blackwell, pp. 65--86
\bibitem
Cooper, Robin (in press) The Attitudes in Discourse Representation Theory and Situation
  Semantics, {\it Proceedings of ITALLC94\/}, CSLI
\bibitem
Cooper, Robin (to appear) Austinian propositions, Davidsonian events
and perception complements, in Ginzburg, Khasidashvili, Levy and
Vallduvi (eds.) {\it The Tbilisi Symposium on Language, Logic and
Computation: selected papers\/}, CSLI Publications.

\bibitem
Lunnon, Rachel (1991) {\it Generalized Universes}, Ph.D.
thesis, University of Manchester

\bibitem
Lunnon, Rachel (1992) Course notes for LLI Summer School.
\bibitem
Muskens, Reinhard (1995) Order-Independence and Underspecification, in
Groenendijk, J. (ed.) {\it Ellipsis, Underspecification, Events and
More in Dynamic Semantics\/}, DYANA-2 Report R2.2.C, available from ILLC/Department of Philosophy,
University of Amsterdam and \\ {\tt ftp://illc-sun.illc.uva.nl/pub/dyana}
\bibitem
Pinkal, Manfred (1991): {\em On the
Syntactic-Semantic 
Analysis of Bound Anaphora\/}, Proceedings of the 5th EACL, Berlin
\bibitem
Ruhrberg, Peter (1994) A simultaneous abstraction calculus, in Cooper,
R. and Groenendijk, J., eds., {\it Integrating Semantic Theories II\/},
DYANA-2 Report R2.1.B, available from ILLC/Department of Philosophy,
University of Amsterdam and {\tt ftp://illc-sun.illc.uva.nl/pub/dyana}
\bibitem
Seligman, Jerry, ed. (1991) {\it Partial and Dynamic Semantics
III}, {\sc dyana} Deliverable R2.1.C, Centre for Cognitive Science,
University of Edinburgh.

\ignore{
\bibitem
S\o rensen, Morton Heine (1995) Characterization of Infinite Reduction
Paths in Untyped $\lambda$-calculus.  Abstract in {\it Tbilisi
Symposium on Language, Logic, and Computation:  19--22 October,
Gudauri, Georgia\/}, Research Paper HCRC/RP-72, Human Communication
Research Centre, University of Edinburgh.
}

\end{Bibliography}

\ignore{
\begin{Bibliography}


\bibitem
Barwise, Jon and Robin Cooper (1991) Simple Situation
Theory and its Graphical Representation, DYANA
deliverable R2.1C, {\it Partial and Dynamic Semantics
III}, ed. by Jerry Seligman.

\bibitem
Barwise, Jon and Robin Cooper (in press) Extended Kamp Notation: a
Graphical Notation for Situation Theory, in {\it Situation Theory and
its Applications, Vol. 3}, ed. by Peter Aczel, David Israel, Yasuhiro
Katagiri and Stanley Peters, Stanford: CSLI 

\bibitem
Black, Alan (1992) Embedding DRT in a Situation Theoretic Framework,
{\it Proceedings of the fifteenth International Conference on
Computational Linguistics}, {\sc coling-92}, pp. 1116--1120

\bibitem
Black, Alan (1993) {\it A Situation Theoretic Approach to
Computational Semantics}, PhD thesis, Department of AI, University of
Edinburgh.

\bibitem
Church, Alonzo (1951) A formulation of the logicof sense and
denotation, in {\it Structure, Method and Meaning\/}, ed. by P. Henle,
H.M. Kallen, and S.K. Langer, Liberal Arts Press, New York, pp. 3--24.


\bibitem
Harper, Robert, Furio Honsell and Gordon Plotkin (1987) A Framework
for Defining Logics, in {\it Symposium on Logic in Computer Science},
IEEE.

\bibitem
Johnson, Mark and Martin Kay (1990): {\em 
Semantic
Abstraction and Anaphora}, Proceedings of COLING 90, Helsinki.

\bibitem
Kamp, Hans (1990) Prolegomena to a Structural Theory of Belief and
Other Attitudes, in {\it Propositional Attitudes:  The Role of Content
in Logic, Language and Mind}, ed. by C. Anthony An derson and Joseph
Owens, CSLI.

\bibitem
Kamp, Hans and Uwe Reyle (1993) {\it From
Discourse to Logic: Introduction to Model Theoretic
Semantics of Natural Language, Formal Logic and Discourse
Representation Theory}, Dordrecht: Kluwer


\bibitem
Muskens, Reinhard (1989) {\it Meaning and Partiality}, PhD thesis, University
of Amsterdam



\bibitem
Sannella, Donald and Andrzej Tarlecki (1992) Toward Formal Development
of Programs from Algebraic Specifications: Model-theoretic
Foundations, {\it Proceedings of the Nineteenth International
Colloquium on Automata, Languages and programming}, Lecture Notes in
Computer Science, Springer Verlag.

\bibitem
Thomason, Richmond (1980) A Model Theory for Propositional Attitudes,
{\it Linguistics and Philosophy\/}, Vol. 4, No. 1, pp. 47--70.

\end{Bibliography}
}




 
\bibliography{bibliography} 
 
\end{document} 
