quant.tex

\chapter{Witness-based quantification}
\label{ch:quant}
\setcounter{equation}{0}



\section{Introduction}

In this chapter we are going to explore how the TTR approach to
semantics we have developed gives us a novel treatment of quantification and binding in
natural language.

In Section~\ref{sec:quantification} we are going to propose a revision of witness conditions for
quantificational ptypes which will constitute what we will call a
\textit{witness based} account of generalized quantifiers. % which will be inconsistent with some of what
% we said before in the book about their witness conditions  --
% eventually we need to go back and revise the previous discussion and
% also the section on anaphora following this section.
The motivation
for this is in part to get a neater treatment of anaphora, and a more
general treatment along the lines of \cite{LueckingGinzburg2019}.
   
In Section~\ref{sec:long-distance} we will take a brief look at how
long distance dependencies can be treated as preparation for our
treatment of quantifier scope and binding in Chapter~\ref{ch:underspec}.


    

\section{Quantifiers and their witness sets}
\label{sec:quantification}

\subsection{Conservativity and dynamic generalized quantifiers}

Here we review the treatment of quantifiers that we have presented so
far and its relation to the notion of \textit{conservativity} which we
will discuss here.  This property of conservativity facilitates the
witness-based account of quantifiers that we will undertake below.

In Chapter~\ref{ch:commonnouns}, example (\ref{ex:dynqconstr}), we
introduced the notion of dynamic generalized quantifier and pointed
out that one of the original motivations for them was what is known as
donkey anaphora which we will discuss in Section~\ref{sec:anaph}.
Here we will point out a connection between dynamic quantifiers and
conservativity of quantifiers, noted in \cite{Chierchia1995}.  The informal way to state
conservativity for quantifiers is as in \nexteg{a} and an example is
given in \nexteg{b}.
\begin{ex} 
\begin{subex} 
 
\item Q A B is true just in case Q A A\&B is true 
 
\item \textit{every farmer likes a donkey} is true just in case
  \textit{every farmer is a farmer and likes a donkey} (or more
  naturally, \textit{every farmer is a farmer who likes a donkey}) is true
 
\end{subex} 
   
\end{ex} 
Most, if not all, natural language quantifiers have this
property.\footnote{For discussion, see \cite{PetersWesterstahl2006},
  p. 138f.}

Now consider the discussion of dynamic generalized quantification in Chapter~\ref{ch:commonnouns}, Section~\ref{sec:dgqs}.  There in
example~(\ref{ex:dynqconstr}) we gave dynamic versions of generalized
quantifier interpretations of noun-phrases.  % We can give a general characterization of the witness
% conditions for dynamic generalized quantifiers as in \nexteg{}, where
% $q$ is a predicate corresponding to a quantifier and $q^*$ is the
% relation between sets corresponding to $q$ in classical generalized
% quantifier theory.
% \begin{ex} 
% $e:q(P,Q)$ iff $q^*$ holds between $\downP{P}$ and
% $\downP{Q|_{\mathcal{F}(P.\mathrm{fg})}\restriction e}$
% \label{ex:witness-cond-GQ}
% \end{ex} 
% According to the definitions given in Chapter~\ref{ch:commonnouns},
% $\downP{Q|_{\mathcal{F}(P.\mathrm{fg})}\restriction e}$ is the set of
% individuals which have property $Q|_{\mathcal{F}(P.\mathrm{fg})}$ in
% $e$ and $Q|_{\mathcal{F}(P.\mathrm{fg})}$ is $Q$ with its
% domain restricted by $P$ (example~(\ref{ex:function-restriction}), p.~\pageref{ex:function-restriction}).
We spell out the witness condition for the quantificational ptype, \nexteg{b},
corresponding to \textit{every dog runs} in \nexteg{}.  % Here, as
% before, we only represent the foregrounds of the properties which are
% arguments to the predicate `every' in order to make the presentation
% clearer.

\begin{ex} 
\begin{subex} 
 
\item dog$'$ = $\ulcorner\lambda r$:\smallrecord{\smalltfield{x}{\textit{Ind}}}
    . \smallrecord{\smalltfield{e}{dog($r$.x)}}$\urcorner$ 

run$'$ = $\ulcorner\lambda r$:\smallrecord{\smalltfield{x}{\textit{Ind}}}
    . \smallrecord{\smalltfield{e}{run($r$.x)}}$\urcorner$
 
\item $T$ = every(dog$'$, run$'\mid_{\mathfrak{F}(\text{dog}')}$)

\item \begin{tabbing}
$s:T$ \=iff
$\downP{\text{dog}'}\subseteq\downP{\text{run}'|_{\mathcal{F}(\text{dog}')}\restriction
s}  $ \hspace*{2em}(witness condition for `every', p.~\pageref{ex:witcond-every})\\
\> iff  $\downP{\text{dog}'}\subseteq\downP{\text{run}'|_{\text{\smallrecord{\smalltfield{x}{\textit{Ind}}\\\smalltfield{e}{dog(x)}}}}\restriction
s}  $ \hspace*{2em}(fixed point types, p.~\pageref{ex:fixedpointtype})\\
\> iff $\downP{\text{dog}'}\subseteq$ [$\downarrow\lambda
r$:\smallrecord{\smalltfield{x}{\textit{Ind}}}\d{$\wedge$}\smallrecord{\smalltfield{x}{\textit{Ind}}\\\smalltfield{e}{dog(x)}}
     . \smallrecord{\smalltfield{e}{run($r$.x)}}$\restriction s$ ]
     \hspace*{2em} (function restriction, p.~\pageref{ex:function-restriction})\\
\> iff $\downP{\text{dog}'}\subseteq$ [$\downarrow\lambda r$:\smallrecord{\smalltfield{x}{\textit{Ind}}\\\smalltfield{e}{dog(x)}}
     . \smallrecord{\smalltfield{e}{run($r$.x)}}$\restriction s$ ]
     \hspace*{2em}\begin{minipage}{.3\textwidth}(merge, p.~\pageref{pg:merge})\end{minipage}\\
\> iff $\downP{\text{dog}'}\subseteq$ [$\downarrow\lambda r$:\smallrecord{\smalltfield{x}{\textit{Ind}}\\\smalltfield{e}{dog(x)}}
     . \smallrecord{\smallrfield{e}{$s$}{run($r$.x)}}
     ]\hspace*{2em}\begin{minipage}{.3\textwidth}(property restriction,
      p.~\pageref{pg:property-restriction})\end{minipage}\\
\> iff \=$\{a\mid\exists r$:\smallrecord{\smalltfield{x}{\textit{Ind}}}
  $\wedge
  r.\text{x}=a\wedge\down{\text{\smallrecord{\smalltfield{e}{dog($r$.x)}}}}\not=\emptyset\}$\\
\>\>$\subseteq\{a\mid\exists r$:\smallrecord{\smalltfield{x}{\textit{Ind}}\\\smalltfield{e}{dog(x)}}
  $\wedge
  r.\text{x}=a\wedge\down{\text{\smallrecord{\smallrfield{e}{$s$}{run($r$.x)}}}}\not=\emptyset\}$
  \hspace*{2em}($\downarrow$, p.~\pageref{pg:property-extension-rev})
  \\
\> iff
$\{a\mid\down{\text{dog}(a)}\not=\emptyset\}\subseteq\{a\mid\down{\text{dog}(a)}\not=\emptyset\wedge\exists
s'[s'\underline{\varepsilon}s\wedge
s':\text{run}(a)]\}$\\
\>\`\begin{minipage}{.3\textwidth}(Arity of `dog', `run' and set
extension of records,  p.~\pageref{pg:set-reduction-gq}ff)\end{minipage}\\ 
\> iff $\{a\mid\exists s'[s':\text{dog}(a)]\}\subseteq\{a\mid\exists
s'[s':\text{dog}(a)]\wedge\exists
s'[s'\underline{\varepsilon}s\wedge s':\text{run}(a)]\}$ \\
\>\`\begin{minipage}{.3\textwidth}($\down{T}$, p.~\pageref{pg:type-extension})\end{minipage}
\end{tabbing} 
\end{subex} 
\label{ex:witnessconds-edr}   
\end{ex} 
  


\subsection{Witness sets}



The classical view of quantifiers is based on the notion that noun
phrases represent sets of sets or set of properties and the definition of a
quantifier involves characterizing which set of sets or properties it
represents.  This was the view presented, for example, in
\cite{BarwiseCooper1981}.  Associated with this was the notion of
\textit{witness set} defined by Barwise and Cooper as in \nexteg{}.
\begin{ex} 
A \textit{witness set} for a quantifier $D(A)$ living on $A$ is any
subset $w$ of $A$ such that $w\in D(A)$. 
\end{ex} 
In \preveg{} $D$ was used as the function corresponding to a
determiner such as \textit{some} or \textit{most} mapping a set $A$
(corresponding, for example, to the set denoted by a common noun phrase such
as  \textit{farmer} or \textit{farmer who owns a donkey}) to a set of
sets.  The notion \textit{lives on} used by Barwise and Cooper
corresponds to what was later in the literature referred to as
\textit{conservativity}.  Their definition of the lives-on property,
slightly simplified by removing reference to the model, is given in \nexteg{}.
\begin{ex} 
A quantifier $Q$ \textit{lives on} a set $A$ if $Q$ is a set of sets
with the property that
\begin{quote}
$X\in Q \text{ iff } (X\cap A)\in Q$
\end{quote}  
\end{ex} 
This means that the notion of witness set given by Barwise and Cooper
is defined for conservative quantifiers.  Examples of witness sets
that they give include: a witness set for the quantifier corresponding
to a proper name \textit{John} as the singleton set containing the
individual John;  a witness set corresponding to \textit{a woman} as
any non-empty set of women; a witness set corresponding to
\textit{most women} as a set of women which contains most women.

The notion of witness set
was introduced by Barwise and Cooper in a section called
\textit{Processing Quantified Statements}.  It was introduced 
as an auxiliary notion which could be used in an account of how an
agent might evaluate the truth of a quantified statement.  This
suggests that it should play an important role in a theory of
semantics like ours which is oriented towards explaining cognitive
semantic processing, especially if it is a theory which attempts to do
this in terms of judgements that objects (including situations) are
witnesses of types.  It seems natural to make a link between the
notion of witnesses for types and the notion of witnesses for
quantifiers.  We will go further and suggest that the characterization
of the meaning of determiners is based on witness sets, thus elevating
the witness sets from an auxiliary notion derived from the meaning
assigned to quantifiers to the central notion which characterizes the
distinctions between the various quantifier meanings available, just
as in type theory the notion of meaning is characterized in terms of
the witness conditions for types.  In doing this we will be going at
least part way to meeting some of the requirements of the proposals by \cite{GinzburgPurver2008,LueckingGinzburg2019}.

In the literature on generalized quantifiers \cite{Benthem1984}
introduced the perspective that we should think of determiners as
representing relations between sets rather than as mappings from sets
to families of sets.  This is reflected in our characterization of
quantifier relations as relations between properties (which can be
used to generate the set of objects which have the property) and the
use of ptypes constructed with quantifier relations and two properties
as arguments.

With each quantifier relation, $q$, and property, $P$, we will
associate a type of witness sets $q^w(P)$.  For example, a set, $X$,
is of type $\text{most}^w(P)$ if $X$ is a set of objects with property
$P$ which contains most of the objects which have property $P$.  We
will say that a witness for the quantificational ptype `most($P$,
$Q$)' is a pair (coded as a record and thus corresponding intuitively
to a situation) consisting of the set, $X$, where  $X:q^w(P)$
(i.e. $X$ is a witness set for $q$ and $P$) and a function, $f$,  whose domain
is $X$ and such that for any $a\in X$, $f(a)$ is a situation which
shows that $a$ has property $Q$.  In general for distributive readings
of monotone increasing
quantifiers, $q$, we can say that a witness for $q(P, Q)$ provides a
witness set $X$ of type $q^w(P)$ and a function which shows that every
member of $X$ has the property $Q$. For distributive readings of
monotone decreasing quantifiers we need a different kind of function
together with the witness set.  Here we have to check that everything
which has both property $P$ and property $Q$ is a member of the
witness set.  Thus we need a function, $f$, whose domain is the set of
objects having both $P$ and $Q$, such that if $a$ is in this set then
$f(a)$ is a situation which shows that $a$ is a member of the witness
set $X$.  These two kinds of functions correspond exactly to the
evaluation procedures suggested in \cite{BarwiseCooper1981} quoted in
\nexteg{}.
\begin{ex} 
\textit{To evaluate $X\in D(A)$ do the following:}
\begin{enumerate} 
 
\item Take some subset $w$ of $A$ which you know to be in $D(A)$ 
 
\item 
\begin{enumerate} 
 
\item[(i)] For mon$\uparrow$ $D(A)$, check $w\subseteq X$. 
 
\item[(ii)] For mon$\downarrow$ $D(A)$, check $(X\cap A)\subseteq w$
 
 
\end{enumerate} 
\item If there is such a $w$, the sentence is true.  Otherwise it is false.   
 
\end{enumerate} 
   
\end{ex} 

Using pairs of witness sets and functions as witnesses for
quantificational ptypes is also closely related to
the treatment of quantification in Martin-Löf type theory using
$\Sigma$-types and dependent types.  (See, for example,  discussion in
\citealp{Ranta1994}.)  A witness for the $\Sigma$-type \nexteg{a}
would be an ordered pair as characterized in \nexteg{b}.
\begin{ex} 
\begin{subex} 
 
\item $(\Sigma x:A)B(x)$ 
 
\item $\langle a,b\rangle$ where $a:A$ and $b:B(a)$ 
 
\end{subex} 
   
\end{ex} 

In the following subsections we will develop the tools we need to make
our analysis precise in terms of the TTR machinery we have developed
so far to create a witness-based analysis of quantfiers.  We will also
consider how we can move away from a set-based account of
quantification to a type-based approach where we can estimate the
probability of a quantificational ptype being witnessed on the basis
of our previous experience.  
    

\subsection{Relating properties, types and sets}

% [????In this section we revise the definition of properties.  We
% probably need to go back and revise previous definitions for
% consistency.]

% We first define a type of record types whose labels include a certain
% set of labels.  Let $L$ be a set of labels, then \textit{RecType}$_L$
% is a type.  $T$ : \textit{RecType}$_L$ iff $T$ : \textit{RecType} and
% $L\subseteq\text{labels}(T)$.  [????Check whether `labels' defined for
% record types -- it is defined for records.]

% Now we can define \textit{Ppty} to be the type in \nexteg{}.
% \begin{ex} 
% \record{\tfield{bg}{\textit{RecType}$_{\{x\}}$}\\
%         \tfield{fg}{(bg$\rightarrow$\textit{RecType})}} 
% \end{ex} 
% A witness for this type,  a property, would be something like
% \nexteg{}, ``the property of being a dog''.
% \begin{ex} 
% \record{\field{bg}{\smallrecord{\smalltfield{x}{\textit{Ind}}}}\\
%         \field{fg}{$\lambda
%           r$:\smallrecord{\smalltfield{x}{\textit{Ind}}} . \record{\tfield{e}{dog($r$.x)}}}} 
% \end{ex} 
% This is a cumbersome notation for a property so we abbreviate it as
% \nexteg{}.
% \begin{ex} 
% $\ulcorner\lambda
%           r$:\smallrecord{\smalltfield{x}{\textit{Ind}}}
%           . \record{\tfield{e}{dog($r$.x)}}$\urcorner$ 
% \label{ex:ppty-dog}
% \end{ex}
% If $P$ is a property we will also use the notation $P(a)$ to represent $P.\text{fg}(a)$.
 
% \preveg{} is a property of individuals  and we will have a subtype of
% \textit{Ppty}, \textit{Ppty}(\textit{Ind}), to represent this more
% specific type of property. In general we give the definition in
% \nexteg{}.
% \begin{ex} 
% \begin{subex} 
 
% \item if $T$ is a type, then
% \textit{Ppty}($T$) is a type 
 
% \item $P$ : \textit{Ppty}($T$) iff
% $P$ : \textit{Ppty} and $P$.bg$^{\text{x}}$ is
% \smallrecord{\smalltfield{x}{$T$}} 
 
% \end{subex} 
   
% \end{ex} 
% Here we use $P$.bg$^{\text{x}}$
% to represent the generalization of $P$.bg to its `x'-field as
% characterized in Appendix~\ref{app:gen-rectypes}, that is the type
% whose only field is the `x'-field of $P$.bg. 

A property, $P$, can be \textit{pure}, as in \nexteg{a}, that is,
$P$.bg has exactly one field, the required `x'-field;  or it can be
restricted by including additional fields in the background as in
\nexteg{b}, the restricted property
of being an individual which is a dog that barks.
\begin{ex} 
\begin{subex} 
 
\item $\ulcorner\lambda r$:\smallrecord{\smalltfield{x}{\textit{Ind}}}
  . \record{\tfield{e}{bark($r$.x)}}$\urcorner$ 
 
\item $\ulcorner\lambda
  r$:\smallrecord{\smalltfield{x}{\textit{Ind}}\\
                  \smalltfield{c}{dog(x)}}
  . \record{\tfield{e}{bark($r$.x)}}$\urcorner$  
 
\end{subex} 
   
\end{ex} 
% Note that \preveg{b} is still of type \textit{Ppty}(\textit{Ind})
% according to our definition above.


The ability to restrict properties will be important for analyzing
dynamic quantification where information from the first argument of
the quantifier relation is passed to the second argument of the
quantifier relation and this is what enables the treatment of donkey
anaphora.  Thus \textit{every farmer who owns a donkey likes it} will
be treated as the `every'-relation holding between the property of
being a farmer and owning a donkey and the property of being a farmer
who owns a donkey and likes it thus providing an antecedent for
\textit{it} within the second property (see
Section~\ref{sec:donkey-anaph}). However, it will also be important to
be able to ``purify'' such restricted properties, that is, relate them
systematically to a corresponding property whose background contains just
the one `x'-field.  This will allow us to avoid the proportion problem
that can arise in the analysis of donkey anaphora, that is in
computing whether a
sentence like \textit{most farmers who own a donkey like it} is true, we need
to ensure that the majority of farmers who own a donkey are such that
they like it and not that the majority of pairs of farmers and donkeys
where the farmer owns the donkey are such that the farmer likes the
donkey. Thus we need a property of individuals, not of farmer-donkey
pairs.  Suppose we have the restricted property \nexteg{a}.  We will
define an operation on functions which will yield the pure property
\nexteg{b}.
\begin{ex} 
\begin{subex} 
 
\item $\ulcorner\lambda r$:\smallrecord{\smalltfield{x}{\textit{Ind}}\\
                               \smalltfield{c$_1$}{farmer(x)}\\
                               \smalltfield{y}{\textit{Ind}}\\
                               \smalltfield{c$_2$}{donkey(y)}\\
                               \smalltfield{e}{own(x, y)}}
                             . \record{\tfield{e}{like($r$.x, $r$.y)}}$\urcorner$
 
\item $\ulcorner\lambda r$:\smallrecord{\smalltfield{x}{\textit{Ind}}} . \record{\tfield{$\mathfrak{c}$}{\smallrecord{\smallmfield{x}{$r$.x}{\textit{Ind}}\\
                               \smalltfield{c$_1$}{farmer(x)}\\
                               \smalltfield{y}{\textit{Ind}}\\
                               \smalltfield{c$_2$}{donkey(y)}\\
                               \smalltfield{e}{own(x, y)}}}\\
        \tfield{e}{\record{\tfield{e}{like($\Uparrow$$\mathfrak{c}$.x,
              $\Uparrow$$\mathfrak{c}$.y)}}}}$\urcorner$ 
 
\end{subex} 
\label{ex:pure-eg}   
\end{ex} 
This purification operation changes the property in \preveg{a}, a
property of farmers who own a donkey into the property \preveg{b}, a
property of individuals.  The restriction in \preveg{a} has been
lowered into the body of the property and labelled with
`$\mathfrak{c}$', intuitively a local context in the type returned by
the function.

We first define an operation which will generalize a type to the type
containing one of its non-dependent fields.  This is just one way of
many to operate on a type to make it more general.  Consider \nexteg{}.
\begin{ex}
\record{\tfield{x}{\textit{Ind}}\\
        \tfield{e}{dog(x)}}
\end{ex}
We can pick out the `x'-field which is not dependent, unlike the
`e'-field. The result is \nexteg{}
\begin{ex}
\record{\tfield{x}{\textit{Ind}}}
\end{ex}
In general for a record type,  $T$, we will represent the generalization
of $T$ to its non-dependent $\ell$-field as $T^\ell$.
\begin{shaded}
The general
definition of this is \nexteg{}, repeated in Appendix~\ref{app:gen-rectypes}.
\begin{ex}
If $T$ : \textit{RecType}, $\ell\in\text{labels}(T)$ and
$\langle\ell,T'\rangle\in T$ where $T'$: \textit{Type} (that is,
$[\ell,T']$ is a non-dependent field in $T$), then \textit{the
  generalization of $T$ to its $\ell$-field}, $T^\ell$, is
\begin{quote}
\record{\tfield{$\ell$}{$T'$}}
\end{quote}
\label{ex:gen-to-ell}
\end{ex}
\end{shaded}


We denote the purification operation on properties by $\mathfrak{P}$
and define it as in \nexteg{}.
\begin{ex} 
If $P$ : \textit{Ppty}, then
\begin{quote}
if $P$.bg$^x$ = $P$.bg, then
\begin{quote}
$\mathfrak{P}(P)=P$
\end{quote}
otherwise:
\begin{quote}
$\mathfrak{P}(P)$ is $\ulcorner\lambda r$:$P$.bg$^{\text{x}}$
. \record{\tfield{$\mathfrak{c}$}{$P.\text{bg}\parallel$ \smallrecord{\field{x}{$r$.x}}}\\
          \tfield{e}{$P(\mathfrak{c})$}}$\urcorner$
\end{quote}
\end{quote}
\label{ex:purification}
\end{ex} 
(Recall that $T\!\!\parallel\!\! r$ is the result of specifying or anchoring
$T$ with the record $r$ as defined in Appendix~\ref{app:specrec}.)

\preveg{} represents one of two options for purifying a property.  It
yields the property of being something such that the background
conditions $P$.bg are met \textit{and} the body of the property is met
under those conditions.  The alternative is to say that the property
yielded is the property of being something such that \textit{if} the
background conditions $P$.bg are met, \textit{then} the body of the
property is met under those conditions.  This alternative, which has
the effect of universal quantification over situations which meet the
background conditions, will we represented by the operator
`$\mathfrak{P}^\forall$' characterized in \nexteg{}.
\begin{ex} 
If $P$ : \textit{Ppty}, then
\begin{quote}
if $P$.bg$^x$ = $P$.bg, then
\begin{quote}
$\mathfrak{P^\forall}(P)=P$
\end{quote}
otherwise:
\begin{quote}
$\mathfrak{P^\forall}(P)$ is $\ulcorner\lambda r$:$P$.bg$^{\text{x}}$
. ($(r'\!:\!P.\text{bg}\!\parallel\!\!\text{\smallrecord{\field{x}{$r$.x}}})\rightarrow$
\record{
          \tfield{e}{$P(r')$}})$\urcorner$
\end{quote}
\end{quote}
\label{ex:purification-universal} 
\end{ex} 
The option presented by `$\mathfrak{P}^\forall$' will become relevant
in our discussion of donkey anaphora on
p.~\pageref{pg:donkey-purification-universal}. For now, we will
continue the discussion with the existential variant, `$\mathfrak{P}$'. 

As an example let us apply $\mathfrak{P}$ to (\ref{ex:pure-eg}a).  The
result will be \nexteg{}
\begin{ex} 
$\ulcorner\lambda r$:\smallrecord{\smalltfield{x}{\textit{Ind}}} . 
\record{\tfield{$\mathfrak{c}$}{\smallrecord{\smalltfield{x}{\textit{Ind}}\\
                               \smalltfield{c$_1$}{farmer(x)}\\
                               \smalltfield{y}{\textit{Ind}}\\
                               \smalltfield{c$_2$}{donkey(y)}\\
                               \smalltfield{e}{own(x, y)}} $\parallel$
                             \smallrecord{\field{x}{$r$.x}}} \\  
        \tfield{e}{$\ulcorner\lambda r$:\smallrecord{\smalltfield{x}{\textit{Ind}}\\
                               \smalltfield{c$_1$}{farmer(x)}\\
                               \smalltfield{y}{\textit{Ind}}\\
                               \smalltfield{c$_2$}{donkey(y)}\\
                               \smalltfield{e}{own(x, y)}}
                             . \record{\tfield{e}{like($r$.x, $r$.y)}}$\urcorner$($\mathfrak{c}$)}}$\urcorner$
\label{ex:pure-eg1}
\end{ex} 
% Following the definition of generalization of a type to a particular
% field in Appendix~\ref{app:gen-rectypes}, \nexteg{a} represents
% \nexteg{b}.
% \begin{ex} 
% \begin{subex} 
 
% \item \smallrecord{\smalltfield{x}{\textit{Ind}}\\
%                                \smalltfield{c$_1$}{farmer(x)}\\
%                                \smalltfield{y}{\textit{Ind}}\\
%                                \smalltfield{c$_2$}{donkey(y)}\\
%                                \smalltfield{e}{own(x, y)}}$^x$ 
 
% \item \smallrecord{\smalltfield{x}{\textit{Ind}}} 
 
% \end{subex} 
   
% \end{ex} 
According to the definition of the specification of a record type by a
record, \nexteg{a} represents
\nexteg{b}.
\begin{ex} 
\begin{subex} 
 
\item \smallrecord{\smalltfield{x}{\textit{Ind}}\\
                               \smalltfield{c$_1$}{farmer(x)}\\
                               \smalltfield{y}{\textit{Ind}}\\
                               \smalltfield{c$_2$}{donkey(y)}\\
                               \smalltfield{e}{own(x, y)}} $\parallel$
                             \smallrecord{\field{x}{$r$.x}} 
 
\item \smallrecord{\smallmfield{x}{$r$.x}{\textit{Ind}}\\
                               \smalltfield{c$_1$}{farmer(x)}\\
                               \smalltfield{y}{\textit{Ind}}\\
                               \smalltfield{c$_2$}{donkey(y)}\\
                               \smalltfield{e}{own(x, y)}}  
 
\end{subex} 
   
\end{ex} 
To understand the reduction of the type in the `e'-field in (\ref{ex:pure-eg1}) we
represent it first in the official notation for dependent fields as in
\nexteg{a}.  This represents the same as \nexteg{b} (by
$\beta$-conversion) and its abbreviatory notation in the context of
(\ref{ex:pure-eg1}) is \nexteg{c}.
\begin{ex} 
\begin{subex} 
 
\item $\langle\lambda v$:\smallrecord{\smalltfield{x}{\textit{Ind}}\\
                                      \smalltfield{c$_1$}{farmer(x)}\\
                                      \smalltfield{y}{\textit{Ind}}\\
                                      \smalltfield{c$_2$}{donkey(y)}\\
                                      \smalltfield{e}{own(x,y)}}
                                    . $\ulcorner\lambda r$:\smallrecord{\smalltfield{x}{\textit{Ind}}\\
                                      \smalltfield{c$_1$}{farmer(x)}\\
                                      \smalltfield{y}{\textit{Ind}}\\
                                      \smalltfield{c$_2$}{donkey(y)}\\
                                      \smalltfield{e}{own(x,y)}}
                                    . \record{\tfield{e}{like($r$.x,$r$.y)}}$\urcorner$($v$), $\langle\mathfrak{c}\rangle\rangle$
 
\item $\langle\lambda v$:\smallrecord{\smalltfield{x}{\textit{Ind}}\\
                                      \smalltfield{c$_1$}{farmer(x)}\\
                                      \smalltfield{y}{\textit{Ind}}\\
                                      \smalltfield{c$_2$}{donkey(y)}\\
                                      \smalltfield{e}{own(x,y)}}
                                    . 
                                    \record{\tfield{e}{like($v$.x,$v$.y)}},
                                      $\langle\mathfrak{c}\rangle\rangle$ 

\item \record{\tfield{e}{like($\Uparrow\!\mathfrak{c}$.x,$\Uparrow\!\mathfrak{c}$.y)}}
 
\end{subex} 
   
\end{ex} 
Making these substitutions yields (\ref{ex:pure-eg}b).

If $P$ is a pure property, we will use the notation $P\{a\}$ to
represent the type $P$(\smallrecord{\field{x}{$a$}}).  If $P\{a\}$ is
witnessed we say that $a$ has property $P$.  We can now define the
type of objects which have $P$, which we will represent as
$\mathfrak{T}(P)$. We introduce this type as in \nexteg{}.
\begin{ex} 
\begin{subex} 
 
\item If $P$ : \textit{Ppty} and $P$ is pure, then $\mathfrak{T}(P)$ : \textit{Type}. 
 
\item $a:\mathfrak{T}(P)$ iff $\mathfrak{P}(P)\{a\}$ is witnessed. 
 
\end{subex} 
   
\end{ex}

There is a different route to a type with the same witnesses as
$\mathfrak{T}(P)$.  We have previously defined $\downP{P}$ as the
set of objects which have the property $P$, as in
Chapter~\ref{ch:commonnouns}, p.~\pageref{pg:property-extension-rev}.  For
any set, $X$, we can define a type whose witnesses are exactly the
members of $X$.  We will represent this type as $\mathfrak{T}(X)$ and
introduce it as in \nexteg{} (repeated in Appendix~\ref{app:settypes}.
\begin{ex} 
\begin{subex} 
 
\item If $T$ is a type and $X:\mathrm{set}(T)$, then $\mathfrak{T}(X)$ is a type 
 
\item $a:\mathfrak{T}(X)$ iff $a\in X$ 
 
\end{subex} 
\label{ex:mathfrakT}   
\end{ex} 
Given this, it is straightforward to see that \nexteg{} holds.
\begin{ex} 
For any property, $P$, $a:\mathfrak{T}(P)$ iff
$a:\mathfrak{T}(\downP{P})$ 
\end{ex} 
What distinguishes these two types is the method they suggest for
determining whether something is a witness for the type.  In the case
of $\mathfrak{T}(\downP{P})$ we have to first determine the complete
set of objects which have the property and then determine whether the
object in question is a member of the set.  In the case of
$\mathfrak{T}(P)$ we only have to determine whether the object in
question has the property $P$.  Computing the set of all objects which
have a property may be viable when we are considering a property whose
extension is a small finite set of objects (for example, if the
property is that of being a dog in a particular small situation) but
it does not seem feasible in the case of large finite sets or infinite
sets.  We will return to this issue below when we consider the
interpretation of generalized quantifiers which are classically
treated by comparing sets and we will consider an alternative in terms
of types and estimated probabilities.        
     

\subsection{Types of witness sets for quantifiers}
\label{sec:witset-types}
In this section we will discuss the characterization of types of
witness sets for various generalized quantifiers as a step on our way
to characterizing a witnessed-based account of generalized
quantifiers.  The witness sets we characterize will be very close to
those of \cite{BarwiseCooper1981}, though not exactly the same in all
cases.  In general for a quantifier relation, $q$, and property,
$P$, a witness set, $X$, of type $q^w(P)$ must meet two conditions.  The
first is that it must be a subset of the property extension of $P$.
We now have two ways of expressing this as shown in \nexteg{}.
\begin{ex} 
\begin{subex} 
 
\item $X\subseteq\downP{P}$
 
\item $X:\mathrm{set}(\mathfrak{T}(P))$ 
 
\end{subex} 
   
\end{ex} 
\preveg{a} makes explicit the connection to the original definition of
witness sets by Barwise and Cooper.  \preveg{b} is an equivalent
condition on $X$ which does not involve the computation of the
complete property extension of $P$.

The second condition which must be met by witnesses, $X$, of $q^w(P)$ is a
cardinality condition on $X$.  This may be an absolute condition on
the size of $X$ or it may involve a comparison of the size of $X$ with
the size of the property extension of $P$, that is, $\downP{P}$.  Thus
even though we have a way of avoiding the computation of the total
property extension in the first condition on witness sets, we will not
always be able to avoid it in the second condition.  It is for this
reason that we will move to probability estimations in the next
section.

The witness condition for `exist$^{\text{w}}$($P$)' is given in
\nexteg{}.
\begin{ex} 
$X:\text{exist}^{\text{w}}(P)$ iff
\begin{enumerate} 
 
\item $X:\mathrm{set}(\mathfrak{T}(P))$ 
 
\item $|X|=1$ 
 
\end{enumerate} 
   
\end{ex}
Note that this differs from Barwise and Cooper in that it requires
that the witness set contain exactly one object having property $P$
rather than at least one such object.  The quantifier relation `exist'
is used in interpreting the English determiner \textit{a} and also the
singular determiner \textit{some}.  Plural \textit{some} corresponds
to the quantifier relation `exist$_{\text{pl}}$'.  The witness condition for `exist$_{\text{pl}}^{\text{w}}$($P$)' is given in
\nexteg{}.
\begin{ex} 
$X:\text{exist}_{\text{pl}}^{\text{w}}(P)$ iff
\begin{enumerate} 
 
\item $X:\mathrm{set}(\mathfrak{T}(P))$ 
 
\item $|X|\geq 2$ 
 
\end{enumerate} 
   
\end{ex}
Correspondingly we can define the witness condition for `no$^{\text{w}}$($P$)' is given in
\nexteg{}.
\begin{ex} 
$X:\text{no}^{\text{w}}(P)$ iff
\begin{enumerate} 
 
\item $X:\mathrm{set}(\mathfrak{T}(P))$ 
 
\item $|X|=0$ 
 
\end{enumerate} 
   
\end{ex}
\preveg{} could, of course, be given more concisely as \nexteg{}.
\begin{ex} 
$X:\text{no}^{\text{w}}(P)$ iff $X=\emptyset$
\end{ex}

The witness condition for `every$^{\text{w}}$($P$)' is given in
\nexteg{}.
\begin{ex} 
$X:\text{every}^{\text{w}}(P)$ iff
\begin{enumerate} 
 
\item $X:\mathrm{set}(\mathfrak{T}(P))$ 
 
\item $|X|=|\down{\mathfrak{T}(P)}|$ 
 
\end{enumerate}  
\end{ex} 
Note that \preveg{} requires $X$ to be identical with $\down{\mathfrak{T}(P)}$ and
we could, of course, express the witness condition more succinctly as
\nexteg{} if we are not concerned about demonstrating that the witness
conditions for the types witness sets for all quantifiers follow the
same pattern.
\begin{ex} 
$X:\text{every}^{\text{w}}(P)$ iff $X=\down{\mathfrak{T}(P)}$ 
\end{ex} 
Either way, we seem committed to computing the set $\downP{P}$ in
order to compute a witness set of `every' and $P$ and this can
therefore lead to problems if $\downP{P}$ is a large set.  A standard
way of avoiding the computation of this set in the interpretation of
universal quantification is to associate universal quantification with
a function so that, using the notions we have built up,  a witness for `every($P$,$Q$)' would be a function
from $\mathfrak{T}(P)$ to $\mathfrak{T}(Q)$ (see \citealp{Ranta1994},
for discussion of how this is done in a standard Martin-Löf type
theory).  This avoids computing the property extension of $P$ if we
have the right view of functions as intensional objects or procedures,
rather than the von Neumann notion of function as a set of ordered
pairs as is standard in set theory.  We will make use of such
functions when we come to treat the witness conditions for
quantificational ptypes.  Such a treatment on its own does not yield a
characterization of a witness set, however, and thus does not
immediately yield a way of treating plural discourse anaphora with
a universal quantifier as antecedent as in \nexteg{}.
\begin{ex} 
Every dog ran into the field.  They had seen the rabbits. 
\end{ex} 
For this reason we will pursue the witness set approach and attempt to
solve the problem of large sets by introducing probability estimation.  


In order to account for the witness condition for `most$^{\text{w}}$'
we assume that there is a threshold,
$\theta_{\text{most}}(P)$, which tells you what proportion of the
property extension of $P$ has to be included in the witness set.  This
is possibly an oversimplification in that the threshold may depend on
more than the quantifier relation and the first argument property
to the relation.  A common assumption in the generalized quantifier
literature is that `most($P$,$Q$)' is true just in case at least one more than
half of the $P$s are $Q$ (see, for example,
\citealp{PetersWesterstahl2006}).  This may be true if the property
extension of $P$ is a small finite set.  But it hardly seems to be the
case for an example involving a larger set as in \nexteg{}.
\begin{ex} 
Most supporters in the stadium cheered when the goal was scored. 
\end{ex} 
\preveg{} does not appear to be true if only one more than half of the
forty thousand supporters in the stadium cheered.  Rather we would expect the number
of cheering supporters to be something in excess of 75\% or 85\%  of the
supporters in the stadium.  The unclarity as to exactly which
proportion is involved leads us to introduce a threshold which can
vary with the context and the speaker.  

The witness condition for `most$^{\text{w}}$($P$)' is given in \nexteg{}. 
\begin{ex} 
$X:\text{most}^{\text{w}}(P)$ iff
\begin{enumerate} 
 
\item $X:\mathrm{set}(\mathfrak{T}(P))$ 
 
\item $\frac{|X|}{|\downP{P}|}\geq\theta_{\text{most}}(P)$ 
 
\end{enumerate}  
\end{ex}
Clause~2 in \preveg{} requires us to count both the witness set, which
may be quite large, like the number of supporters in a stadium, as
well as the property extension of $P$.  We will address this by using
probability estimations in the next section.

The English determiner \textit{many}, has two readings: absolute and
proportional.  We will treat this in terms of two quantifier relations
`many$_a$' and `many$_p$'.  For any property, $P$, we will assume that
thresholds, $\theta_{\text{many}_a}(P)$ and $\theta_{\text{many}_p}(P)$ are
provided.  These will indicate, respectively, the number of objects
having property $P$ that will count as many and the proportion of the
set of objects having $P$ that will count as many.  The witness
condition for `many$_a^{\text{w}}$($P$)' is given in \nexteg{}.
\begin{ex} 
$X:\text{many}_a^{\text{w}}(P)$ iff
\begin{enumerate} 
 
\item $X:\mathrm{set}(\mathfrak{T}(P))$ 
 
\item $|X|\geq\theta_{\text{many}_a}(P)$ 
 
\end{enumerate} 
 
\end{ex}
The witness condition for `many$_p^{\text{w}}$($P$)' is given in \nexteg{}.
\begin{ex} 
$X:\text{many}_p^{\text{w}}(P)$ iff
\begin{enumerate} 
 
\item $X:\mathrm{set}(\mathfrak{T}(P))$ 
 
\item $\frac{|X|}{|\downP{P}|}\geq\theta_{\text{many}_p}(P)$ 
 
\end{enumerate}  
\end{ex} 
The quantifier relations corresponding to \textit{few} are treated in
an exactly similar fashion to those corresponding to \textit{many}
except that the cardinality of the witness set or the proportion of
the property extension included in the witness set is required to be
less than or equal to the relevant threshold. The witness
condition for `few$_a^{\text{w}}$($P$)' is given in \nexteg{}.
\begin{ex} 
$X:\text{few}_a^{\text{w}}(P)$ iff
\begin{enumerate} 
 
\item $X:\mathrm{set}(\mathfrak{T}(P))$ 
 
\item $|X|\leq\theta_{\text{few}_a}(P)$ 
 
\end{enumerate} 
 
\end{ex}
The witness condition for `few$_p^{\text{w}}$($P$)' is given in \nexteg{}.
\begin{ex} 
$X:\text{few}_p^{\text{w}}(P)$ iff
\begin{enumerate} 
 
\item $X:\mathrm{set}(\mathfrak{T}(P))$ 
 
\item $\frac{|X|}{|\downP{P}|}\leq\theta_{\text{few}_p}(P)$ 
 
\end{enumerate}  
\end{ex}

The quantifier relations corresponding to \textit{a few} use the same
thresholds as those corresponding to \textit{few} but in the case of
\textit{a few} the size of the witness set and the proportion of the
witness set to the property extension have to be greater than or equal
to the threshold. The witness
condition for `a\_few$_a^{\text{w}}$($P$)' is given in \nexteg{}.
\begin{ex} 
$X:\text{a\_few}_a^{\text{w}}(P)$ iff
\begin{enumerate} 
 
\item $X:\mathrm{set}(\mathfrak{T}(P))$ 
 
\item $|X|\geq\theta_{\text{few}_a}(P)$ 
 
\end{enumerate} 
 
\end{ex}
The witness condition for `a\_few$_p^{\text{w}}$($P$)' is given in \nexteg{}.
\begin{ex} 
$X:\text{a\_few}_p^{\text{w}}(P)$ iff
\begin{enumerate} 
 
\item $X:\mathrm{set}(\mathfrak{T}(P))$ 
 
\item $\frac{|X|}{|\downP{P}|}\geq\theta_{\text{few}_p}(P)$ 
 
\end{enumerate}  
\end{ex} 
     

\section{Relating witness sets to probabilities}
In general our strategy for relating witness sets to probabilities
will involve two conditions, the first of which is the same as we had
in the previous section, that is that the witness set, $X$, is a set
of objects which have the property, $P$, i.e. $X:\mathrm{set}(\mathfrak{T}(P))$.
The second condition, however, will place a constraint on the value of
a conditional probability which we will represent as
$p(\mathfrak{T}(X)\|\mathfrak{T}(P))$, that its, the probability for
any object $a$ that it is of type $\mathfrak{T}(X)$ given that it is
of type $\mathfrak{T}(P)$.\footnote{We contrast this with
  $p(\mathfrak{T}(X)|\mathfrak{T}(P)$, the probability that there is
  something of type $\mathfrak{T}(X)$, given that there is something
  of type $\mathfrak{T}(P)$. See \cite{CooperDobnikLappinLarsson2014a}
  for discussion.}  Similar probabilities associated with quantifiers
have been suggested by \cite{Emerson2020}.    Here we will take a
frequentist view of this probability and define it according the
equation in \nexteg{}.
\begin{ex} 
$p(T_1\|T_2)=\frac{|\down{T_1\wedge T_2}|}{|\down{T_2}|}$ if $T_2$ is
witnessed and $0$ otherwise.
\label{ex:freq-cond-prob}
\end{ex} 
Clearly, this of itself will not help if we wish to avoid counting the
set of witnesses of $T_1$ or $T_2$. However, probabilities can be
estimated on the basis of previous experience.  We will assume that an
agent has available in memory a finite set of Austinian propositions,
$\mathfrak{J}$, recording judgements previously made.  We will define
a notion of having a type with respect to a set of Austinian
propositions, $\mathfrak{J}$, using $a:_{\mathfrak{J}}T$ to represent
``$a$ is of type $T$ with respect to $\mathfrak{J}$''.  This notion
is defined in \nexteg{}.
\begin{ex} 
\begin{subex} 
 
\item $a:_{\mathfrak{J}}T$ if \record{\field{sit}{$a$}\\
                                         \field{type}{$T$}}
                                       $\in$ $\mathfrak{J}$ 
 
\item If $T=(T_1\wedge T_2)$, then $a:_{\mathfrak{J}}T$ if $a:_{\mathfrak{J}}T_1$ and
  $a:_{\mathfrak{J}}T_2$

\item Otherwise $a\not:_{\mathfrak{J}}T$
 
\end{subex} 
   
\end{ex} 
We will use the notation $\down{T}_{\mathfrak{J}}$ to represent the
extension of $T$ with respect to $\mathfrak{J}$, defined in \nexteg{}.
\begin{ex} 
$\down{T}_{\mathfrak{J}}=\{a\mid a:_{\mathfrak{J}}T\}$ 
\end{ex} 
We can now define the notion of \textit{estimate of} $p(T_1\|T_2)$
\textit{based on} $\mathfrak{J}$, $p_{\mathfrak{J}}(T_1\|T_2)$, as in
\nexteg{}.
\begin{ex} 
$p_{\mathfrak{J}}(T_1\|T_2)=\frac{|\down{T_1\wedge T_2}_{\mathfrak{J}}|}{|\down{T_2}_{\mathfrak{J}}|}$ 
\end{ex} 
A measure of reliability of the estimate could be related to the
number of instances observed, that is, about which a judgement has
been made, for example as in \nexteg{}.
\begin{ex} 
reliability($p_{\mathfrak{J}}(T_1\|T_2)$) = ln min($|\down{T_1}_{\mathfrak{J}}|,|\down{T_2}_{\mathfrak{J}}|$) 
\end{ex} 
This could still involve an agent in a serious amount of counting
which might be unintuitive from a psychological point of view. From a
computational point of view it would be straightforward enough to keep
track of how many objects of each type have already been judged and to
increment these numbers when a new object of the type is encountered.
However, we do not seem to be aware of how many objects of a given
type we have encountered when the numbers get high.  For example, I
know that I have seen a lot of dogs in my life but I have no idea how
many.  It would also not explain how I could estimate the probability
that any person in a stadium is wearing an IFK Göteborg scarf just by
looking around the stadium but not exactly counting the number of
people in the stadium and the number of those wearing the scarf.  This
seems to point to the related proposals based on Austinian
propositions involving Bayesian reasoning about probability which are
suggested in \cite{CooperDobnikLappinLarsson2014a}.  An
important difference between what we are doing here and what we did in
the earlier work is that here we assume that the Austinian
propositions in $\mathfrak{J}$ are categorical rather than
probabilistic.  We could, of course, derive a set of categorical
propositions from a set of probabilistic propositions by choosing
categorical propositions for all those in the probabilistic set whose
probabilities exceed a given threshold.

Here we will look at the straight frequentist interpretation of
probabilities associated with types of witness sets of quantifiers as
this can be shown to relate directly to the characterization of these
types in Section~\ref{sec:witset-types} and assume that these
probabilities can be estimated on the basis of a (tractably small) set, $\mathfrak{J}$,
of propositions available to the agent in memory.   For convenience in
the discussion below we will repeat the second clause of the
non-deterministic characterization from Section~\ref{sec:witset-types}
for comparison.

The witness condition for `exist$^{\text{w}}$($P$)' is given in
\nexteg{}.
\begin{ex} 
$X:\text{exist}^{\text{w}}(P)$ iff
\begin{enumerate} 
 
\item $X:\mathrm{set}(\mathfrak{T}(P))$ 
 
\item
  $p(\mathfrak{T}(X)\|\mathfrak{T}(P))=\frac{1}{|\down{\mathfrak{T}(P)}|}$
  (corresponds to $|X|=1$) 
 
\end{enumerate} 
   
\end{ex}
It is easy to see that the clauses~(1.) and (2.) in \preveg{} are
equivalent to the non-probabilistic version if we take the frequentist
interpretation of the conditional probability in
(\ref{ex:freq-cond-prob}).  Nothing is gained by going to the extra
expense of computing the probability here.  All we need to do is check
that the witness set is a singleton and that its member is of the type
$\mathfrak{T}(P)$.  

The witness condition for `exist$_{\text{pl}}^{\text{w}}$($P$)' is given in
\nexteg{}.
\begin{ex} 
$X:\text{exist}_{\text{pl}}^{\text{w}}(P)$ iff
\begin{enumerate} 
 
\item $X:\mathrm{set}(\mathfrak{T}(P))$ 
 
\item
  $p(\mathfrak{T}(X)\|\mathfrak{T}(P))\geq\frac{2}{|\down{\mathfrak{T}(P)}|}$
  (corresponds to $|X|\geq 2$) 
 
\end{enumerate} 
   
\end{ex}
The probabilistic condition is again equivalent to the
non-probabilistic condition and there is no point in going to the
extra expense of computing the probability.

The witness condition for `no$^{\text{w}}$($P$)' is given in
\nexteg{}.
\begin{ex} 
$X:\text{no}^{\text{w}}(P)$ iff
\begin{enumerate} 
 
\item $X:\mathrm{set}(\mathfrak{T}(P))$ 
 
\item $p(\mathfrak{T}(X)\|\mathfrak{T}(P))=0$ (corresponds to $|X|=0$) 
 
\end{enumerate} 
   
\end{ex}
Again the probabilistic and non-probabilistic conditions are
equivalent and there is no point to computing the probability since
all we have to do is check that the witness set is the empty set.

The witness condition for `every$^{\text{w}}$($P$)' is given in
\nexteg{}.
\begin{ex} 
$X:\text{every}^{\text{w}}(P)$ iff
\begin{enumerate} 
 
\item $X:\mathrm{set}(\mathfrak{T}(P))$ 
 
\item $p(\mathfrak{T}(X)\|\mathfrak{T}(P))=1$ (corresponds to $|X|=|\down{\mathfrak{T}(P)}|$) 
 
\end{enumerate}  
\end{ex}



Again the probabilistic and non-probabilistic conditions are
equivalent given the frequentist interpretation of probability.
However, here there is some point to the probability for semantic
processing. Both the conditions as formulated require counting the set
of objects which have the property, $P$, which can be intractable
especially if the set is infinite or finite and reasonably large.
However, the probability can be estimated on the basis of a finite
number of observations.  The more relevant observations you have, the
more reliable your estimate.  Consider the sentence in \nexteg{}.
\begin{ex} 
Every dog barks when it is time to go for a walk 
\end{ex} 
An utterance of \preveg{} is naturally interpreted to be quantifying
over dogs in general, or at least those which are physically capable
of barking.  I have no practical way of determining the truth or
falsity of this
sentence, though I can make an estimate on the basis of my observations
of dogs in pre-walk situations.  If all relevant observations of dogs
involved the dog barking, then I can estimate that the sentence is
true.  Of course, if I have only observed
two or three dogs, my estimate is not very reliable even though it is
consistent with my experience.  If on the other hand I have observed
hundreds of situations where a dog is about to go for a walk, all of
them with the dog barking, then it seems like a more reliable estimate,
although my experience will not show conclusively that it will be
true.  How do sentences like this get used in a dialogue.  Consider
the (constructed) dialogue in \nexteg{}.
\begin{ex} 
\begin{tabular}[t]{lp{.8\textwidth}}
\multicolumn{2}{p{.9\textwidth}}{\textit{$A$ and $B$ are about to
  take $A$'s  dog
  for a walk.  The dog, realizing that a walk is in the offing, begins
  to bark excitedly.}}\\
$A:$ & I must apologize for the racket.\\
$B:$ & Not to worry. Every dog barks when it is time to go for a
       walk. \textit{$B$ is thinking of her past experience of dogs in
       similar situations.}\\
$A:$ & Yes, that's right. \textit{$A$ is thinking of
       \emph{her} past experience of dogs in similar situations.}
\end{tabular}
\label{ex:walkies}
\end{ex} 
$A$ and $B$ are agreeing on the basis of their own distinct
observations.  They both know what the sentence means but they both
also know that it is not practically possible for a human agent to
verify the truth of the sentence on the set-based view or its
equivalent frequentist probabilistic interpretation and therefore that
the basis for the assertion must be a probability estimation.  The
situation seems similar to that with predicates of personal taste on
the kind of approach taken by \cite{Cooper2015a,Cooper2017c}.
Consider the (constructed) dialogue in \nexteg{}.
\begin{ex} 
\begin{tabular}[t]{lp{.8\textwidth}}
\multicolumn{2}{p{.9\textwidth}}{\textit{$A$ and $B$ are eating lunch
  together and have just been served soup}}\\
$A:$ & \textit{(tasting the soup)}  Hhm, this soup is good.
       \textit{$A$ is basing her assertion on her taste sensations.}\\
$B:$ & \textit{(also tasting the soup)} You're right.  It
       is. \textit{$B$ is basing her assertion on \emph{her} taste
       sensations.}
\end{tabular}
\label{ex:taste}
\end{ex} 
Again $A$ and $B$ are agreeing on the basis of their own distinct
observations.  The reason here, however, does not have to do with the
impracticality of counting a large set but rather that it is not
possible to directly observe another person's taste sensation. But
there is also an important difference between (\ref{ex:walkies}) and
\preveg{}.  In (\ref{ex:walkies}) there is a fact of the matter which
is being discussed.  For example, consider the continuation of
(\ref{ex:walkies}) given in \nexteg{} where a third dialogue participant, $C$, joins the
conversation.
\begin{ex} 
\begin{tabular}[t]{lp{.8\textwidth}}
$C:$ & Actually, I used to have a dog which never barked except when
       he saw another dog or a squirrel. \\
$B:$ & OK, then, \textit{most} dogs bark when it's time for a walk /
       \#Well, \textit{I} think that every dog barks when it's time
       for a walk
\end{tabular}
\end{ex} 
This contrasts with a continuation of (\ref{ex:taste}) in a similar
vein.
\begin{ex} 
\begin{tabular}[t]{lp{.8\textwidth}}
$C:$ & No, this soup is not good.\\
$A:$ & \#OK, then the soup is sort of/mostly good / Well, \textit{I}
       think it's good. 
\end{tabular}
\end{ex} 
What the examples have in common is that the justification for the
assertions of the same ``proposition'' is different facts based on
personal experience.   Where they differ is in whether there is an
objective fact or not.

A similar discussion holds for \textit{most}. The witness condition for `most$^{\text{w}}$($P$)' is given in \nexteg{}. 
\begin{ex} 
$X:\text{most}^{\text{w}}(P)$ iff
\begin{enumerate} 
 
\item $X:\mathrm{set}(\mathfrak{T}(P))$ 
 
\item $p(\mathfrak{T}(X)\|\mathfrak{T}(P))\geq\theta_{\text{most}}(P)$ (corresponds to $\frac{|X|}{|\downP{P}|}\geq\theta_{\text{most}}(P)$) 
 
\end{enumerate}  
\end{ex}
As usual the frequentist interpretation of the conditional probability
is equivalent to the corresponding non-probabilistic.  In order to see
this note that
\nexteg{} holds.
\begin{ex} 
$\frac{|\down{\mathfrak{T}(X)\wedge\mathfrak{T}(P)}|}{|\down{\mathfrak{T}(P)}|}=\frac{|X|}{|\downP{P}|}$
\end{ex} 
\preveg{} holds because of the equalities in \nexteg{}.
\begin{ex} 
\begin{subex} 
 
\item $|\down{\mathfrak{T}(X)}|=|X|$ since $\down{\mathfrak{T}(X)}=X$ 
 
\item $\down{\mathfrak{T}(P)}=\downP{P}$

\item
  $|\down{\mathfrak{T}(X)\wedge\mathfrak{T}(P)}|=|\down{\mathfrak{T}(X)}|$
    since $\down{\mathfrak{T}(X)}\subseteq\down{\mathfrak{T}(P)}$
    (since $X:\mathrm{set}(\mathfrak{T}(P))$)
 
\end{subex} 
   
\end{ex} 
Again, to make an evaluation when large sets are involved we may need to
estimate the relevant probability on the basis of our own experience
and the kind of dialogue which we illustrated for \textit{every} might
occur.

The witness
condition for `many$_a^{\text{w}}$($P$)' is given in \nexteg{}.
\begin{ex} 
$X:\text{many}_a^{\text{w}}(P)$ iff
\begin{enumerate} 
 
\item $X:\mathrm{set}(\mathfrak{T}(P)$ 
 
\item
$p(\mathfrak{T}(X)\|\mathfrak{T}(P))\geq\frac{\theta_{\text{many}_a}(P)}{[\down{\mathfrak{T}(P)}]}$
  (corresponds to $|X|\geq\theta_{\text{many}_a}(P)$) 
 
\end{enumerate} 
\end{ex}
Again the probabilistic condition on the frequentist interpretation is equivalent to the
non-probabilistic one since both require that the cardinality of $X$ is
greater than or equal to $\theta_{\text{many}_a}(P)$.

The witness condition for `many$_p^{\text{w}}$($P$)' is given in \nexteg{}.
\begin{ex} 
$X:\text{many}_p^{\text{w}}(P)$ iff
\begin{enumerate} 
 
\item $X:\mathrm{set}(\mathfrak{T}(P))$ 
 
\item
  $p(\mathfrak{T}(X)\|\mathfrak{T}(P))\geq\theta_{\text{many}_p}(P)$ (corresponds to $\frac{|X|}{|\downP{P}|}\geq\theta_{\text{many}_p}(P)$) 
 
\end{enumerate}  
\end{ex}     
Again, the frequentist interpretation of the probabilisitic condition
is equivalent to the non-probabilistic condition and with large sets
we may need to estimate the probability rather than compute the
cardinality of the witness set.

The same holds for the quantifier relations corresponding to
\textit{few} and \textit{a few}. The witness
condition for `few$_a^{\text{w}}$($P$)' is given in \nexteg{}.
\begin{ex} 
$X:\text{few}_a^{\text{w}}(P)$ iff
\begin{enumerate} 
 
\item $X:\mathrm{set}(\mathfrak{T}(P))$ 
 
\item
  $p(\mathfrak{T}(X)\|\mathfrak{T}(P))\leq\frac{\theta_{\text{few}_a}(P)}{[\down{\mathfrak{T}(P)}]}$
  (corresponds to $|X|\leq\theta_{\text{few}_a}(P)$) 
 
\end{enumerate} 
 
\end{ex}

The witness condition for `few$_p^{\text{w}}$($P$)' is given in \nexteg{}.
\begin{ex} 
$X:\text{few}_p^{\text{w}}(P)$ iff
\begin{enumerate} 
 
\item $X:\mathrm{set}(\mathfrak{T}(P))$ 
 
\item $p(\mathfrak{T}(X)\|\mathfrak{T}(P))\leq\theta_{\text{few}_p}(P)$
  (corresponds to $\frac{|X|}{|\downP{P}|}\leq\theta_{\text{few}_p}(P)$) 
 
\end{enumerate}  
\end{ex}

The witness
condition for `a\_few$_a^{\text{w}}$($P$)' is given in \nexteg{}.
\begin{ex} 
$X:\text{a\_few}_a^{\text{w}}(P)$ iff
\begin{enumerate} 
 
\item $X:\mathrm{set}(\mathfrak{T}(P))$ 
 
\item $p(\mathfrak{T}(X)\|\mathfrak{T}(P))\geq\frac{\theta_{\text{few}_a}(P)}{[\down{\mathfrak{T}(P)}]}$
  (corresponds to $|X|\geq\theta_{\text{few}_a}(P)$) 
 
\end{enumerate} 
 
\end{ex}

The witness condition for `a\_few$_p^{\text{w}}$($P$)' is given in \nexteg{}.
\begin{ex} 
$X:\text{a\_few}_p^{\text{w}}(P)$ iff
\begin{enumerate} 
 
\item $X:\mathrm{set}(\mathfrak{T}(P))$ 
 
\item $p(\mathfrak{T}(X)\|\mathfrak{T}(P))\geq\theta_{\text{few}_p}(P)$
  (corresponds to $\frac{|X|}{|\downP{P}|}\geq\theta_{\text{few}_p}(P)$) 
 
\end{enumerate}  
\end{ex}


    

\section{Witness conditions for quantificational ptypes}

In general there are two witness conditions that can be associated
with quantificational ptypes $q(P,Q)$ where $q$ is a quantifier
relation and $P$ and $Q$ are properties.  These correspond to the two
evaluation procedures suggested by \cite{BarwiseCooper1981} in
connection with witness sets for monotone increasing and decreasing
quantifiers respectively.  The two conditions are given in
\nexteg{}.
\begin{ex} 
\begin{subex} 
 
\item $s:q(P,Q)$ iff $s$ :
  \record{\tfield{X}{$q^w(P)$}\\
          \tfield{f}{$((a:\mathfrak{T}(\text{X}))\rightarrow\mathfrak{P}(Q)\{a\})$}} 
 
\item $s:q(P,Q)$ iff $s$ :
  \record{\tfield{X}{$q^w(P)$}\\
          \tfield{f}{($(a:(\mathfrak{T}(P)\wedge\mathfrak{T}(Q)))\rightarrow$
            \record{\mfield{x}{$a$}{$\mathfrak{T}$(X)}})}} 
 
\end{subex} 
   
\end{ex} 
\preveg{a} is the condition to be associated with monotone increasing
quantifiers.  It says that $s$ is of the quantificational ptype just in
case it provides an appropriate witness set (in a field labelled `X')
and a function (in a field labelled `f') from objects, $a$, in that witness set to situations
(modelled as records) which show that $a$ has the purified property
derived from second argument of the quantificational ptype.
\preveg{b} is the condition to be associated with monotone decreasing
quantifiers.  It says that $s$ is of the quantificational ptype just
in case it provides an appropriate witness set (in a field labelled
`X') and a function from objects, $a$, which have both the property
which is the first argument  and the purified property derived from
the second argument to a situation (record) which shows that $a$ is a
member of the witness set.

For each quantifier relation, $q$, we have to say whether ptypes
constructed with $q$ have the witness condition \preveg{a} or
\preveg{b}.  We shall call these the \textit{general} witness
conditions.  Judging from the anaphoric possibilities associated with
natural language quantified expressions the witness conditions used
for some quantifier relations
are not the general witness conditions but simpler conditions (which
we will call \textit{particular} witness conditions) using an equivalent type.  That
is, if the relevant witness condition expressed in \preveg{} is $s:T$
what actually gets used is $s:T'$ where $T$ is witnessed if and only
if $T'$ is witnessed.  We shall discuss these cases as we go through
the witness conditions associated with the individual quantifier
relations. 

The general witness condition for `exist($P$,$Q$)' is given in
\nexteg{}.
\begin{ex} 
 $s:\text{exist}(P,Q)$ iff $s$ :
  \record{\tfield{X}{exist$^w(P)$}\\
          \tfield{f}{$((a:\mathfrak{T}(\text{X}))\rightarrow\mathfrak{P}(Q)\{a\})$}}
\end{ex} 
This requires that a witness for `exist($P$,$Q$)' must be a record
providing a pair of a singleton set whose member is an object which
has property $P$ and a function whose domain is this set which returns
for any $a$ a situation in which $a$ has (the purification of) the
property $Q$.  Thus if we let `dog$'$' and `bark$'$' represent the
properties indicated in \nexteg{a} and \nexteg{b} respectively then a
witness for `exist(dog$'$,bark$'$)' will according to \preveg{} be of
the type \nexteg{c}.
\begin{ex} 
\begin{subex} 
 
\item $\ulcorner\lambda r$:\smallrecord{\smalltfield{x}{\textit{Ind}}} . \record{\tfield{e}{dog($r$.x)}}$\urcorner$ 
 
\item $\ulcorner\lambda r$:\smallrecord{\smalltfield{x}{\textit{Ind}}}
  . \record{\tfield{e}{bark($r$.x)}}$\urcorner$ 

\item \record{\tfield{X}{exist$^w$(dog$'$)}\\
              \tfield{f}{$((a:\mathfrak{T}(X))\rightarrow\text{bark}'\{a\})$}}
 
\end{subex} 
   
\end{ex} 
It is trivial to show that \preveg{c} has a witness just in case
\nexteg{} has a witness.
\begin{ex} 
\record{\tfield{x}{$\mathfrak{T}$(dog$'$)}\\
        \tfield{e}{bark$'$\{x\}}} 
\end{ex} 
The argument is essentially that there is a singleton set containing a
dog all of whose members bark just in case there is a dog which barks.
We might prefer to have the particular witness condition for
`exist($P$,$Q$)' in \nexteg{}.
\begin{ex} 
$s:\text{exist}(P,Q)$ iff $s$ :
  \record{\tfield{x}{$\mathfrak{T}(P)$}\\
        \tfield{e}{$\mathfrak{P}(Q)$\{x\}}}
\label{ex:existPQ-part}
\end{ex}

Apart from its intuitive simplicity and correspondence to the
classical DRT treatment of indefinites as well as to the use of
$\Sigma$-types to interpret indefinites in type theory the particular
witness condition provides a component in the witness (in the
`x'-field) which can be
picked up on by singular anaphora in examples like \nexteg{}.
\begin{ex} 
A dog is barking. It is right outside my window 
\end{ex} 

The general witness condition for `exist$_{\text{pl}}$($P$,$Q$)' is
\nexteg{}.
\begin{ex} 
$s:\text{exist}_{\text{pl}}(P,Q)$ iff $s$ :
  \record{\tfield{X}{exist$_{\text{pl}}^w(P)$}\\
          \tfield{f}{$((a:\mathfrak{T}(\text{X}))\rightarrow\mathfrak{P}(Q)\{a\})$}} 
\end{ex} 
This corresponds to a distributive reading of plural \textit{some}.
It says intuitively that a situation, $s$, is of type
`exist$_{\text{pl}}$($P$,$Q$) just in case $s$ provides a set of
objects which have property $P$
with at least two members and a function which shows that each member
of 
the set has property $Q$.  In this case the witness set provides us
with a suitable antecedent for plural anaphora as in \nexteg{} and we
do not need a particular witness condition.
\begin{ex} 
Some dogs are barking.  They are right outside my window. 
\end{ex} 

The general witness condition for `no($P$,$Q$)' is given in \nexteg{}.
\begin{ex} 
$s:\text{no}(P,Q)$ iff $s$ :
  \record{\tfield{X}{$\text{no}^w(P)$}\\
          \tfield{f}{($(a:(\mathfrak{T}(P)\wedge\mathfrak{T}(Q)))\rightarrow$
            \record{\mfield{x}{$a$}{$\mathfrak{T}$(X)}})}}  
\end{ex} 
The only witness set allowed (that is,  the only set of type
$\text{no}^w(P)$, no matter what $P$ is) is the empty set.  Suppose
that we find some object, $a$, which has both properties $P$ and $Q$,
then the function will return a situation (record) that shows that $a$
is in the empty set.  There is, however, no such situation.  The only
way that there can be a function of this type is if the set of objects
which have both $P$ and $Q$ is also the empty set.  While this is
technically correct and fits the general pattern for monotone
decreasing quantifiers it does not seem to be an intuitive account of
how we would check that `no($P$,$Q$)' is witnessed.  More intuitive is
to check each object that has property $P$ and find that it does not
have property $Q$.  This method is equivalent to the first and the
relationship between the two corresponds to the equivalence between
\nexteg{a} and \nexteg{b} in first order logic.
\begin{ex} 
\begin{subex} 
 
\item $\neg\exists x[P(x)\wedge Q(x)]$ 
 
\item $\forall x [P(x)\rightarrow\neg Q(x)]$ 
 
\end{subex} 
   
\end{ex} 
In order to do this we will use the notion of negation given  in
\cite{CooperGinzburg2011,CooperGinzburg2012}.  % [We should probably
% introduce negation somewhere else independently! ????]
First we say that two
types, $T_1$ and $T_2$ \textit{preclude each other}, $T_1\bot T_2$, just in case there is no
possibility in which $\down{T_1}$ and $\down{T_2}$ overlap.  That is,
nothing can be of both types.  We then introduce negated types as in
\nexteg{}.
\begin{ex} 
\begin{subex} 
 
\item if $T$ is a type, then $\neg T$ is a type 
 
\item $a:\neg T$ iff for some type, $T'$, such that $T\bot T'$, $a:T'$ 
 
\end{subex} 
   
\end{ex}   
We will define the particular witness condition for `no($P$,$Q$)' as
\nexteg{}.
\begin{ex} 
$s:\text{no}(P,Q)$ iff $s$ :
  \record{\tfield{X}{$\text{every}^w(P)$}\\
          \tfield{f}{$((x:\mathfrak{T}(X))\rightarrow\neg\mathfrak{P}(Q)\{x\})$}} 
\label{ex:noPQ-part}
\end{ex} 
Some evidence that English uses the particular witness condition
rather than the general one comes from the fact that we can have
plural discourse anaphora related to a noun phrase with \textit{no} as
its determiner, as in \nexteg{}.
\begin{ex} 
No dog barked.  They were all busy gnawing on a bone. 
\end{ex} 
Clearly, \textit{they} does not refer to the witness set of type
`no$^w$(dog$'$)', which would have to be the empty set, but rather to
a witness set of type `every$^w$(dog$'$)', the set of all dogs.  This
is an instance of \textit{complement set anaphora}, first discussed in
the psychology literature by
\cite{MoxeySanford1987,SanfordMoxey1993} and discussed in the
semantics literature by
\cite{Kibble1997,Nouwen2003,LueckingGinzburg2019} among others.

The general witness condition for `every($P$,$Q$)' is given in
\nexteg{}.
\begin{ex} 
$s:\text{every}(P,Q)$ iff $s$ :
  \record{\tfield{X}{$\text{every}^w(P)$}\\
          \tfield{f}{$((a:\mathfrak{T}(\text{X}))\rightarrow\mathfrak{P}(Q)\{a\})$}} 
\end{ex} 
In this case we do not need a particular witness condition.  \preveg{}
correctly predicts the availability of plural discourse anaphora as in
\nexteg{}.
\begin{ex} 
Every dog barked.  They had been disturbed by the intruder. 
\end{ex} 

The same holds for \textit{most}.  The general witness condition for `most($P$,$Q$)' is given in
\nexteg{}.
\begin{ex} 
$s:\text{most}(P,Q)$ iff $s$ :
  \record{\tfield{X}{$\text{most}^w(P)$}\\
          \tfield{f}{$((a:\mathfrak{T}(\text{X}))\rightarrow\mathfrak{P}(Q)\{a\})$}} 
\label{ex:mostPQ-witcond}
\end{ex} 
In this case we do not need a particular witness condition.  \preveg{}
correctly predicts the availability of plural discourse anaphora as in
\nexteg{}.
\begin{ex} 
Most dogs bark when somebody unknown comes into their territory.  They
are disturbed by an intruder.
\end{ex}       
Note that the occurrence of \textit{they} here can be interpreted to refer not to all dogs
or dogs in general but to the witness set of dogs containing most
dogs. (This is what Moxey and Sanford call REFSET anaphora.) It can, however, also be interpreted to refer to dogs in
general, that is, all dogs are disturbed by an intruder but not all of
them bark when this happens.  This is referred to as MAXSET anaphora
by Moxey and Sanford.  This could be taken as motivation for having a
field which introduces the property `dog' in the sign corresponding to
\textit{most dogs} in the manner suggested in
Chapter~\ref{ch:gram}. Alternatively, it might be considered as
motivation for an additional field corresponding to $P$ in the witness
for `most($P$,$Q$)'.  We will leave this issue unresolved.   It seems clear, though, as has been pointed out in the
literature \citep{Nouwen2003}, that COMPSET anaphora is not possible with
\textit{most}.  That is, \textit{they} in \nexteg{} cannot refer to
dogs which do not bark when somebody unknown comes into their
territory.
\begin{ex} 
\#Most dogs bark when somebody unknown comes into their territory.  They
never feel threatened whatever happens. 
\end{ex} 
The lack of this reading is consistent with the witness condition in
(\ref{ex:mostPQ-witcond}).

Similar remarks can be made for \textit{many}.  The general witness condition for `many$_a$($P$,$Q$)' is given in
\nexteg{}.
\begin{ex} 
$s:\text{many}_a(P,Q)$ iff $s$ :
  \record{\tfield{X}{$\text{many}_a^w(P)$}\\
          \tfield{f}{$((a:\mathfrak{T}(\text{X}))\rightarrow\mathfrak{P}(Q)\{a\})$}} 
\label{ex:mostPQ-witcond}
\end{ex}   
The general witness condition for `many$_p$($P$,$Q$)' is given in
\nexteg{}.
\begin{ex} 
$s:\text{many}_p(P,Q)$ iff $s$ :
  \record{\tfield{X}{$\text{many}_p^w(P)$}\\
          \tfield{f}{$((a:\mathfrak{T}(\text{X}))\rightarrow\mathfrak{P}(Q)\{a\})$}} 
\label{ex:mostPQ-witcond}
\end{ex}   
For both absolute and proportional readings of \textit{many} REFSET
and MAXSET anaphora are available but not COMPSET.  There is no
motivation for a particular witness condition.

The general witness condition for `few$_a$($P$,$Q$)' is given in
\nexteg{}. 
\begin{ex} 
 $s:\text{few}_a(P,Q)$ iff $s$ :
  \record{\tfield{X}{$\text{few}_a^w(P)$}\\
          \tfield{f}{($(a:(\mathfrak{T}(P)\wedge\mathfrak{T}(Q)))\rightarrow$
            \record{\mfield{x}{$a$}{$\mathfrak{T}$(X)}})}}
\end{ex} 
The general witness condition for `few$_p$($P$,$Q$)'  is exactly
similar as given in \nexteg{}.
\begin{ex} 
 $s:\text{few}_p(P,Q)$ iff $s$ :
  \record{\tfield{X}{$\text{few}_p^w(P)$}\\
          \tfield{f}{($(a:(\mathfrak{T}(P)\wedge\mathfrak{T}(Q)))\rightarrow$
            \record{\mfield{x}{$a$}{$\mathfrak{T}$(X)}})}}
\end{ex}  
% As with \textit{no} we can formulate particular witness conditions
% using the dual of \textit{few}, that is, \textit{many} and type
% negation.  This corresponds to our intuition that few $P$ have
% property $Q$ is equivalent to saying that many $P$ do not have
% property $Q$.  
These witness conditions involve computing first the set of all
objects that have both property $P$ and $Q$ and then checking that all
the members of the set are in the witness set.  A more intuitive and
less computationally expensive way of achieving an equivalent result
is to find a sufficient number of objects that have property $P$ but
which don't have property $Q$ (in our terms they have a property which
precludes them having $Q$).  What counts as a sufficient  number of
objects?  It has to be a number of objects with property $P$ such that
only few objects having property $P$ remain, that is, it has to be a
set with cardinality at least the cardinality of the set whose members
have $P$ minus the threshold, $\theta_{\text{few}}$ in the case of an
absolute quantifier.  In the case of a proportional quantifier the
proportion of objects having $P$ but not $Q$ has to be greater than
one minus the proportional threshold.  We treat this by introducing
types of complement witness sets for \textit{few}.  The absolute case
is given in \nexteg{}.
\begin{ex} 
\begin{subex} 
 
\item If few$_a^w$($P$) is a type, then $\overline{\text{few}_a^w(P)}$ is a type 
 
\item $X:\overline{\text{few}_a^w(P)}$ iff
\begin{enumerate} 
 
\item $X:\mathrm{set}(\mathfrak{T}(P))$ 
 
\item $|X|\geq|\down{\mathfrak{T}(P)}|-\theta_{\text{few}_a}(P)$ 
 
\end{enumerate} 
   
 
\end{subex} 
   
\end{ex}
The proportional case is given in \nexteg{}.
\begin{ex} 
\begin{subex} 
 
\item If few$_p^w$($P$) is a type, then $\overline{\text{few}_p^w(P)}$ is a type 
 
\item $X:\overline{\text{few}_p^w(P)}$ iff
\begin{enumerate} 
 
\item $X:\mathrm{set}(\mathfrak{T}(P))$ 
 
\item $\frac{|X|}{|\down{\mathfrak{T}(P)}|}\geq 1-\theta_{\text{few}_p}(P)$ 
 
\end{enumerate} 
   
 
\end{subex} 
   
\end{ex} 
Clearly, computing whether a set is a witness for one of these new
types can involve computing the cardinality of the set of objects
which have property $P$ and for this reason is may be more tractable
to estimate a probability.  The relevant probabilities here are
similar to those associated with \textit{many}.  The witness condition
for $\overline{\text{few}_a^w(P)}$ is given in \nexteg{}.
\begin{ex} 
$X:\overline{\text{few}_a^w(P)}$ iff
\begin{enumerate} 
 
\item $X:\mathrm{set}(\mathfrak{T}(P))$ 
 
\item
$p(\mathfrak{T}(X)\|\mathfrak{T}(P))\geq\frac{\theta_{\text{few}_a}(P)}{[\down{\mathfrak{T}(P)}]}$
   
 
\end{enumerate} 
\end{ex}
The witness condition for $\overline{\text{few}_p^w(P)}$ is given in
\nexteg{}.
\begin{ex} 
$X:\overline{\text{few}_p^w(P)}$ iff
\begin{enumerate} 
 
\item $X:\mathrm{set}(\mathfrak{T}(P))$ 
 
\item
  $p(\mathfrak{T}(X)\|\mathfrak{T}(P)\geq1-\theta_{\text{few}_p}(P)$  
 
\end{enumerate}  
\end{ex} 
   
Now we can give particular witness conditions for ptypes constructed with the
quantifier predicates `few$_a$' and `few$_p$'.  The witness condition
for `few$_a$($P$,$Q$)' is given in \nexteg{}.
\begin{ex} 
$s:\text{few}_a(P,Q)$ iff $s$ :
  \record{\tfield{X}{$\overline{\text{few}_a^w(P)}$}\\
          \tfield{f}{$((x:\mathfrak{T}(X))\rightarrow\neg\mathfrak{P}(Q)\{x\})$}} 
\label{ex:fewaPQwitcond-part} 
\end{ex} 
The witness condition
for `few$_p$($P$,$Q$)' is given in \nexteg{}.
\begin{ex} 
$s:\text{few}_p(P,Q)$ iff $s$ :
  \record{\tfield{X}{$\overline{\text{few}_p^w(P)}$}\\
          \tfield{f}{$((x:\mathfrak{T}(X))\rightarrow\neg\mathfrak{P}(Q)\{x\})$}} 
\label{ex:fewpPQwitcond-part} 
\end{ex}

Why do we use complement witness set types for \textit{few} in the
particular witness conditions rather than witness sets related to
\textit{many}?  We might naively have thought that \textit{few dogs
  barked} was equivalent to \textit{many dogs did not bark}.  A
standard analysis of \textit{few} in the literature is as \textit{not
  many}, that is \textit{few dogs barked} is equivalent to \textit{not
  many dogs barked} or \textit{it is not true that many dogs barked}.
On the kind of analysis that we are proposing here neither of these
will work. We illustrate this with an example.  Suppose that we have a
dog hotel with twenty-five dogs in residence.  Suppose that what
counts as many dogs in the context is ten and what counts as few is
five.  This means that few dogs barked means that five or less dogs
barked.  If this is true then it follows that many dogs did not bark
(fifteen or more, and we only need ten to count as many) and it also
follows that it is not the case that many dogs barked (since at most
five did and for many dogs to bark we would need ten).  Thus
\textit{few} seems to imply both \textit{many not} and \textit{not
  many}.  However, the implications do not go back the other way.
Suppose that many dogs did not bark.  This means that ten or more dogs
did not bark.  If ten dogs did not bark then fifteen did bark.  Thus
many dogs barked at the same time as many dogs did not bark.  It does
not follow that few dogs barked.  Suppose that it is not the case that
many dogs barked.  This means that less than ten dogs barked.  For
example, nine dogs barked.  While nine is not many in this context
neither is it few.  We might say \textit{quite a lot} or \textit{quite
  a few}.  That is, our analysis allows for a gap between what counts
as many and what counts as few and thus \textit{not many} is not
equivalent to \textit{few}.
 
Adopting the particular witness condition predicts the existence of
COMPSET anaphora as in \nexteg{}.
\begin{ex} 
Few dogs in the kennels barked.  They didn't hear the intruder. 
\end{ex} 
However, there are convincing examples in the literature that
\textit{few} will also allow REFSET anaphora, which would be predicted
by the general witness condition.  \cite{Nouwen2003} quotes \nexteg{}
from \cite{Evans1980}.
\begin{ex} 
Few congressmen admire Kennedy, and they are very junior. 
\end{ex} 
One way to handle this is to allow both the general and particular
witness conditions as alternatives. Another solution to consider is
letting the general witness condition be used for absolute
\textit{few} and the particular witness condition for proportional
\textit{few}.  This would perhaps be consistent with Kibble's
(\citeyear{Kibble1997}) observation that complement anaphora seems to be
associated with monotone decreasing proportional quantifiers.

The general witness condition for `a\_few$_a$($P$,$Q$)' is given in
\nexteg{}.
\begin{ex} 
$s:\text{a\_few}_a(P,Q)$ iff $s$ :
  \record{\tfield{X}{$\text{a\_few}_a^w(P)$}\\
          \tfield{f}{$((a:\mathfrak{T}(\text{X}))\rightarrow\mathfrak{P}(Q)\{a\})$}} 
\end{ex} 
The general witness condition for `a\_few$_p$($P$,$Q$)' is given in
\nexteg{}.
\begin{ex} 
$s:\text{a\_few}_p(P,Q)$ iff $s$ :
  \record{\tfield{X}{$\text{a\_few}_p^w(P)$}\\
          \tfield{f}{$((a:\mathfrak{T}(\text{X}))\rightarrow\mathfrak{P}(Q)\{a\})$}} 
\end{ex} 
These will correctly predict the availability of REFSET anaphora as in
\nexteg{}.
\begin{ex} 
A few dogs barked.  They had heard the intruder. 
\end{ex} 
If these are the only witness conditions then this will correctly
predict the unavailability of COMPSET anaphora as shown by \nexteg{},
where \textit{they} cannot refer to the dogs that did not bark.
\begin{ex} 
\#A few dogs barked.  They hadn't heard the intruder 
\end{ex} 
     
            

\subsection{Some examples}

In this section we show how these definitions could be
used to express content for English utterances, ignoring for the
moment the parametric properties using in Chapter~\ref{ch:commonnouns}
and expressing the content of a quantified declarative sentence as a
quantificational ptype rather than a record type containing a
quantificational ptype as in Chapter~\ref{ch:gram} and subsequent
chapters.


\paragraph{\textit{A dog barks}}
The content of the indefinite article, \textit{a(n)}, is given in
\nexteg{}. This is `SemIndefArt'
\begin{ex} 
% $\lambda Q$:\textit{Ppty} . $\lambda P$:\textit{Ppty}
% . exist($Q$,$P|_{\mathcal{F}(Q)}$)
$\lambda Q$:\textit{Ppty} . \\
  \hspace*{1em}$\ulcorner\lambda c$:\textit{Cntxt} . \\
  \hspace*{2em}$\lambda P$:\textit{Ppty} . \\
  \hspace*{3em}\record{
    \mfield{restr}{$Q$}{\textit{Ppty}}\\
    \mfield{scope}{$P\mid_{\mathfrak{F}(\text{restr})}$}{\textit{Ppty}}\\
    \tfield{e}{exist(restr, scope)}}$\urcorner$  

\end{ex} 
The content of \textit{a dog} would then be as in \nexteg{}.
\begin{ex} 
%$\lambda
%P$:\textit{Ppty}. exist(dog$'$,$P|_{\mathcal{F}(\text{dog}')}$)
  $\ulcorner\lambda c$:\smallrecord{
    \footnotesize{\textit{Cntxt}}\\
    \smalltfield{$\mathfrak{c}$}{\smallrecord{
        \smalltfield{f}{\textit{PropCntxt}}\\
        \smalltfield{a}{\textit{PropCntxt}}}}} . \\
  \hspace*{1em}$\lambda P$:\textit{Ppty} . \\
  \hspace*{2em}\record{
    \mfield{restr}{dog$'$}{\textit{Ppty}}\\
    \mfield{scope}{$P\mid_{\mathfrak{F}(\text{dog}')}$}{\textit{Ppty}}\\
    \tfield{e}{exist(restr, scope)}}$\urcorner$  
\end{ex} 
Finally, the content of \textit{a dog barks} would be as in \nexteg{}.
\begin{ex} 
  % exist(dog$'$,bark$'|_{\mathcal{F}(\text{dog}')}$)
  $\ulcorner\lambda c$:\smallrecord{
    \footnotesize{\textit{Cntxt}}\\
    \smalltfield{$\mathfrak{c}$}{\smallrecord{
        \smalltfield{f}{\textit{PropCntxt}}\\
        \smalltfield{a}{\smallrecord{
            \smalltfield{f}{\textit{PropCntxt}}\\
            \smalltfield{a}{\textit{PropCntxt}}}}}}}. \\
  \hspace*{1em}\record{
    \mfield{restr}{dog$'$}{\textit{Ppty}}\\
    \mfield{scope}{bark$'\mid_{\mathfrak{F}(\text{dog}')}$}{\textit{Ppty}}\\
    \tfield{e}{exist(restr, scope)}}$\urcorner$
\label{ex:cont-a-dog-barks}
\end{ex} 
Following the particular witness condition for `exist($P$,$Q$)' in
(\ref{ex:existPQ-part}) we can infer \nexteg{}.
\begin{ex} 
$s$ : exist(dog$'$,bark$'|_{\mathcal{F}(dog')}$) iff
\begin{quote}
$s$ : \record{\tfield{x}{$\mathfrak{T}$(dog$'$)}\\
              \tfield{e}{$\mathfrak{P}$(bark$'|_{\mathcal{F}(\text{dog}')}$)\{x\}}}
\end{quote}
\label{ex:adb-witcond} 
\end{ex} 
$\mathcal{F}$(dog$'$) is given in \nexteg{}.
\begin{ex} 
\record{\tfield{x}{\textit{Ind}}\\
        \tfield{e}{dog(x)}} 
\end{ex} 
`bark$'|_{\mathcal{F}(\text{dog}')}$' is thus \nexteg{}.
\begin{ex} 
$\lambda r$:\smallrecord{\smalltfield{x}{\textit{Ind}}\\
                         \smalltfield{e}{dog(x)}} . \record{\tfield{e}{bark($r$.x)}} 
\end{ex} 
This means that `$\mathfrak{P}$(bark$'|_{\mathcal{F}(\text{dog}')}$)'
is \nexteg{}.
\begin{ex} 
$\lambda r$:\smallrecord{\smalltfield{x}{\textit{Ind}}} . 
\record{\tfield{$\mathfrak{c}$}{\record{\mfield{x}{$r$.x}{\textit{Ind}}\\
                                        \tfield{e}{dog(x)}}}\\
        \tfield{e}{bark($\mathfrak{c}$.x)}} 
\label{ex:Pdog_Fbark}
\end{ex} 
This means we can restate (\ref{ex:adb-witcond}) as \nexteg{}.
\begin{ex} 
$s$ : exist(dog$'$,bark$'|_{\mathcal{F}(dog')}$) iff
\begin{quote}
$s$ : \record{\tfield{x}{$\mathfrak{T}$(dog$'$)}\\
              \tfield{e}{\record{\tfield{$\mathfrak{c}$}{\record{\mfield{x}{$\Uparrow^2$x}{\textit{Ind}}\\
                                        \tfield{e}{dog(x)}}}\\
                                    \tfield{e}{bark($\mathfrak{c}$.x)}} }}
\label{ex:witcond-exist-dog-bark}
\end{quote}
\label{ex:adb-witcond-spelledout} 
\end{ex} 
Note that the record type on the right hand side of \preveg{} is
truth-conditionally equivalent to the simpler record types in
\nexteg{}, that is, for any pair of the types there is a witness for one of the types just in
case there is a witness for the other type.
\begin{ex}
\begin{subex} 
\item \record{\tfield{x}{$\mathfrak{T}$(dog$'$)}\\
        \tfield{e}{bark(x)}} 
\item \record{\tfield{x}{\textit{Ind}}\\
              \tfield{c}{dog(x)}\\
              \tfield{e}{bark(x)}}
\end{subex}
\end{ex} 
The additional structure in (\ref{ex:adb-witcond-spelledout}) is
unnecessary for this example but it will help us when we come to
donkey anaphora.

% We have ignored the additional structure associated with quantifiers
% in Chapter~\ref{ch:gram} and the introduction of context dependence
% using parametric properties and contents as discussed in
% Chapter~\ref{ch:commonnouns} for the sake of readability but this
% additional structure can be added.  For example, the content of the indefinite
% article  could be \nexteg{}, following Chapter~\ref{ch:commonnouns}.
% \begin{ex} 
% $\lambda Q$:\textit{PPpty} . $\ulcorner\lambda
% r$:\smallrecord{\smalltfield{f}{\textit{Rec}}\\
%                 \smalltfield{a}{$Q$.bg}} . $\lambda P$:\textit{Ppty}
%               . \record{\mfield{restr}{$Q$.fg($r$.a)}{\textit{Ppty}}\\
%                         \mfield{scope}{$P|_{\mathfrak{F}(Q)}$}{\textit{Ppty}}\\
%                         \tfield{e}{exist(restr,scope)}}$\urcorner$
% \end{ex} 
% [???? This might change after we have reconsidered the presentation of
% quantifiers in Ch. 5 in the light of this section.]

The witness condition in (\ref{ex:witcond-exist-dog-bark}) means that
anything of the type resulting from applying
(\ref{ex:cont-a-dog-barks}) to a context will also be of the type
\nexteg{}.
\begin{ex} 
\record{
    \mfield{restr}{dog$'$}{\textit{Ppty}}\\
    \mfield{scope}{bark$'\mid_{\mathfrak{F}(\text{dog}')}$}{\textit{Ppty}}\\
    \tfield{e}{\record{\tfield{x}{$\mathfrak{T}$(dog$'$)}\\
              \tfield{e}{\record{\tfield{$\mathfrak{c}$}{\record{\mfield{x}{$\Uparrow^2$x}{\textit{Ind}}\\
                                        \tfield{e}{dog(x)}}}\\
                                    \tfield{e}{bark($\mathfrak{c}$.x)}} }}}} 
\end{ex} 
  

Assuming a theory of anaphora where anaphoric references must relate
to paths in a witness, $s$, for the content,  we could potentially have all of the
examples of anaphora in \nexteg{}.
\begin{ex} 
\begin{subex} 
 
\item A dog barked.  They (dogs in general, $s$.restr, MAXSET) do when they notice an
  intruder.

\item A dog barked.  They (dogs in general which bark, $s$.scope) make such
  a racket.

  
\item A dog barked.  That (an event of a dog barking, $s$.e, event
  anaphora) frightened off an intruder.

\item A dog barked.  It (the dog which barked, $s$.e.x, individual,
   REFSET, anaphora) heard an intruder. 
 
\end{subex} 
   
\end{ex} 
% Of these, \preveg{b} seems very doubtful as a reasonable case of
% anaphora.  However, if we make the pronominal reference generic as
% might be appropriate if we are deriving the anaphoric interpretation
% from a property then the anaphora seems more plausible.
% \begin{ex} 
% A dog barked.  They (dogs in general which barked) frightened me when
% I was a child, but now I remained calm. 
% \end{ex}


\paragraph{\textit{No dog barks}} The content for
\textit{no dog barks} would be derived in an exactly similar way as
that for \textit{a dog barks}.  We obtain \nexteg{}.
\begin{ex} 
  % no(dog$'$,bark$'|_{\mathcal{F}(\text{dog}')}$)
  $\ulcorner\lambda c$:\smallrecord{
    \footnotesize{\textit{Cntxt}}\\
    \smalltfield{$\mathfrak{c}$}{\smallrecord{
        \smalltfield{f}{\textit{PropCntxt}}\\
        \smalltfield{a}{\smallrecord{
            \smalltfield{f}{\textit{PropCntxt}}\\
            \smalltfield{a}{\textit{PropCntxt}}}}}}}. \\
  \hspace*{1em}\record{
    \mfield{restr}{dog$'$}{\textit{Ppty}}\\
    \mfield{scope}{bark$'\mid_{\mathfrak{F}(\text{dog}')}$}{\textit{Ppty}}\\
    \tfield{e}{no(restr, scope)}}$\urcorner$
  \label{ex:cont-no-dog-barks}
\end{ex} 
Following the particular witness condition in (\ref{ex:noPQ-part}), we
can infer \nexteg{}.
\begin{ex} 
$s$ : no(dog$'$,bark$'|_{\mathcal{F}(\text{dog}')}$) iff
\begin{quote}
$s$ :
  \record{\tfield{X}{$\text{every}^w(\text{dog}')$}\\
          \tfield{f}{$((x:\mathfrak{T}(X))\rightarrow\neg
            \mathfrak{P}(\text{bark}'|_{\mathfrak{F}(\text{dog}')})\{x\})$}}
\end{quote} 
\end{ex}
Given that $\mathfrak{P}(\text{bark}'|_{\mathfrak{F}(\text{dog}')})$
is (\ref{ex:Pdog_Fbark}) we can restate \preveg{} as \nexteg{}.
\begin{ex}
$s$ : no(dog$'$,bark$'|_{\mathcal{F}(\text{dog}')}$) iff
\begin{quote} 
$s$ :
  \record{\tfield{X}{$\text{every}^w(\text{dog}')$}\\
          \tfield{f}{$((x:\mathfrak{T}(X))\rightarrow\neg$
           \record{\tfield{$\mathfrak{c}$}{\record{\mfield{x}{$\Uparrow^2$x}{\textit{Ind}}\\
                                        \tfield{e}{dog(x)}}}\\
        \tfield{e}{bark($\mathfrak{c}$.x)}} $)$}} 
\end{quote}
\end{ex}

Anything of the type resulting from applying
(\ref{ex:cont-no-dog-barks}) to a context will also be of the type
\nexteg{}.
\begin{ex} 
 \record{
    \mfield{restr}{dog$'$}{\textit{Ppty}}\\
    \mfield{scope}{bark$'\mid_{\mathfrak{F}(\text{dog}')}$}{\textit{Ppty}}\\
    \tfield{e}{\record{\tfield{X}{$\text{every}^w(\text{dog}')$}\\
          \tfield{f}{$((x:\mathfrak{T}(X))\rightarrow\neg$
           \record{\tfield{$\mathfrak{c}$}{\record{\mfield{x}{$\Uparrow^2$x}{\textit{Ind}}\\
                                        \tfield{e}{dog(x)}}}\\
        \tfield{e}{bark($\mathfrak{c}$.x)}} $)$}}}}
\end{ex} 
This suggests that we could potentially have the anaphora in
\nexteg{}.
\begin{ex} 
\begin{subex} 
 
\item No dog barked.  They (dogs in general, $s$.restr, MAXSET)
  normally do when they notice an
  intruder.

\item No dog barked.  They (dogs in general which bark, $s$.scope)
  normally make such
  a racket.

  
\item No dog barked.  That (an event of no dog barking, $s$.e, event
  anaphora) made it easy for the intruder.

\item No dog barked.  They (the dogs which didn't bark, $s$.e.X, 
   COMPSET anaphora) did not hear the intruder. 
 
\end{subex} 
   
\end{ex} 
% That no dog barks just in case every dog is such that it is not a dog
% that barks.  This can be made to take account of the additional
% structure used in Chapter~\ref{ch:commonnouns} in the same way that we
% did for \textit{a dog barks}.

\paragraph{few dogs bark}  The content for an utterance of
\textit{few dogs bark} is either \nexteg{a} or \nexteg{b}.
\begin{ex} 
\begin{subex} 
 
\item % few$_a$(dog$'$,bark$'|_{\mathcal{F}(\text{dog}')}$)
  $\ulcorner\lambda c$:\smallrecord{
    \footnotesize{\textit{Cntxt}}\\
    \smalltfield{$\mathfrak{c}$}{\smallrecord{
        \smalltfield{f}{\textit{PropCntxt}}\\
        \smalltfield{a}{\smallrecord{
            \smalltfield{f}{\textit{PropCntxt}}\\
            \smalltfield{a}{\textit{PropCntxt}}}}}}} . \\
  \hspace*{1em}\record{
    \mfield{restr}{dog$'$}{\textit{Ppty}}\\
    \mfield{scope}{bark$'\mid_{\mathfrak{F}(\text{dog}')}$}{\textit{Ppty}}\\
    \tfield{e}{few$_a$(restr, scope)}}$\urcorner$
 
\item % few$_p$(dog$'$,bark$'|_{\mathcal{F}(\text{dog}')}$)
  $\ulcorner\lambda c$:\smallrecord{
    \footnotesize{\textit{Cntxt}}\\
    \smalltfield{$\mathfrak{c}$}{\smallrecord{
        \smalltfield{f}{\textit{PropCntxt}}\\
        \smalltfield{a}{\smallrecord{
            \smalltfield{f}{\textit{PropCntxt}}\\
            \smalltfield{a}{\textit{PropCntxt}}}}}}} . \\
  \hspace*{1em}\record{
    \mfield{restr}{dog$'$}{\textit{Ppty}}\\
    \mfield{scope}{bark$'\mid_{\mathfrak{F}(\text{dog}')}$}{\textit{Ppty}}\\
    \tfield{e}{few$_p$(restr, scope)}}$\urcorner$
 
\end{subex} 
\label{ex:cont-few-dogs-bark}    
\end{ex} 
Following the particular witness conditions in
(\ref{ex:fewaPQwitcond-part}) and \ref{ex:fewpPQwitcond-part}, we
obtain \nexteg{a} and \nexteg{b} respectively.
\begin{ex} 
\begin{subex} 
 
\item
  $s:\text{few}_a(\text{dog}',\text{bark}'|_{\mathcal{F}(\text{dog}')})$
  iff 
\begin{quote}
$s$ :
  \record{\tfield{X}{$\overline{\text{few}_a^w(\text{dog}')}$}\\
          \tfield{f}{$((x:\mathfrak{T}(X))\rightarrow\neg\mathfrak{P}(\text{bark}'|_{\mathcal{F}(\text{dog}')})\{x\})$}} 
\end{quote}
 
\item
  $s:\text{few}_p(\text{dog}',\text{bark}'|_{\mathcal{F}(\text{dog}')})$
  iff 
\begin{quote}
$s$ :
  \record{\tfield{X}{$\overline{\text{few}_p^w(\text{dog}')}$}\\
          \tfield{f}{$((x:\mathfrak{T}(X))\rightarrow\neg\mathfrak{P}(\text{bark}'|_{\mathcal{F}(\text{dog}')})\{x\})$}} 
\end{quote}
 
\end{subex} 
   
\end{ex} 
As with our treatment of \textit{no} these can be unpacked as
\nexteg{}.
\begin{ex} 
\begin{subex} 
 
\item
  $s:\text{few}_a(\text{dog}',\text{bark}'|_{\mathcal{F}(\text{dog}')})$
  iff 
\begin{quote}
$s$ :
  \record{\tfield{X}{$\overline{\text{few}_a^w(\text{dog}')}$}\\
          \tfield{f}{$((x:\mathfrak{T}(X))\rightarrow\neg$\record{\tfield{$\mathfrak{c}$}{\record{\mfield{x}{$\Uparrow^2$x}{\textit{Ind}}\\
                                        \tfield{e}{dog(x)}}}\\
        \tfield{e}{bark($\mathfrak{c}$.x)}}$)$}} 
\end{quote}
 
\item
  $s:\text{few}_p(\text{dog}',\text{bark}'|_{\mathcal{F}(\text{dog}')})$
  iff 
\begin{quote}
$s$ :
  \record{\tfield{X}{$\overline{\text{few}_p^w(\text{dog}')}$}\\
          \tfield{f}{$((x:\mathfrak{T}(X))\rightarrow\neg$\record{\tfield{$\mathfrak{c}$}{\record{\mfield{x}{$\Uparrow^2$x}{\textit{Ind}}\\
                                        \tfield{e}{dog(x)}}}\\
        \tfield{e}{bark($\mathfrak{c}$.x)}}$)$}} 
\end{quote}
 
\end{subex} 
  
\end{ex}
Anything of the type resulting from applying the functions in
(\ref{ex:cont-few-dogs-bark}) to a context will also be of the types
in 
\nexteg{}.
\begin{ex} 
\begin{subex} 
 
\item \record{
    \mfield{restr}{dog$'$}{\textit{Ppty}}\\
    \mfield{scope}{bark$'\mid_{\mathfrak{F}(\text{dog}')}$}{\textit{Ppty}}\\
    \tfield{e}{\record{\tfield{X}{$\overline{\text{few}_a^w(\text{dog}')}$}\\
          \tfield{f}{$((x:\mathfrak{T}(X))\rightarrow\neg$\record{\tfield{$\mathfrak{c}$}{\record{\mfield{x}{$\Uparrow^2$x}{\textit{Ind}}\\
                                        \tfield{e}{dog(x)}}}\\
        \tfield{e}{bark($\mathfrak{c}$.x)}}$)$}} }} 
 
\item \record{
    \mfield{restr}{dog$'$}{\textit{Ppty}}\\
    \mfield{scope}{bark$'\mid_{\mathfrak{F}(\text{dog}')}$}{\textit{Ppty}}\\
    \tfield{e}{\record{\tfield{X}{$\overline{\text{few}_p^w(\text{dog}')}$}\\
          \tfield{f}{$((x:\mathfrak{T}(X))\rightarrow\neg$\record{\tfield{$\mathfrak{c}$}{\record{\mfield{x}{$\Uparrow^2$x}{\textit{Ind}}\\
                                        \tfield{e}{dog(x)}}}\\
        \tfield{e}{bark($\mathfrak{c}$.x)}}$)$}}}} 
 
\end{subex} 
   
\end{ex} 
This suggests that we could potentially have the anaphora in
\nexteg{}.
\begin{ex} 
\begin{subex} 
 
\item Few dogs barked.  They (dogs in general, $s$.restr, MAXSET)
  normally do when they notice an
  intruder.

\item Few dogs barked.  They (dogs in general which bark, $s$.scope)
  normally make such
  a racket.

  
\item Few dogs barked.  That (an event of few dogs barking, $s$.e, event
  anaphora) made it easier for the intruder.

\item Few dogs barked.  They (the dogs which didn't bark, $s$.e.X, 
   COMPSET anaphora) did not hear the intruder. 
 
\end{subex} 
   
\end{ex}   

% This, then yields a set up for COMPSET anaphora by providing the set
% in the `X'-field.

% \section{Binding and anaphora}
% \label{sec:binding-anaph}

\section{Long distance dependencies}
\label{sec:long-distance}

Let us consider how to derive the content of \textit{who Sam hugged}
as a relative clause.  We use \textbf{hug}$_V$ to represent the content of \textit{hug} as a transitive verb,
characterized as in \nexteg{}.

\begin{ex} 
\textbf{hug}$_V$ = $\ulcorner\lambda c$:\textit{Cntxt} . $\lambda
\mathcal{Q}$:\textit{Quant} . $\ulcorner\lambda
r$:\smallrecord{\smalltfield{x}{\textit{Ind}}}
. \smallrecord{\smalltfield{e}{hug($r$.x, $\mathcal{Q}$)}}$\urcorner\urcorner$ 
\end{ex} 
Our theory of syntax in terms of event types means that what have been
called ``gaps'' or ``traces'' in other theories of syntax would
somehow have to correspond to non-events in which nothing happens and
do not have any temporal extent.  This strongly suggests that they do
not exist.  Instead we will take a strategy similar to that pursued,
for example, in combinatory categorial grammar (see, for example,
\citealp{Steedman2012}) where \textit{hug} can also be interpreted as
a verb phrase whose content is ``looking for'' a \textit{wh}-phrase
content.  We will add a third component to our contexts with label
`$\mathfrak{g}$' for assignments associated with
gaps.  Thus we will redefine the type
\textit{Cntxt} as \nexteg{}.
\begin{ex} 
  \record{
    \tfield{$\mathfrak{s}$}{\textit{Assgnmnt}}\\
    \tfield{$\mathfrak{g}$}{\textit{Assgnmnt}}\\
    \tfield{$\mathfrak{c}$}{\textit{PropCntxt}}} 
\end{ex}

We will represent this content as
\textbf{hug}$_{\mathit{VP}}$ and characterize it in terms of
\textbf{hug}$_V$ as in \nexteg{a} which is identical with \nexteg{b}.
\begin{ex} 
\begin{subex}
\item \textbf{hug}$_{\mathit{VP}}$ = $\ulcorner\lambda
  c$:\smallrecord{
\footnotesize{\textit{Cntxt}}\\
    \smalltfield{$\mathfrak{g}$}{\smallrecord{
        \smalltfield{x$_0$}{\textit{Ind}}}}}
. \textbf{hug}$_V$($c$)($\lambda P$:\textit{Ppty}
. $P$(\smallrecord{\field{x}{$c.\mathfrak{g}$.x$_0$}}))$\urcorner$ 

\item
  $\ulcorner\lambda c$:\smallrecord{
\footnotesize{\textit{Cntxt}}\\
    \smalltfield{$\mathfrak{g}$}{\smallrecord{
        \smalltfield{x$_0$}{\textit{Ind}}}}}
  . $\ulcorner\lambda r$:\smallrecord{\smalltfield{x}{\textit{Ind}}}
  . \smallrecord{\smalltfield{e}{hug($r$.x, $\lambda P$:\textit{Ppty}
. $P$(\smallrecord{\field{x}{$c.\mathfrak{g}$.x$_0$}}))}}$\urcorner\urcorner$
\end{subex}
\end{ex}

Let us now consider the content of \textit{Sam hugged}.  % In order to
% avoid the additional complexity of combining different kinds of
% context which we will undertake in Section~\ref{sec:struc-cntxt} we
% will go back to the treatment of proper names in Chapter~\ref{ch:gram}
% rather than the treatment in Chapter~\ref{ch:propnames} where proper
% names introduce a constraint on the context. Thus we will consider the
% foreground of
The parametric content of \textit{Sam}, which we will
represent as \textbf{Sam}, is \nexteg{}
% where `sam' is a particular individual named Sam
.
\begin{ex} 
  \textbf{Sam} = $\ulcorner\lambda c$:\smallrecord{
\footnotesize{\textit{Cntxt}}\\
      \smalltfield{$\mathfrak{c}$}{\smallrecord{\smalltfield{x}{\textit{Ind}}\\
          \smalltfield{e}{named(x, ``Sam'')}}}} . $\lambda
    P$:\textit{Ppty} . $P(c.\mathfrak{c})\urcorner$

  % $\lambda\mathfrak{s}$:\textit{Rec} . $\lambda P$:\textit{Ppty} . $P$(\smallrecord{\field{x}{sam}})

\end{ex}
In order to combine \textbf{Sam} with \textbf{hug}$_{\mathit{VP}}$ we
will need to adjust the combination of parametric contents based on
functional application so that it takes account of incrementation of
the context path $\mathfrak{w}.\text{x}$ in addition to
$\mathfrak{s}.\text{x}$ to allow for more than one
\textit{wh}-dependency. This uses the operation `$\mathrm{incr}$' defined in
Chapter~\ref{ch:propnames}, p.~\pageref{pg:incr}.  We will use
\nexteg{a} to represent \nexteg{b}.
\begin{ex} 
\begin{subex} 
 
\item $\mathrm{incr}_{\pi_1,\ldots,\pi_n}(\varphi, T)$ 
 
\item
  $\mathrm{incr}_{\pi_1}(\ldots\mathrm{incr}_{\pi_n}(\varphi,T),\ldots, T)$ 
 
\end{subex} 
   
\end{ex}
We will informally use \nexteg{} to represent incrementation of all
paths which lead to assignments so that we do not have to keep track
of the required subscripts as we add additional assignments to our
contexts.  
\begin{ex} 
$\mathrm{incr}(\varphi, T)$ 
\end{ex} 
  
We now modify the definition of the combination of $\alpha$ and
$\beta$, $\alpha\text{@}\beta$, given in Chapter~\ref{ch:propnames},
p.~\pageref{ex:s-combination} to \nexteg{}.
\begin{ex}
If $\alpha$ : \smallrecord{\smalltfield{bg}{\textit{CntxtType}}\\
                           \smalltfield{fg}{(bg$\rightarrow$($T_1\rightarrow
                             T_2$))}} 
and $\beta$ : \smallrecord{\smalltfield{bg}{\textit{CntxtType}}\\
                           \smalltfield{fg}{(bg$\rightarrow T_1$)}}
                         then the \textit{combination of $\alpha$ and
    $\beta$  based on functional application}, $\alpha\text{@}\beta$, is
  \begin{quote}
   $\ulcorner\lambda c$:$[\alpha.\text{bg}]_{\mathfrak{c}\leadsto\mathfrak{c}.\text{f}}$
      \d{$\wedge$}$\mathrm{incr}([\beta.\text{bg}]_{\mathfrak{c}\leadsto\mathfrak{c}.\text{a}},\alpha.\text{bg})$
      . \\
      \hspace*{2em}$[\alpha]_{\mathfrak{c}\leadsto\mathfrak{c}.\text{f}}(c)(\mathrm{incr}([\beta.\text{fg}]_{\mathfrak{c}\leadsto\mathfrak{c}.\text{a}},\alpha.\text{bg})(c))\urcorner$

      
\end{quote}

 
\end{ex}

  

The content of \textit{Sam hugged}, which we will
represent as \textbf{Sam$^\frown$hugged}, is
\textbf{Sam}@\textbf{hug}$_{\mathit{VP}}$, that is \nexteg{a} which is
identical with \nexteg{b}.



\begin{ex} 
\begin{subex} 
 
\item \textbf{Sam$^\frown$hugged} = \\
  $\ulcorner\lambda c$:\smallrecord{
    \footnotesize{\textit{Cntxt}}\\
    \smalltfield{$\mathfrak{g}$}{\smallrecord{
        \smalltfield{x$_0$}{\textit{Ind}}}}\\
    \smalltfield{$\mathfrak{c}$}{\smallrecord{
        \smalltfield{f}{\smallrecord{
            \footnotesize{\textit{PropCntxt}}\\
            \smalltfield{x}{\textit{Ind}}\\
            \smalltfield{e}{named(x, ``Sam'')}}}\\
      \smalltfield{a}{\textit{PropCntxt}}}}}
  . \textbf{Sam}$_{\mathfrak{c}\leadsto\mathfrak{c}.\text{f}}$($c$)(\textbf{hug}$_{\mathit{VP},\mathfrak{c}\leadsto\mathfrak{c}.\text{a}}$($c$))$\urcorner$ 
 
\item
  $\ulcorner\lambda c$:\smallrecord{
    \footnotesize{\textit{Cntxt}}\\
    \smalltfield{$\mathfrak{g}$}{\smallrecord{
        \smalltfield{x$_0$}{\textit{Ind}}}}\\
    \smalltfield{$\mathfrak{c}$}{\smallrecord{
        \smalltfield{f}{\smallrecord{
            \footnotesize{\textit{PropCntxt}}\\
            \smalltfield{x}{\textit{Ind}}\\
            \smalltfield{e}{named(x, ``Sam'')}}}\\
      \smalltfield{a}{\textit{PropCntxt}}}}}
  .
  \smallrecord{\smalltfield{e}{hug($c$.f.x, $\lambda P$:\textit{Ppty} . $P$(\smallrecord{\field{x}{$c.\mathfrak{g}$.x$_0$}}))}}$\urcorner$
 
\end{subex} 
   
\end{ex}

In order to treat \textit{wh}-phrases we will add a fourth component
to contexts labelled with `$\mathfrak{w}$' for an assignment.  Thus we
revise \textit{Cntxt} to \nexteg{}.
\begin{ex} 
  \record{
    \tfield{$\mathfrak{s}$}{\textit{Assgnmnt}}\\
    \tfield{$\mathfrak{w}$}{\textit{Assgnmnt}}\\
    \tfield{$\mathfrak{g}$}{\textit{Assgnmnt}}\\
    \tfield{$\mathfrak{c}$}{\textit{PropCntxt}}} 
\end{ex}
% We also modify the definition of combination to increment the
% $\mathfrak{w}$-assignment as in \nexteg{}.
% \begin{ex}
% If $\alpha$ : \smallrecord{\smalltfield{bg}{\textit{CntxtType}}\\
%                            \smalltfield{fg}{(bg$\rightarrow$($T_1\rightarrow
%                              T_2$))}} 
% and $\beta$ : \smallrecord{\smalltfield{bg}{\textit{CntxtType}}\\
%                            \smalltfield{fg}{(bg$\rightarrow T_1$)}}
%                          then the \textit{combination of $\alpha$ and
%     $\beta$  based on functional application}, $\alpha\text{@}\beta$, is
%   \begin{quote}
%    $\ulcorner\lambda c$:$[\alpha.\text{bg}]_{\mathfrak{c}\leadsto\mathfrak{c}.\text{f}}$
%       \d{$\wedge$}$\mathrm{incr}_{\mathfrak{s}.\text{x},\mathfrak{w}.\text{x},\mathfrak{g}.\text{x}}([\beta.\text{bg}]_{\mathfrak{c}\leadsto\mathfrak{c}.\text{a}},\alpha.\text{bg})$
%       . \\
%       \hspace*{2em}$[\alpha]_{\mathfrak{c}\leadsto\mathfrak{c}.\text{f}}(c)(\mathrm{incr}_{\mathfrak{s}.\text{x},\mathfrak{w}.\text{x},\mathfrak{g}.\text{x}}([\beta.\text{fg}]_{\mathfrak{c}\leadsto\mathfrak{c}.\text{a}},\alpha.\text{bg})(c))\urcorner$

      
% \end{quote}

 
% \end{ex}



The content of \textit{who}, which we will represent
as \textbf{who}, is given in \nexteg{}.
\begin{ex} 
\textbf{who} =
$\ulcorner\lambda c$:\smallrecord{
  \footnotesize{\textit{Cntxt}}\\
  \smalltfield{$\mathfrak{w}$}{\smallrecord{
      \smalltfield{x$_0$}{\textit{Ind}}}}}
. $\lambda P$:\textit{Ppty} . $P$(\smallrecord{\field{x}{$c.\mathfrak{w}.\text{x}_0$}})$\urcorner$ 
\end{ex}
This content is identical with the universal resource `SemWhPron' and
is exactly parallel to `SemPron' but using the context label
`$\mathfrak{w}$' rather than `$\mathfrak{s}$'.  There will also be a
universal lexical resource `LexWhPron' parallel to `LexPron',
characterized in \nexteg{}.
\begin{ex} 
If $T_{\text{phon}}$ is a phonological type, then
LexWhPron($T_{\text{phon}}$) is
\begin{quote}
Lex($T_{\mathrm{phon}}$, \textit{NP}) \d{$\wedge$}
\smallrecord{\smallmfield{cont}{SemWhPron}{\textit{PQuant}}}
\end{quote} 
\end{ex}


\preveg{} makes a \textit{wh}-word such as \textit{who} into a noun
phrase and this is important, for instance, if it occurs in a noun
phrase position such as the subject or object of a sentence.  However,
these phrases also have a role as complementizers as \textit{who} does
in relative clauses, that is in a fronted position in the sentence and
not in a argument position to a verb or preposition.  It is important
in this case to recognize that this is a \textit{wh}-NP, that is, an
NP with a \textit{wh}-content.  For this we have the type in \nexteg{}
which we can abbreviate as \textit{WhNP}.
\begin{ex} 
  \record{
    \footnotesize{\textit{NP}}\\
    \mfield{cont}{SemWhPron}{\textit{PQuant}}}
\end{ex}
\preveg{} would, however, only allow the wh-index introduced by
`SemWhPron', that is `0´ and not allowing for incremented versions of
this obtained by combining constituents.
A more general way of characterizing the type \textit{WhNP} is to
treat it as a basic type with the witness condition in \nexteg{}.
\begin{ex} 
$\sigma$ : \textit{WhNP} iff $\sigma$ : \textit{NP}, $\sigma$.cont is $\mathcal{Q}$ and
$\mathcal{Q}.\text{bg}\sqsubseteq$\smallrecord{
  \smalltfield{$\mathfrak{w}$}{\smallrecord{
      \smalltfield{x$_i$}{\textit{Ind}}}}}, for some natural number $i$.

\end{ex} 
  


% In order to be able to characterize the kind of binding involved in
% combining \textit{who} with \textit{Sam hugged} we will define an
% operation, $\oplus$, which adds a field to a record or, if the label
% of the field being added
% is already present in the record, will replace that field with the new
% field.  This operation is characterized in \nexteg{}.
% \begin{ex} 
% If $r$ is a record, $\ell$ is a label and $v$ is some TTR object, then
% \\
% \hspace*{1em} $r\oplus[\ell=v]$ is \\
% \hspace*{2em} $r\cup\{\langle\ell,v\rangle\}$, if there is no $v'$
% such that $\langle\ell,v'\rangle\in r$\\
% \hspace*{2em}
% $(r-\{\langle\ell,r.\ell\rangle\})\cup\{\langle\ell,v\rangle\}$, otherwise 
% \end{ex} 
% We are using records here to do the work of partial variable
% assignments in logic and the $\oplus$-operation carries out the kind
% of modification which is performed on variable assignments when
% defining binding in the logical treatment.

In order to be able to characterize the kind of binding involved in
combining \textit{who} with \textit{Sam hugged} we will use the
notation $r[\pi=v]$ for a record, $r$, path, $\pi$, and value $v$.
This notation is characterized in \nexteg{}.
\begin{ex} 
If $r$ is a record, $\pi$ is $\ell_0.\ell_1.\ldots.\ell_n$ where
$\ell_0,\ell_1,\ldots,\ell_n$ are labels and $v$ is an object of some
type, then
\begin{quote}
  $r[\pi=v]$ is the record, $r'$, exactly like $r$ except for the
  possible difference that $r'.\pi=v$.
\end{quote}

\end{ex}
\begin{shaded}
  We can make \preveg{} more explicit as in \nexteg{}, repeated in Appendix~\ref{app:rec}.
  \begin{ex} 
    If $r$ is a record, $\pi$ is $\ell_0.\ell_1.\ldots.\ell_n$ where
    $\ell_0,\ell_1,\ldots,\ell_n$ are labels and $v$ is an object of some
    type, then
    \begin{quote}
      if $\pi\not\in\mathrm{paths}(r)$, then $r[\pi=v]$ is the
      smallest record, $r'$, such that
      \begin{enumerate} 
        
      \item $\pi\in\mathrm{paths}(r')$ 
        
      \item $r'.\pi=v$
        
      \item for any $\pi'\in\mathrm{paths}(r)$,
        $\pi'\in\mathrm{paths}(r')$ and $r'.\pi'=r.\pi'$
        
      \end{enumerate} 

      if $\pi\in\mathrm{paths}(r)$, then $r[\pi=v]$ is the
      smallest record, $r'$, such that
      \begin{enumerate} 
        
      \item  $\pi\in\mathrm{paths}(r')$ and $r'.\pi=v$
        
      \item  for any $\pi'\in(\mathrm{paths}(r)-\{\pi''\mid
        \pi''\leq\pi\})$, $\pi'\in\mathrm{paths}(r')$ and $r'.\pi'=r.\pi'$
        
      \end{enumerate}
    \end{quote}
    
  \label{ex:vary-assgnmnt}

  \end{ex} 
  
Recall that $\pi_1\leq\pi_2$ as used in \preveg{} means that $\pi_1$
is an initial subpath of $\pi_2$ (see Chapter~\ref{ch:propnames}, p.~\pageref{ex:subpath}).

\end{shaded}

We generalize this notation so that we can use a record to modify
another record.  This is characterized in \nexteg{}, where
$\mathrm{tpaths}(r)$ represents the set of total paths in $r$ (Chapter~\ref{ch:percint},p.~\pageref{pg:record-paths}).
\begin{ex} 
If $r_1$ is a record and $r_2$ is a record such
$\mathrm{tpaths}(r_2)=\{\pi_1,\ldots,\pi_n\}$, then $r_1[r_2]$ is
$r_1[\pi_1=r_2.\pi_1]\ldots[\pi_n=r_2.\pi_n]$ 
\end{ex} 
  
  

This now gives us what we
need to characterize the content of the relative
clause \textit{who Sam hugged}, which we will represent as
\textbf{who}$^\frown$\textbf{Sam}$^\frown$\textbf{hugged}, as in
\nexteg{a} which is identical with \nexteg{b}.  \nexteg{b} is in turn
equivalent to \nexteg{c} because of the constraint on the extensional
predicate `hug' similar to that for `find' given in  (\ref{ex:mp-find})
on p.~\pageref{ex:mp-find}. 
\begin{ex} 
\begin{subex} 
 
\item \textbf{who}$^\frown$\textbf{Sam}$^\frown$\textbf{hugged} = \\
  $\ulcorner\lambda c$:\smallrecord{
    \footnotesize{\textit{Cntxt}}\\
    \smalltfield{$\mathfrak{c}$}{\smallrecord{
        \smalltfield{f}{\textit{PropCntxt}}\\
        \smalltfield{a}{\smallrecord{
        \smalltfield{f}{\smallrecord{
            \footnotesize{\textit{PropCntxt}}\\
            \smalltfield{x}{\textit{Ind}}\\
            \smalltfield{e}{named(x, ``Sam'')}}}\\
      \smalltfield{a}{\textit{PropCntxt}}}}}}} . \\
\hspace*{1em}$\ulcorner\lambda
  r_1$:\smallrecord{\smalltfield{x}{\textit{Ind}}}
  . \\
\hspace*{2em}\textbf{who}$_{\mathfrak{c}\leadsto\mathfrak{c}.\text{f}}$($c[\mathfrak{w}.\text{x}_0=r_1.\text{x}]$)
($\ulcorner\lambda
  r_2$:\smallrecord{\smalltfield{x}{\textit{Ind}}} . \textbf{Sam}$^\frown$\textbf{hugged}$_{\mathfrak{c}\leadsto\mathfrak{c}.\text{a}}$($c[\mathfrak{g}.\text{x}_0=r_2.\text{x}]$)$\urcorner$)$\urcorner\urcorner$ 
 
\item $\ulcorner\lambda c$:\smallrecord{
    \footnotesize{\textit{Cntxt}}\\
    \smalltfield{$\mathfrak{c}$}{\smallrecord{
        \smalltfield{f}{\textit{PropCntxt}}\\
        \smalltfield{a}{\smallrecord{
        \smalltfield{f}{\smallrecord{
            \footnotesize{\textit{PropCntxt}}\\
            \smalltfield{x}{\textit{Ind}}\\
            \smalltfield{e}{named(x, ``Sam'')}}}\\
        \smalltfield{a}{\textit{PropCntxt}}}}}}} . \\
\hspace*{1em}$\ulcorner\lambda
  r_1$:\smallrecord{\smalltfield{x}{\textit{Ind}}}
  . \smallrecord{\smalltfield{e}{hug($c.\mathfrak{c}.$a.f.x, $\lambda P$:\textit{Ppty}
      . $P$(\smallrecord{\field{x}{$r_1$.x}}))}}$\urcorner\urcorner$

\item $\ulcorner\lambda c$:\smallrecord{
    \footnotesize{\textit{Cntxt}}\\
    \smalltfield{$\mathfrak{c}$}{\smallrecord{
        \smalltfield{f}{\textit{PropCntxt}}\\
        \smalltfield{a}{\smallrecord{
        \smalltfield{f}{\smallrecord{
            \footnotesize{\textit{PropCntxt}}\\
            \smalltfield{x}{\textit{Ind}}\\
            \smalltfield{e}{named(x, ``Sam'')}}}\\
      \smalltfield{a}{\textit{PropCntxt}}}}}}} . $\ulcorner\lambda
  r_1$:\smallrecord{\smalltfield{x}{\textit{Ind}}}
  . \smallrecord{\smalltfield{e}{hug$^\dagger$($c.\mathfrak{c}.$a.f.x, $r_1$.x))}}$\urcorner\urcorner$ 
 
\end{subex} 
   
\end{ex}

In order to achieve this we need a general operation of
\textit{wh}-combination which will pass whatever context restrictions
are associated with the \textit{wh}-phrase and those that are
associated with the phrase with which it is being combined up to
context restrictions associated with the whole phrase except for those
associated with the paths `$\mathfrak{w}.\text{x}_i$' (for the
\textit{wh}-phrase which is binding the gap) and
`$\mathfrak{g}.\text{x}_j$' (for the gap being bound).  The
discharging of the requirements associated with these two paths will
involve subtracting them from the types which are passed up to the
context type for the combined phrase.

As record types are labelled
sets (Chapter~\ref{ch:percint}, p.~\pageref{ex:ndrectypes}ff.), this
subtraction is based on set-theoretic subtraction.  % We will limit what
% can be subtracted to total paths (Chapter~\ref{ch:percint},
% p.~\pageref{ex:paths-rectype}).  In \nexteg{} we give a preliminary
% characterization of what it means to subtract a total path, $\pi$,
% from a record type, $T$ which we represent as $T\ominus\pi$.
% \begin{ex} 
% (preliminary) If $T$ is a record type and $\pi\in\mathrm{tpaths}(T)$, then
% $T\ominus\pi$ is the type $T'$ exactly like $T$ except that $\mathrm{tpaths}(T')=\mathrm{tpaths}(T)-\{\pi\}$. 
% \end{ex}

We first define what it means to subtract the field labelled $\ell$
from an assignment type, $T$, in \nexteg{}.
\begin{ex} 
  If $T\sqsubseteq\textit{Assgnmnt}$ and
  $\ell\in\mathrm{labels}(T)$, then
  \begin{enumerate} 
    
  \item if $\mathrm{labels}(T)=\{\ell\}$, then $T\ominus\ell=\textit{Assgnmnt}$ 
    
  \item otherwise, $T\ominus\ell=T-\{\langle\ell,\varphi\rangle\}$,
    where $\langle\ell,\varphi\rangle\in T$.
    
    
  \end{enumerate} 
    
\end{ex} 
Based on \preveg{} we can define the subtraction of a path to an
assignment in a context type given in \nexteg{}.
\begin{ex} (preliminary)
  
  If $T\sqsubseteq$ \smallrecord{
    \footnotesize{\textit{Cntxt}}\\
    \smalltfield{$\ell_1$}{\smallrecord{
        \footnotesize{\textit{Assgnmnt}}\\
        \smalltfield{$\ell_2$}{\textit{Ind}}}}}, then
  $T\ominus\ell_1.\ell_2$ is $T$\fbox{\d{$\wedge$}}\smallrecord{
    \smalltfield{$\ell_1$}{$(T.\ell_1\ominus\ell_2)$}}
\end{ex} 
  
\begin{shaded}
  
This is a preliminary definition because it does not take account of
what happens if the path that is being removed has dependent fields
associated with it.  Suppose, for example, that the context type
associated with \textit{who} were \nexteg{} where we represent the
presupposition that what is associated with \textit{who} is a person.
\begin{ex} 
  \record{
    \footnotesize{\textit{Cntxt}}\\
    \tfield{$\mathfrak{w}$}{\record{
        \tfield{x$_0$}{\textit{Ind}}}}\\
    \tfield{$\mathfrak{c}$}{\record{
        \tfield{e}{person($\Uparrow$$\mathfrak{w}$.x$_0$)}}}}
\end{ex}
Suppose that $T$ is \preveg{}. Then $T\ominus\mathfrak{w}.\text{x}_0$
according to our present definition would be \nexteg{} which is not a
record type since there is a dependence on `$\mathfrak{w}.\text{x}_0$'
but there is no such path.
\begin{ex} 
 \record{
    \footnotesize{\textit{Cntxt}}\\
    \tfield{$\mathfrak{w}$}{\textit{Assgnmnt}}\\
    \tfield{$\mathfrak{c}$}{\record{
        \tfield{e}{person($\Uparrow$$\mathfrak{w}$.x$_0$)}}}}
\label{ex:who-person}
\end{ex} 
The solution to this is to extend subtraction so
that it removes not only the path referred to but also those paths
that depend on it.  Thus the result of
$T\ominus\mathfrak{w}.\text{x}_0$ should rather be \nexteg{}.
\begin{ex} 
\record{
    \footnotesize{\textit{Cntxt}}\\
    \tfield{$\mathfrak{w}$}{\textit{Assgnmnt}}\\
    \tfield{$\mathfrak{c}$}{\textit{PropCntxt}}} 
\end{ex} 
In this particular case, the resulting type, \preveg{}, is actually
identical with \textit{Cntxt}.


Actually, things are more complicated that this.  For any path we
remove by this method we must recursively remove all the dependencies
on that path.  Thus if something had depended on
`$\mathfrak{c}.\text{e}$' in the above example we would have had to
remove that and so on. In our context types, as defined here, all the
dependencies on assignments will occur under the label
`$\mathfrak{c}$', that is, in the propositional context.  It is
perhaps most straightforward to use the unique identifier notation
introduced in Chapter~\ref{ch:infex},
p.~\pageref{pg:unique-identifier-notation}, in order to identify paths
which depend on another path.  Consider again
(\ref{ex:who-person}). In unique identifier notation this is
\nexteg{}.
\begin{ex}
  \record{
    \footnotesize{\textit{Cntxt}}\\
    \tfield{$\mathfrak{w}$}{\record{
        \tfield{x$_{0_\text{\fbox{0}}}$}{\textit{Ind}}}}\\
    \tfield{$\mathfrak{c}$}{\record{
        \tfield{e}{person(\fbox{0})}}}}
\end{ex}
In \preveg{}, the path `$\mathfrak{c}$.e' depends on
`$\mathfrak{w}$.x$_0$'  because the representation of the type at the
former contains the unique identifier which indexes the latter.  We
give a general characterization of dependency between paths in a
record type in \nexteg{} (repeated in Appendix~\ref{app:dep-rectype}).
\begin{ex} 
If $T$ is a record type, $\pi_1\in\mathrm{paths}(T)$ and
$\pi_2\in\mathrm{tpaths}(T)$, then $\pi_2$ \textit{depends on} $\pi_1$
iff, in unique identifier notation, $\pi_1$ is indexed with \fbox{$i$}
and the representation of $T.\pi_2$ contains \fbox{$i$}, for some
natural number $i$.
\label{ex:path-dep}  
\end{ex} 
Given this notion of dependency it is then possible to define the set
of paths in a record type, $T$, which constitute a dependency family on some
particular path, $\pi$, which we will represent as
$\mathrm{paths}_{\pi}(T)$.  This is given in \nexteg{} (repeated in Appendix~\ref{app:dep-rectype}).
\begin{ex} 
If $T$ is a record type and $\pi\in\mathrm{paths}(T)$ then \textit{the
  dependency family of $\pi$ in $T$},
$\mathrm{paths}_\pi(T)$, is that subset, $\Pi$, of $\mathrm{paths}(T)$
such that
\begin{enumerate} 
 
\item $\pi\in\Pi$ 
 
\item for any $\pi'\in\Pi$ and $\pi''\in\mathrm{tpaths}(T)$, if
  $\pi''$ depends on $\pi'$, then $\pi''\in\Pi$

\item for and $\pi'\in\Pi$ and $\pi''\in\mathrm{paths}(T)$, if $\pi'$
  depends on $\pi''$, then $\pi''\in\Pi$
 
\end{enumerate}

We use $\pi/T$ as an shorter alternative notation for $\mathrm{paths}_{\pi}(T)$.
\label{ex:path-dep-fam}
\end{ex}
That is, the dependency family of $\pi$ includes $\pi$ itself,
anything that depends on anything in the dependency family and
anything on which something in the dependency family depends.  This
dependency family gives rise to a generalization of the original type,
$T$, which we will call \textit{$T$ generalized to $\pi$}, $T^\pi$.
We define this in \nexteg{} (repeated in Appendix~\ref{app:dep-rectype}).
\begin{ex} 
If $T$ is a record type and $\pi\in\mathrm{paths}(T)$, then $T$
\textit{generalized to} $\pi$, $T^\pi$, is the smallest labelled set $T'$ such
that $\mathrm{paths}_\pi(T)\subseteq\mathrm{paths}(T')$ and for all
$\pi'\in\mathrm{tpaths}(T')$, $T'.\pi=T.\pi$
\label{ex:rectype-gen}
\end{ex}
We give a definition of a more general version of \preveg{} in
\nexteg{} (repeated in Appendix~\ref{app:dep-rectype}) where we generalize to several paths in a type
simultaneously.
\begin{ex} 
If $T$ is a record type and $\{\pi_1,\ldots,\pi_n\}\subset\mathrm{paths}(T)$, then $T$
\textit{generalized to} $\pi_1,\ldots,\pi_n$, $T^{\pi_1,\ldots,\pi_n}$, is the smallest labelled set $T'$ such
that for all $\pi_i\in\{\pi_1,\ldots,\pi_n\}$, $\mathrm{paths}_{\pi_i}(T)\subseteq\mathrm{paths}(T')$ and for all
$\pi'\in\mathrm{tpaths}(T')$, $T'.\pi=T.\pi$
\label{ex:rectype-gen-gen}
\end{ex}
This notion of generalization is important if we wish to associate
presuppositions with \textit{wh}-phrases and extract them from the
context type for local accommodation at the point at which the
\textit{wh}-phrase binds a gap.

We can now generalize the subtraction operation, $\ominus$.  First we
will characterize branching paths in a labelled set,  as in
\nexteg{}.
\begin{ex} 
If $X$ is a labelled set and $\pi\in\mathrm{tpaths}(X)$ then $\pi$
\textit{is branching in} $X$ iff
\begin{enumerate} 
 
\item there is some $\pi'\in\mathrm{tpaths}(X)$ such that $\pi'\not=\pi$ 
 
\item there is some $\pi''$ such that $\pi''<\pi'$ and $\pi''<\pi$ 
 
\end{enumerate} 
  
\end{ex} 
(Recall that $\pi_1<\pi_2$ means that $\pi_1$ is a proper initial
subpath of $\pi_2$, Chapter~\ref{ch:propnames},
p.~\pageref{ex:subpath}.)

We characterize subtraction in general for labelled sets as \nexteg{}
(repeated in Appendix~\ref{app:sets}).
\begin{ex} 
\begin{subex} 
 
\item If $X$ is a labelled set, $\ell\in\mathrm{labels}(X)$ and
  $\langle\ell,\varphi\rangle\in X$, then
  \begin{quote}
    $X\ominus\ell=X-\{\langle\ell,\varphi\rangle\}$
  \end{quote}
  
 
\item If $X$ is a labelled set, $\langle\ell,\varphi\rangle\in X$ and
  $\ell.\pi\in\mathrm{tpaths}(X)$, then
  \begin{quote}
    if $\ell.\pi$ is branching in $X$, then
    \begin{quote}
      $X\ominus\ell.\pi=(X-\{\langle\ell,\varphi\rangle\})\cup\{\langle\ell,\varphi\ominus\pi\rangle\}$
    \end{quote}
    otherwise
    \begin{quote}
      $X\ominus\ell.\pi=X-\{\langle\ell,\varphi\rangle\}$
    \end{quote}
  \end{quote}
  
 
\end{subex} 
\label{ex:subtraction-labelled-sets}   
\end{ex}
If $X$ is a labelled set and
$\pi_1,\ldots,\pi_n\in\mathrm{tpaths}(X)$, then we write \nexteg{a}
for \nexteg{b}
\begin{ex}
  \begin{subex}
  
  \item $X\ominus\pi_1,\ldots,\pi_n$

  
  \item $X\ominus\pi_1\ominus\ldots\ominus\pi_n$
  \end{subex}
  
\end{ex}

If $T$ is a record type, $\pi\in\mathrm{paths}(T)$ and
  $\mathrm{paths}_\pi(T)=\{\pi,\pi_1,\ldots,\pi_n\}$, then
     we normally write $T\ominus\pi/T$ for
    $T\ominus\pi,\pi_1,\ldots,\pi_n$.
 
We now extend subtraction to include some cases where it would
otherwise be undefined.

\begin{ex} 
  \begin{enumerate} 

  
 
\item If $T$ is \textit{Assgnmnt}$\wedge T'$, $T'$ is a record type and
  $\ell\in\mathrm{labels}(T')$, then
  \begin{enumerate} 
    
  \item if $\mathrm{labels}(T')=\{\ell\}$, $T\ominus\ell=\textit{Assgnmnt}$ 
    
  \item otherwise, $T\ominus\ell= \textit{Assgnmnt}\wedge (T'\ominus\ell/T)$
    
  \end{enumerate}
  
% \item If $T$ is \textit{PropCntxt}$\wedge T'$, $T'$ is a record type and
%   $\ell\in\mathrm{labels}(T')$, then
%   \begin{enumerate} 
    
%   \item if $\mathrm{labels}(T')=\{\ell\}$, $T\ominus\ell=\textit{PropCntxt}$
    
%   \item otherwise, $T\ominus\ell=\textit{PropCntxt}\wedge (T'\ominus\ell/T)$
    
%   \end{enumerate} 

\item If $T$ is \textit{PropCntxt}$\wedge T'$ and
  $\pi\in\mathrm{tpaths}(T')$ then
  \begin{enumerate}
    
  \item if $\pi$ is $\ell$ and $\mathrm{labels}(T')=\{\ell\}$, then $T\ominus\pi=\textit{PropCntxt}$
    
  \item otherwise, $T\ominus\pi= \textit{PropCntxt}\wedge(T'\ominus \pi/T')$
  \end{enumerate}

% \item Otherwise, if $T$ is a labelled set, then
%   \begin{enumerate}
%   \item if $\ell.\pi\in\mathrm{tpaths}(T)$ and
%     $\langle\ell,\varphi\rangle\in T$, then
%     $T\ominus\ell.\pi=(T-\{\langle\ell,\varphi\rangle\})\cup\{\langle\ell,\varphi\ominus\pi\rangle\}$
%   \item otherwise, $T\ominus\pi$ is $T$
%  \end{enumerate}

  
 
\end{enumerate} 
\label{ex:ominus}   
\end{ex} 


  
  
\end{shaded}

We can now create a preliminary definition of combination based on
functional application for \textit{wh}-phrases and sentences with
gaps, `@$_{\mathrm{wh}}$', characterized in \nexteg{}.
\begin{ex} 
  (preliminary)

  If
  \begin{enumerate}
  \item $\alpha$ : \smallrecord{
      \smalltfield{bg}{\textit{CntxtType}}\\
      \smalltfield{fg}{(bg$\rightarrow$\textit{Quant})}},
    
  \item $\beta$ : \smallrecord{
      \smalltfield{bg}{\textit{CntxtType}}\\
      \smalltfield{fg}{(bg$\rightarrow$\textit{RecType})}},
    
  \item $\alpha$.bg $\sqsubseteq$ \smallrecord{
      \smalltfield{$\mathfrak{w}$}{\smallrecord{
          \smalltfield{x$_i$}{\textit{Ind}}}}} for some natural number,
    $i$, and
    
  \item $\beta$.bg $\sqsubseteq$ \smallrecord{
      \smalltfield{$\mathfrak{g}$}{\smallrecord{
          \smalltfield{x$_j$}{\textit{Ind}}}}} for some natural number,
    $j$,
  \end{enumerate}
  then \textit{the \textit{wh}$_{i,j}$-combination of $\alpha$ and
    $\beta$}, $\alpha\text{@}_{\mathrm{wh}_{i,j}}\beta$, is
  \begin{quote}
    $\ulcorner\lambda
    c$:([$\alpha$.bg$\ominus\mathfrak{w}.\text{x}_i$]$_{\mathfrak{c}\leadsto\mathfrak{c}.\text{f}}$\d{$\wedge$}$\mathrm{incr}([\beta.\text{bg}\ominus\mathfrak{g}.\text{x}_j]_{\mathfrak{c}\leadsto\mathfrak{c}.a},\alpha.\text{bg})$)
    .
    \hspace*{1em} $\mathfrak{P}(\ulcorner\lambda r_1$:\smallrecord{
      \smalltfield{x}{\textit{Ind}}\\
      \smalltfield{$\mathfrak{w}$}{\smallrecord{
          \smallmfield{x$_i$}{$\Uparrow$x}{\textit{Ind}}}}} . \\
    \hspace*{4em}$\alpha_{\mathfrak{c}\leadsto\mathfrak{c}.\text{f}}(c[r_1])$
    ($\mathfrak{P}(\ulcorner\lambda r_2$:\smallrecord{
      \smalltfield{x}{\textit{Ind}}\\
      \smalltfield{$\mathfrak{g}$}{\smallrecord{
          \smallmfield{x$_j$}{$\Uparrow$x}{\textit{Ind}}}}} . \\
    \hspace*{13em}$\mathrm{incr}(\beta_{\mathfrak{c}\leadsto\mathfrak{c}.\text{a}},\alpha.\text{bg})(c[r_2])\urcorner)$)$\urcorner)\urcorner$
  \end{quote}
  
\end{ex}
Recall that $\mathfrak{P}(P)$ represents the purification of the
property $P$ defined in (\ref{ex:purification}) on p.~\pageref{ex:purification}.
 
\begin{shaded}
We can adjust \preveg{} to take account of any presuppositions
introduced by the \textit{wh} and gap interpretations as in \nexteg{}.
\begin{ex} 
  If
  \begin{enumerate}
  \item $\alpha$ : \smallrecord{
      \smalltfield{bg}{\textit{CntxtType}}\\
      \smalltfield{fg}{(bg$\rightarrow$\textit{Quant})}},
    
  \item $\beta$ : \smallrecord{
      \smalltfield{bg}{\textit{CntxtType}}\\
      \smalltfield{fg}{(bg$\rightarrow$\textit{RecType})}},
    
  \item $\alpha$.bg $\sqsubseteq$ \smallrecord{
      \smalltfield{$\mathfrak{w}$}{\smallrecord{
          \smalltfield{x$_i$}{\textit{Ind}}}}} for some natural number,
    $i$, and
    
  \item $\beta$.bg $\sqsubseteq$ \smallrecord{
      \smalltfield{$\mathfrak{g}$}{\smallrecord{
          \smalltfield{x$_j$}{\textit{Ind}}}}} for some natural number,
    $j$,
  \end{enumerate}
  then \textit{the \textit{wh}$_{i,j}$-combination of $\alpha$ and
    $\beta$}, $\alpha\text{@}_{\mathrm{wh}_{i,j}}\beta$, is
  \begin{quote}
    $\ulcorner\lambda
    c$:([$\alpha$.bg$\ominus\mathrm{paths}_{\mathfrak{w}.\text{x}_i}(\alpha.\text{bg})]_{\mathfrak{c}\leadsto\mathfrak{c}.\text{f}}$\d{$\wedge$}\\
    \hspace*{5em}$\mathrm{incr}([\beta.\text{bg}\ominus\mathrm{paths}_{\mathfrak{g}.\text{x}_j}(\beta.\text{bg})]_{\mathfrak{c}\leadsto\mathfrak{c}.a},\alpha.\text{bg})$)
    . \\
    \hspace*{1em} $\mathfrak{P}(\ulcorner\lambda r_1$:$[\alpha.\text{bg}^{\mathfrak{w}.\text{x}_i}]_{\mathfrak{w}.\text{x}_i\leadsto\text{x}}$ . \\
    \hspace*{4em}$\alpha_{\mathfrak{c}\leadsto\mathfrak{c}.\text{f},\mathfrak{w}.\text{x}_i\leadsto\text{x}}(c[r_1])$
    ($\mathfrak{P}(\ulcorner\lambda r_2$:$[\beta.\text{bg}^{\mathfrak{g}.\text{x}_j}]_{\mathfrak{g}.\text{x}_j\leadsto\text{x}}$ . \\
    \hspace*{15em}$\mathrm{incr}(\beta_{\mathfrak{c}\leadsto\mathfrak{c}.\text{a},\mathfrak{g}.\text{x}_j\leadsto\text{x}},\alpha.\text{bg})(c[r_2])\urcorner)$)$\urcorner)\urcorner$
  \end{quote} 
\end{ex}
The effect of the property purification here will be to locally
accommodate whatever presuppositions are associated
`$\mathfrak{w}.\text{x}_i$' or `$\mathfrak{g}.\text{x}_j$' at the
level at which the \textit{wh}-binding takes place.
  
We leave the treatment of contraints on long distance dependencies
like \textit{wh}-constructions (such as \textit{island constraints})
to future work.  The strategy for handling these would be to elaborate
on the conditions 1.--4. in \preveg{} or as conditions associated with
constituent structure rules.
\end{shaded}
We can then define a version of `ContForwardApp' (forward application
of contents) based on wh$_{i,j}$-combination as given in \nexteg{}.
\begin{ex} 
If $T_{\text{fun}}$, $T_{\text{arg}}$ and $T_{\text{res}}$ are types
such that if $\alpha:T_{\text{fun}}$ and $\beta:T_{\text{arg}}$, then
$\alpha\text{@}_{\text{wh}_{i,j}}\beta$ is defined and of type
$T_{\text{res}}$, then
\begin{quote}
  ContForwardApp$_{\text{@}_{\text{wh}_{i,j}}}$($T_{\text{fun}},T_{\text{arg}},T_{\text{res}}$)
\end{quote}
is
\begin{quote}
  $\lambda u$:\smallrecord{
    \smalltfield{cont}{$T_{\text{fun}}$}}$^\frown$\smallrecord{
    \smalltfield{cont}{$T_{\text{arg}}$}} . \smallrecord{
    \smallmfield{cont}{$u[0]$.cont@$_{\text{wh}_{i,j}}u[1]$.cont}{$T_{\text{res}}$}}
\end{quote}
  
\end{ex}

We can then characterize a notation for phrase structure rules which
use `ContForwardApp$_{\text{@}_{\text{wh}_{i,j}}}$' as in \nexteg{}.
\begin{ex} 
If $T_{\text{mother}}$, $T_{\text{daughter}_1}$ and
  $T_{\text{daughter}_2}$ are sign
  types, $T_{\text{daughter}_1}\sqsubseteq$\smallrecord{
    \smallmfield{cont}{$c_1$}{\textit{Cont}}} where
  $c_1.\text{bg}\sqsubseteq$\smallrecord{
    \smalltfield{$\mathfrak{w}$}{\smallrecord{
        \smalltfield{x$_i$}{\textit{Ind}}}}}, $T_{\text{daughter}_2}\sqsubseteq$\smallrecord{
    \smallmfield{cont}{$c_2$}{\textit{Cont}}} where
  $c_2.\text{bg}\sqsubseteq$\smallrecord{
    \smalltfield{$\mathfrak{g}$}{\smallrecord{
        \smalltfield{x$_j$}{\textit{Ind}}}}} and $T_{\text{arg}}$ and
  $T_{\text{res}}$ are content types, then
  \begin{quote}
    $T_{\text{mother}}\longrightarrow
    T_{\text{daughter}_1}\ T_{\text{daughter}_2}\ \mid\
T_{\text{daughter}_1}'(_{\text{@}_{\text{wh}_{i,j}}}T_{\text{daughter}_2}':T_{\text{arg}}):T_{\text{res}}$
  \end{quote}
  is
  \begin{quote}
  $T_{\text{mother}}\longrightarrow
    T_{\text{daughter}_1}\ T_{\text{daughter}_2}$ \d{\d{$\wedge$}}
    ContForwardApp$_{\text{@}_{\text{wh}_{i,j}}}$($T_{\text{arg}}$, $T_{\text{res}}$)
  \end{quote}  
 
\end{ex} 
We introduce a sign type \textit{Rel} which
requires the category to be `rel' for relative clause  and types
\textit{NP}$_{\text{wh}_i}$ and \textit{S}/$i$ whose witness
conditions are given in \nexteg{}.
\begin{ex} 
\begin{subex} 
 
\item $\alpha:\textit{NP}_{\text{wh}_i}$ iff $\alpha:\textit{NP}$ and
  $\alpha.\text{cont}.\text{bg}\sqsubseteq$\smallrecord{
    \smalltfield{$\mathfrak{w}$}{\smallrecord{
        \smalltfield{x$_i$}{\textit{Ind}}}}}
 
\item $\alpha:\textit{S}/i$ iff $\alpha:\textit{S}$ and $\alpha.\text{cont}.\text{bg}\sqsubseteq$\smallrecord{
    \smalltfield{$\mathfrak{g}$}{\smallrecord{
        \smalltfield{x$_i$}{\textit{Ind}}}}} 
 
\end{subex} 
   
\end{ex} 
The slash notation `$\textit{S}/i$' is derived from the use of slash
categories to represent constituents containing gaps in Generalized
Phrase Structure Grammar \citep{GazdarKleinPullumSag1985}  and Head
Driven Phrase Structure Grammar \citep{Sag:Wasow:ea:03}.

We can now add the rule in \nexteg{} to the language specific
resources for English.
\begin{ex} 
\textit{Rel} $\longrightarrow$ \textit{NP}$_{\text{wh}_i}$
\textit{S}/$j$ $\mid$
\textit{NP}$_{\text{wh}_i}'$($_{\text{@}_{\text{wh}_{i,j}}}$\textit{S}/$j'$:\textit{PRecType}):\textit{PPpty} 
\end{ex} 

To form the content of a noun modified by a relative clause such as
\textit{child who Sam hugged} we use a record type which requires of
an individual that it has both the property of being a child and being
hugged by Sam as given in \nexteg{}.
\begin{ex} 
  $\ulcorner\lambda c$: \smallrecord{
    \footnotesize{\textit{Cntxt}}\\
    \smalltfield{$\mathfrak{c}$}{\smallrecord{
        \smalltfield{f}{\textit{PropCntxt}}\\
        \smalltfield{a}{\smallrecord{
            \smalltfield{f}{\textit{PropCntxt}}\\
            \smalltfield{a}{\smallrecord{
                \smalltfield{f}{\smallrecord{
                    \footnotesize{\textit{PropCntxt}}\\
                    \smalltfield{x}{\textit{Ind}}\\
                    \smalltfield{e}{named(x, ``Sam'')}}}\\
                \smalltfield{a}{\textit{PropCntxt}}}}}}}}} .  \\
  \hspace*{1em}$\ulcorner\lambda
  r$:\smallrecord{\smalltfield{x}{\textit{Ind}}}
  . \\
  \hspace*{2em}\record{
    \tfield{e$_1$}{child$'$\{$r$.x\}}\\
    \tfield{e$_2$}{\textbf{who$^\frown$Sam$^\frown$hugged$_{\mathfrak{c}\leadsto\mathfrak{c}.\text{a}}$}($c$)\{$r$.x\}}}$\urcorner\urcorner$  
\end{ex}

In order to achieve this we will first introduce an operation of
property conjunction in \nexteg{}.  As a preliminary, we introduce
types for properties and parametric properties of particular types of
objects.  This is done in \nexteg{}.
\begin{ex} 
\begin{subex} 
 
\item If $T$ is a type, then $^T\textit{Ppty}$ is a type -- ``the type
  of properties of objects of type $T$'' 
 
\item $P:{^T\textit{Ppty}}$ iff $P:\textit{Ppty}$ and
  $P.\text{bg}\sqsubseteq$ \smallrecord{
    \smalltfield{x}{$T$}}
  
\item If $T$ is a type, then $^T\textit{PPpty}$ is a type -- ``the type
  of parametric properties of objects of type $T$''
  
\item $\mathcal{P}:{^T\textit{PPpty}}$ iff
  $\mathcal{P}:\textit{PPpty}$ and for any $c:\mathcal{P}.\text{bg}$, $\mathcal{P}(c):{^T\textit{Ppty}}$
 
\end{subex} 
   
\end{ex}
We can now characterize property conjunction as in \nexteg{}.
\begin{ex} 
If $T$ is a type, $P_1:{^T\textit{Ppty}}$ and $P_2:{^T\textit{Ppty}}$,
then \textit{the conjunction of $P_1$ and
  $P_2$}, $P_1\&P_2$, is
\begin{quote}
  $\ulcorner\lambda r$:\smallrecord{
    \smalltfield{x}{$T$}} .
  \record{
    \tfield{e$_1$}{$P_1\{r.\text{x}\}$}\\
    \tfield{e$_2$}{$P_2\{r.\text{x}\}$}}$\urcorner$
\end{quote}

\end{ex}
We can now characterize a combination operation, @$_{\&}$, in
\nexteg{}.
\begin{ex}
  
  If $T$ is a type, $\alpha:{^T\textit{PPpty}}$ and
  $\beta:{^T\textit{PPpty}}$ 
  then \textit{the property conjunction
    combination of $\alpha$ and $\beta$}, $\alpha\text{@}_{\&}\beta$,
  is
\begin{quote}
  $\lambda
  c$:$[\alpha.\text{bg}]_{\mathfrak{c}\leadsto\mathfrak{c}.\text{f}}$\d{$\wedge$}$\mathrm{incr}([\beta.\text{bg}]_{\mathfrak{c}\leadsto\mathfrak{c}.\text{a}},\alpha.\text{bg})$
        . $\alpha_{\mathfrak{c}\leadsto\mathfrak{c}.\text{f}}(c)\&\mathrm{incr}([\beta]_{\mathfrak{c}\leadsto\mathfrak{c}.\text{a}},\alpha.\text{bg})(c)$
\end{quote}
\end{ex}

We introduce a version of `ContForwardApp' for `@$_{\text{\&}}$' in
\nexteg{}.
\begin{ex} 
  If $T$ is a type, then ContForwardApp$_{\text{@}_{\&}}$($T$) is
  \begin{quote}
    $\lambda u$:\record{
      \tfield{cont}{${^T\textit{PPpty}}$}}$^\frown$\record{
      \tfield{cont}{${^T\textit{PPpty}}$}} .\\
    \hspace*{1em}\record{
      \mfield{cont}{$u[0].\text{cont}\text{@}_{\&}u[1].\text{cont}$}{${^T\textit{PPpty}}$}}
  \end{quote}
  
\end{ex} 
We can then introduce a notation of constituent structure rules which
use `ContForwardApp$_{\text{@}_{\&}}$' in \nexteg{}.
\begin{ex} 
If $T$ is a type, $T_{\text{mother}}$, $T_{\text{daughter}_1}$ and
$T_{\text{daughter}_2}$ are sign types,
$T_{\text{daughter}_1}\sqsubseteq$ \record{
  \tfield{cont}{$^T\textit{PPpty}$}} and $T_{\text{daughter}_2}\sqsubseteq$ \record{
  \tfield{cont}{$^T\textit{PPpty}$}}, then
  \begin{quote}
    $T_{\text{mother}}\longrightarrow T_{\text{daughter}_1}\
    T_{\text{daughter}_2}\ \mid\
    T_{\text{daughter}_1}'(_{\text{@}_{\&}}T_{\text{daughter}_2}':{^T\textit{PPpty}}):{^T\textit{PPpty}}$
  \end{quote}
  is
  \begin{quote}
    $T_{\text{mother}}\longrightarrow T_{\text{daughter}_1}\
    T_{\text{daughter}_2}$ \d{\d{$\wedge$}}
    ContForwardApp$_{\text{@}_{\&}}$($T$)
  \end{quote}
  
\end{ex}

Finally, we introduce the English rules for combining common nouns
with relative clauses. First we introduce types $^T\textit{N}$ and
$^T\textit{Rel}$ in \nexteg{}.
\begin{ex} 
\begin{subex} 
 
\item If $T$ is a type, then $^T\textit{N}$ and $^T\textit{Rel}$ are types. 
 
\item $\alpha:{^T\textit{N}}\text{ or }{^T\textit{Rel}}$ iff
  $\alpha:\textit{N}\text{ or }\textit{Rel}$ and $\alpha.\text{cont}:{^T\textit{PPpty}}$ 
 
\end{subex} 
   
\end{ex} 
For any type, $T$, we introduce the constituent structure rule in
\nexteg{}.
\begin{ex} 
$\textit{N}\longrightarrow{^T\textit{N}}\ {^T\textit{Rel}}\ \mid\ {^T\textit{N}}'(_{\text{@}_\&}{^T\textit{Rel}}':{^T\textit{PPpty}}):{^T\textit{PPpty}}$
\end{ex}
  
        



  

\section{Summary of resources introduced}
\label{sec:summresch7}

% This summary does not include the resources for chart processing
% introduced in Section~\ref{sec:chart}.

Items that are new since Chapter~\ref{ch:intensional} are marked
``\textbf{New!}'' and items that have been revised since
Chapter~\ref{ch:intensional} are marked ``\textbf{Revised!}''.  % We have
% included some items for completeness which were not explicitly
% introduced in the text.

\subsection{Universal grammar resources} 

\subsubsection{Types} 

\begin{description}

  \item[\textnormal{\textit{Loc}}] --- \record{\tfield{x-coord}{\textit{Real}}\\
        \tfield{y-coord}{\textit{Real}}\\
        \tfield{z-coord}{\textit{Real}}}

  
\item[\textnormal{\textit{Phon}}] --- a basic type

  $e$ : \textit{Phon} iff $e$ is a phonological event
  
\item[\textnormal{\textit{SEvent}}] --- \record{\tfield{e-loc}{\textit{Loc}} \\
        \tfield{sp}{\textit{Ind}} \\
        \tfield{au}{\textit{Ind}} \\
        \tfield{e}{\textit{Phon}} \\
        \tfield{c$_{\mathrm{loc}}$}{loc(e,e-loc)} \\
        \tfield{c$_{\mathrm{sp}}$}{speaker(e,sp)} \\
        \tfield{c$_{\mathrm{au}}$}{audience(e,au)}} (as in
      Chapter~\ref{ch:infex})

      \item[\textnormal{\textit{Assgnmnt}} Revised!] --- a basic type

      $r:\textit{Assgnmnt}$ iff
$r:\textit{Rec}$ and
$\mathrm{labels}(r)\subset\{\text{x}_0,\text{x}_1,\ldots\}$

\bigskip

If $T$ is \textit{Assgnmnt}$\wedge T'$, $T'$ is a record type and
  $\ell\in\mathrm{labels}(T')$, then
  \begin{enumerate} 
    
  \item if $\mathrm{labels}(T')=\{\ell\}$, $T\ominus\ell=\textit{Assgnmnt}$ 
    
  \item otherwise, $T\ominus\ell= \textit{Assgnmnt}\wedge (T'\ominus\ell/T)$
    
  \end{enumerate}

    
    
  %\end{enumerate}

  

\item[\textnormal{\textit{PropCntxt}} Revised!] --- a basic type

  $r:\textit{PropCntxt}$ iff
$r:\textit{Rec}$ and
$\mathrm{labels}(r)\cap\{\text{x}_0,\text{x}_1,\ldots\}=\emptyset$

\bigskip

If $T$ is \textit{PropCntxt}$\wedge T'$ and
  $\pi\in\mathrm{tpaths}(T')$ then
  \begin{enumerate}
    
  \item if $\pi$ is $\ell$ and $\mathrm{labels}(T')=\{\ell\}$, then $T\ominus\pi=\textit{PropCntxt}$
    
  \item otherwise, $T\ominus\pi= \textit{PropCntxt}\wedge(T'\ominus \pi/T')$
  \end{enumerate}

\item[\textnormal{\textit{Cntxt}} Revised!] --- \record{
    \tfield{$\mathfrak{s}$}{\textit{Assgnmnt}}\\
    \tfield{$\mathfrak{w}$}{\textit{Assgnmnt}}\\
    \tfield{$\mathfrak{g}$}{\textit{Assgnmnt}}\\
      \tfield{$\mathfrak{c}$}{\textit{PropCntxt}}}

        \item[\textnormal{\textit{CntxtType}}] --- a basic type

    $T:\textit{CntxtType}$ iff $T\sqsubseteq\textit{Cntxt}$
      
    % \item[\textnormal{\textit{IndPpty}} New!] ---
    %   (\smallrecord{\smalltfield{x}{\textit{Ind}}}$\rightarrow$\textit{RecType})

      
    % \item[\textnormal{\textit{FramePpty}} New!] ---
    %   (\smallrecord{\smalltfield{x}{\textit{Rec}}}$\rightarrow$\textit{RecType})
      
    \item[\textnormal{\textit{xType}}] --- a basic type

      $T$ : \textit{xType} iff $T$ : \textit{RecType} and $\text{x}\in\mathrm{labels}(T)$

      \item[\textnormal{\textit{Ppty}}] ---
        \record{\tfield{bg}{\textit{xType}}\\
          \tfield{fg}(bg$\rightarrow$\textit{RecType})}

        \begin{description}
        
      \item[purification of properties, \textnormal{$\mathcal{P}(P)$}
          New!]\mbox{}

        If $P$ : \textit{Ppty}, then
\begin{quote}
if $P$.bg$^x$ = $P$.bg, then
\begin{quote}
$\mathfrak{P}(P)=P$
\end{quote}
otherwise:
\begin{quote}
$\mathfrak{P}(P)$ is $\ulcorner\lambda r$:$P$.bg$^{\text{x}}$
. \record{\tfield{$\mathfrak{c}$}{$P.\text{bg}\parallel$ \smallrecord{\field{x}{$r$.x}}}\\
          \tfield{e}{$P(\mathfrak{c})$}}$\urcorner$
\end{quote}
\end{quote}
\item[purification$^\forall$ of properties, \textnormal{$\mathcal{P}^\forall(P)$}
  New!]\mbox{}

  If $P$ : \textit{Ppty}, then
\begin{quote}
if $P$.bg$^x$ = $P$.bg, then
\begin{quote}
$\mathfrak{P^\forall}(P)=P$
\end{quote}
otherwise:
\begin{quote}
$\mathfrak{P^\forall}(P)$ is $\ulcorner\lambda r$:$P$.bg$^{\text{x}}$
. ($(r'\!:\!P.\text{bg}\!\parallel\!\!\text{\smallrecord{\field{x}{$r$.x}}})\rightarrow$
\record{
          \tfield{e}{$P(r')$}})$\urcorner$
\end{quote}
\end{quote}
\item[\textnormal{$P\{a\}$} New!] \mbox{}

  If $P$ is a pure property, $P\{a\}$
  represents the type $P$(\smallrecord{\field{x}{$a$}})

\item[\textnormal{$\mathfrak{T}(P)$} New!] \mbox{}

  If $P$ : \textit{Ppty} and $P$ is pure, then $\mathfrak{T}(P)$ : \textit{Type}.

  $a:\mathfrak{T}(P)$ iff $\mathfrak{P}(P)\{a\}$ is witnessed.
  
\item[\textnormal{exist$^{\text{w}}$($P$)} New!] \mbox{}

  If $P$ : \textit{Ppty}, then exist$^{\text{w}}$($P$) :
  \textit{Type}.

  $X:\text{exist}^{\text{w}}(P)$ iff
\begin{enumerate} 
 
\item $X:\mathrm{set}(\mathfrak{T}(P))$ 
 
\item $|X|=1$

  (equivalently, $p(\mathfrak{T}(X)\|\mathfrak{T}(P))=\frac{1}{|\down{\mathfrak{T}(P)}|}$)
 
\end{enumerate}

\item[\textnormal{exist$_{\text{pl}}^{\text{w}}$($P$)} New!] \mbox{}

  If $P$ : \textit{Ppty}, then exist$_{\text{pl}}^{\text{w}}$($P$) :
  \textit{Type}.

  $X:\text{exist}_{\text{pl}}^{\text{w}}(P)$ iff
\begin{enumerate} 
 
\item $X:\mathrm{set}(\mathfrak{T}(P))$ 
 
\item $|X|\geq 2$

  (equivalently, $p(\mathfrak{T}(X)\|\mathfrak{T}(P))\geq\frac{2}{|\down{\mathfrak{T}(P)}|}$)
 
\end{enumerate}

\item[\textnormal{no$^{\text{w}}$($P$)} New!] \mbox{}

  If $P$ : \textit{Ppty}, then no$^{\text{w}}$($P$) : \textit{Type}.

  $X:\text{no}^{\text{w}}(P)$ iff
\begin{enumerate} 
 
\item $X:\mathrm{set}(\mathfrak{T}(P))$ 
 
\item $|X|=0$


(equivalently, $p(\mathfrak{T}(X)\|\mathfrak{T}(P))=0$)
\end{enumerate}
  equivalently,
\begin{quote}
  $X:\text{no}^{\text{w}}(P)$ iff $X=\emptyset$
\end{quote}

\item[\textnormal{every$^{\text{w}}$($P$)} New!] \mbox{}

  If $P$ : \textit{Ppty}, then every$^{\text{w}}$($P$) :
  \textit{Type}.

  $X:\text{every}^{\text{w}}(P)$ iff
\begin{enumerate} 
 
\item $X:\mathrm{set}(\mathfrak{T}(P))$ 
 
\item $|X|=|\down{\mathfrak{T}(P)}|$

  (equivalently, $p(\mathfrak{T}(X)\|\mathfrak{T}(P))=1$)
 
\end{enumerate}
equivalently,
\begin{quote}
  $X:\text{every}^{\text{w}}(P)$ iff $X=\down{\mathfrak{T}(P)}$
\end{quote}


\item[\textnormal{most$^{\text{w}}$($P$)} New!] \mbox{}

  If $P$ : \textit{Ppty}, then most$^{\text{w}}$($P$) : \textit{Type}.

  $X:\text{most}^{\text{w}}(P)$ iff
\begin{enumerate} 
 
\item $X:\mathrm{set}(\mathfrak{T}(P))$ 
 
\item $\frac{|X|}{|\downP{P}|}\geq\theta_{\text{most}}(P)$, where
  $.5<\theta_{\text{most}}(P)<1$

  (equivalently, $p(\mathfrak{T}(X)\|\mathfrak{T}(P))\geq\theta_{\text{most}}(P)$)
 
\end{enumerate}

\item[\textnormal{many$_a^{\text{w}}$($P$)} New!] \mbox{}

  If $P$ : \textit{Ppty}, then many$_a^{\text{w}}$($P$) :
  \textit{Type}.

  $X:\text{many}_a^{\text{w}}(P)$ iff
\begin{enumerate} 
 
\item $X:\mathrm{set}(\mathfrak{T}(P))$ 
 
\item $|X|\geq\theta_{\text{many}_a}(P)$, where
  $\theta_{\text{many}_a}(P)$ is a natural number, $i$, such that
  $i>2$.

  (equivalently, $p(\mathfrak{T}(X)\|\mathfrak{T}(P))\geq\frac{\theta_{\text{many}_a}(P)}{[\down{\mathfrak{T}(P)}]}$)
 
\end{enumerate}

\item[\textnormal{many$_p^{\text{w}}$($P$)} New!] \mbox{}

  If $P$ : \textit{Ppty}, then many$_p^{\text{w}}$($P$) :
  \textit{Type}.

  $X:\text{many}_p^{\text{w}}(P)$ iff
\begin{enumerate} 
 
\item $X:\mathrm{set}(\mathfrak{T}(P))$ 
 
\item $\frac{|X|}{|\downP{P}|}\geq\theta_{\text{many}_p}(P)$, where
  $0<\theta_{\text{many}_p}(P)<1$

  (equivalently, $p(\mathfrak{T}(X)\|\mathfrak{T}(P))\geq\theta_{\text{many}_p}(P)$)
 
\end{enumerate}

\item[\textnormal{few$_a^{\text{w}}$($P$)} New!] \mbox{}

  If $P$ : \textit{Ppty}, then few$_a^{\text{w}}$($P$) :
  \textit{Type}.

  $X:\text{few}_a^{\text{w}}(P)$ iff
\begin{enumerate} 
 
\item $X:\mathrm{set}(\mathfrak{T}(P))$ 
 
\item $|X|\leq\theta_{\text{few}_a}(P)$, where
  $\theta_{\text{few}_a}(P)$ is a natural number, $i$, such that $i>2$

  (equivalently, $p(\mathfrak{T}(X)\|\mathfrak{T}(P))\leq\frac{\theta_{\text{few}_a}(P)}{[\down{\mathfrak{T}(P)}]}$)
 
\end{enumerate}

\item[\textnormal{few$_p^{\text{w}}$($P$)} New!] \mbox{}

  If $P$ : \textit{Ppty}, then few$_p^{\text{w}}$($P$) :
  \textit{Type}.

  $X:\text{few}_p^{\text{w}}(P)$ iff
\begin{enumerate} 
 
\item $X:\mathrm{set}(\mathfrak{T}(P))$ 
 
\item $\frac{|X|}{|\downP{P}|}\leq\theta_{\text{few}_p}(P)$, where
  $0<\theta_{\text{few}_p}(P)<1$

  (equivalently, $p(\mathfrak{T}(X)\|\mathfrak{T}(P))\leq\theta_{\text{few}_p}(P)$)
 
\end{enumerate}  

\item[\textnormal{a\_few$_a^{\text{w}}$($P$)} New!] \mbox{}

  If $P$ : \textit{Ppty}, then a\_few$_a^{\text{w}}$($P$) :
  \textit{Type}.

  $X:\text{a\_few}_a^{\text{w}}(P)$ iff
\begin{enumerate} 
 
\item $X:\mathrm{set}(\mathfrak{T}(P))$ 
 
\item $|X|\geq\theta_{\text{few}_a}(P)$, where
  $\theta_{\text{few}_a}(P)$ is a natural number, $i$, such that $i>2$

  (equivalently, $p(\mathfrak{T}(X)\|\mathfrak{T}(P))\geq\frac{\theta_{\text{few}_a}(P)}{[\down{\mathfrak{T}(P)}]}$)
 
\end{enumerate}

\item[\textnormal{a\_few$_p^{\text{w}}$($P$)} New!] \mbox{}

  If $P$ : \textit{Ppty}, then a\_few$_p^{\text{w}}$($P$) :
  \textit{Type}.

  $X:\text{a\_few}_p^{\text{w}}(P)$ iff
\begin{enumerate} 
 
\item $X:\mathrm{set}(\mathfrak{T}(P))$ 
 
\item $\frac{|X|}{|\downP{P}|}\geq\theta_{\text{few}_p}(P)$, where
  $0<\theta_{\text{few}_p}(P)<1$

  (equivalently, $p(\mathfrak{T}(X)\|\mathfrak{T}(P))\geq\theta_{\text{few}_p}(P)$)
 
\end{enumerate}  

  
\end{description}

\item[\textnormal{$^T\textit{Ppty}$} New!] --- if $T$ is a type, then
  $^T\textit{Ppty}$ is a type

  $P:{^T\textit{Ppty}}$ iff $P:\textit{Ppty}$ and
  $P.\text{bg}\sqsubseteq$ \smallrecord{
    \smalltfield{x}{$T$}}
        
      \item[\textnormal{\textit{PlPpty}}] --- a basic type

        $P$ : \textit{PlPpty} iff $P$ : \textit{Ppty} and for some type $T$,
$P$.bg $\sqsubseteq$ \smallrecord{\smalltfield{x}{$\mathrm{plurality}(T)$}} 
        
      \item[\textnormal{\textit{PPpty}}] --- \record{\tfield{bg}{\textit{CntxtType}} \\
          \tfield{fg}{(bg$\rightarrow$\textit{Ppty})}}

        
      \item[\textnormal{$^T\textit{PPpty}$} New!] --- if $T$ is a
        type, then $^T\textit{PPpty}$ is a type

        $\mathcal{P}:{^T\textit{PPpty}}$ iff
  $\mathcal{P}:\textit{PPpty}$ and for any $c:\mathcal{P}.\text{bg}$, $\mathcal{P}(c):{^T\textit{Ppty}}$
        
      \item[\textnormal{\textit{Quant}}] ---
        (\textit{Ppty}$\rightarrow$\textit{RecType})
        
      \item[\textnormal{\textit{PQuant}}] --- \record{\tfield{bg}{\textit{CntxtType}} \\
          \tfield{fg}{(bg$\rightarrow$\textit{Quant})}}
        
      \item[\textnormal{\textit{QuantDet}}] ---
        (\textit{Ppty}$\rightarrow$\textit{Quant})
        
      \item[\textnormal{\textit{PQuantDet}}] ---
        \record{
          \tfield{bg}{\textit{CntxtType}}\\
          \tfield{fg}{(bg$\rightarrow$\textit{QuantDet})}}
        
      \item[\textnormal{\textit{PRecType}}] ---
        \record{
          \tfield{bg}{\textit{CntxtType}}\\
          \tfield{fg}{(bg$\rightarrow$\textit{RecType})}}
          

    \item[\textnormal{\textit{Cont}}] --- \textit{PRecType}$\vee$\textit{PPpty}$\vee$\textit{PQuant}$\vee$\textit{PQuantDet}

      
    \item[\textnormal{\textit{Cat}}] --- a basic type

      s, np, det, n, v, vp : \textit{Cat}

    
    \item[\textnormal{\textit{Syn}}] ---  \record{\tfield{cat}{\textit{Cat}} \\
        \tfield{daughters}{\textit{Sign}$^*$}} 
 


  
    \item[\textnormal{\textit{Sign}}] ---  a basic type

      $\sigma$ : \textit{Sign} iff $\sigma$ :
      \record{\tfield{s-event}{\textit{SEvent}} \\
         \tfield{syn}{\textit{Syn}} \\
        \tfield{cont}{\textit{Cont}}} 

  
\item[\textnormal{\textit{SignType}}] --- a basic type

  $T:\textit{SignType}$ iff $T\sqsubseteq\textit{Sign}$ 

  
\item[\textnormal{\textit{S}}] --- 
  \smallrecord{
    \footnotesize{\textit{Sign}}\\
    \smalltfield{syn}{\smallrecord{\smallmfield{cat}{s}{\textit{Cat}}}}})
  
\item[\textnormal{\textit{S}/$i$} New!] --- if $i$ is a natural
  number, then \textit{S}/$i$ is a type

  $\alpha:\textit{S}/i$ iff $\alpha:\textit{S}$ and $\alpha.\text{cont}.\text{bg}\sqsubseteq$\smallrecord{
    \smalltfield{$\mathfrak{g}$}{\smallrecord{
        \smalltfield{x$_i$}{\textit{Ind}}}}} 
  
  
\item[\textnormal{\textit{NP}}] --- 
  \smallrecord{
    \footnotesize{\textit{Sign}}\\
    \smalltfield{syn}{\smallrecord{\smallmfield{cat}{np}{\textit{Cat}}}}}
  
\item[\textnormal{\textit{whNP}} New!] --- a basic type

  $\sigma$ : \textit{WhNP} iff $\sigma$ : \textit{NP}, $\sigma$.cont is $\mathcal{Q}$ and
$\mathcal{Q}.\text{bg}\sqsubseteq$\smallrecord{
  \smalltfield{$\mathfrak{w}$}{\smallrecord{
      \smalltfield{x$_i$}{\textit{Ind}}}}}, for some natural number
$i$.

\item[\textnormal{\textit{NP}$_{\text{wh}_i}$} New!] --- if $i$ is a
  natural number, then \textit{NP}$_{\text{wh}_i}$ is a type

  $\alpha:\textit{NP}_{\text{wh}_i}$ iff $\alpha:\textit{NP}$ and
  $\alpha.\text{cont}.\text{bg}\sqsubseteq$\smallrecord{
    \smalltfield{$\mathfrak{w}$}{\smallrecord{
        \smalltfield{x$_i$}{\textit{Ind}}}}}

  
\item[\textnormal{\textit{Det}}] --- 
  \smallrecord{
    \footnotesize{\textit{Sign}}\\
\smalltfield{syn}{\smallrecord{\smallmfield{cat}{det}{\textit{Cat}}}}}
  
\item[\textnormal{\textit{N}}] --- 
  \smallrecord{
    \footnotesize{\textit{Sign}}\\
    \smalltfield{syn}{\smallrecord{\smallmfield{cat}{n}{\textit{Cat}}}}}
  
\item[\textnormal{$^T\textit{N}$} New!] --- if $T$ is a type, then
  $^T\textit{N}$ is a type

  $\alpha:{^T\textit{N}}$ iff
  $\alpha:\textit{N}$ and $\alpha.\text{cont}:{^T\textit{PPpty}}$
  
\item[\textnormal{\textit{V}}] --- 
  \smallrecord{
    \footnotesize{\textit{Sign}}\\
    \smalltfield{syn}{\smallrecord{\smallmfield{cat}{v}{\textit{Cat}}}}}
  
  
\item[\textnormal{\textit{VP}}] --- 
  \smallrecord{
    \footnotesize{\textit{Sign}}\\
    \smalltfield{syn}{\smallrecord{\smallmfield{cat}{vp}{\textit{Cat}}}}}

\item[\textnormal{\textit{Rel}} New!] --- 
  \smallrecord{
    \footnotesize{\textit{Sign}}\\
    \smalltfield{syn}{\smallrecord{\smallmfield{cat}{rel}{\textit{Cat}}}}}

  
\item[\textnormal{$^T\textit{Rel}$} New!] --- if $T$ is a type, then
  $^T\textit{Rel}$ is a type

  $\alpha:{^T\textit{Rel}}$ iff
  $\alpha:\textit{Rel}$ and $\alpha.\text{cont}:{^T\textit{PPpty}}$
  
\item[\textnormal{\textit{NoDaughters}}] ---
  \smallrecord{\smalltfield{syn}{\smallrecord{\smallmfield{daughters}{$\varepsilon$}{\textit{Sign}$^*$}}}}

  
\item[\textnormal{\textit{Real}}] --- a basic type

  $n$ : \textit{Real} iff $n$ is a real number

  
\item[\textnormal{\textit{Card}}] --- a basic type

  $n$ : \textit{Card} iff $n$ is a cardinal number (natural numbers
  with the addition of $\aleph_0, \aleph_1,\ldots$)
 

  

\item[\textnormal{\textit{AmbTempFrame}}] --- \record{\tfield{x}{\textit{Real}} \\
        \tfield{loc}{\textit{Loc}} \\
        \tfield{e}{temp(loc, x)}}

      
    \item[\textnormal{\textit{TempRiseEventCntxt}}] ---
      \record{
        \tfield{fix}{\record{
            \tfield{loc}{\textit{Loc}}}}\\
        \tfield{scale}{(\textit{AmbTempFrame}
          $\rightarrow$ \textit{Real})}}
      
    \item[\textnormal{\textit{TempRiseEvent}}] ---
      
      $\lambda r$:\textit{TempRiseEventCntxt} .\\  
\hspace*{2em}\record{\tfield{e}{(\textit{AmbTempFrame}$\parallel$$r$.fix)$^2$}\\
        \tfield{c$_{\mathrm{rise}}$}{$r$.scale(e[0]) $<$
          $r$.scale(e[1])}}
      
    \item[\textnormal{\textit{PriceFrame}}] --- \record{\tfield{x}{\textit{Real}} \\
        \tfield{loc}{\textit{Loc}} \\
        \tfield{commodity}{\textit{Ind}} \\
        \tfield{e}{price(commodity, loc, x)}}
      
    \item[\textnormal{\textit{PriceRiseEventCntxt}}] --- \record{
        \tfield{fix}{\record{
            \tfield{loc}{\textit{Loc}}\\
            \tfield{commodity}{\textit{Ind}}}}\\
        \tfield{scale}{(\textit{PriceFrame}
                             $\rightarrow$ \textit{Real})}}
 
  \item[\textnormal{\textit{PriceRiseEvent}}] --- \mbox{}

   $\lambda
r$:\textit{TempRiseEventCntxt} .\\  
\hspace*{2em}\record{\tfield{e}{(\textit{PriceFrame}$\parallel$$r$.fix)$^2$}\\
        \tfield{c$_{\mathrm{rise}}$}{$r$.scale(e[0]) $<$
          $r$.scale(e[1])}}
      
    \item[\textnormal{\textit{LocFrame}}] --- \record{\tfield{x}{\textit{Ind}} \\
        \tfield{loc}{\textit{Loc}} \\
        \tfield{e}{at(x, loc)}}
      
    \item[\textnormal{\textit{LocRiseEventCntxt}}] ---
      \record{\tfield{fix}{\record{\tfield{x}{\textit{Ind}}
                                               }}\\
                         \tfield{scale}{(\textit{LocFrame}
                           $\rightarrow$ \textit{Real})}}
                       
 \item[\textnormal{\textit{LocRiseEvent}}] ---

   $\lambda
r$:\textit{LocRiseEventCntxt} .\\  
\hspace*{2em}\record{\tfield{e}{(\textit{LocFrame}$\parallel$$r$.fix)$^2$}\\
        \tfield{c$_{\mathrm{rise}}$}{$r$.scale(e[0]) $<$
          $r$.scale(e[1])}}

      
    \item[\textnormal{\textit{Topos}}] --- a basic type

      If $\tau:\textit{Topos}$, then $\tau$ : \record{\tfield{bg}{\textit{Type}}\\
        \tfield{fg}{(bg$\rightarrow$\textit{Type})}} 

                       


\end{description}

   \subsubsection{Predicates} 

\begin{description}

 \item[with arity \textnormal{$\langle$\textit{Phon},
    \textit{Loc}$\rangle$}] \mbox{}
  
    \begin{description}

    \item[\textnormal{loc}] --- $e$ : loc($u$, $l$) iff $u$ is located
      at $l$ in $e$

    \end{description}
    
  \item[with arity \textnormal{$\langle$\textit{Phon},
      \textit{Ind}$\rangle$}] \mbox{}

    \begin{description}

    \item[\textnormal{speaker}] --- $e$ : speaker($u$, $a$) iff $u$
        is the speaker of $u$ in $e$

    \item[\textnormal{audience}] --- $e$ : audience($u$, $a$) iff
        $u$ is the audience of $u$ in $e$

      \end{description}

    \item[with arity \textnormal{$\langle\textit{Card}\rangle$}] \mbox{}

  \begin{description}
    
  \item[\textnormal{card}] --- $X$ : card($n$) iff for some $T$,
    $X:\mathrm{set}(T)$ and $|X|=n$
    
  \item[\textnormal{card\_at\_least}] --- $X$ : card\_at\_least($n$) iff for some $T$, $X:\mathrm{set}(T)$
    and $|X|\geq n$

    
  \item[\textnormal{card\_at\_most}] --- $X$ : card\_at\_most($n$) iff for some $T$, $X:\mathrm{set}(T)$
    and $|X|\leq n$

  \end{description}
      
  \item[with arity \textnormal{$\langle$\textit{Ppty}$\rangle$}]
    \mbox{}

    \begin{description}
      
    \item[\textnormal{unique}] --- $s:\textrm{unique}(P)$ iff
      $\mid\!\downP{P\!\restriction\!s}\!\mid = 1$

    \end{description}

    \item[with arity \textnormal{$\langle\textit{Ppty},\textit{Ppty}\rangle$}] \mbox{}

  \begin{description}
    
  \item[\textnormal{exist} Revised!] \mbox{}
    \begin{description}
      
    \item[general witness condition] \mbox{}

      $s:\text{exist}(P,Q)$ iff $s$ :
      \record{\tfield{X}{exist$^w(P)$}\\
        \tfield{f}{$((a:\mathfrak{T}(\text{X}))\rightarrow\mathfrak{P}(Q)\{a\})$}}

      
    \item[particular witness condition] \mbox{}

      $s:\text{exist}(P,Q)$ iff $s$ :
  \record{\tfield{x}{$\mathfrak{T}(P)$}\\
        \tfield{e}{$\mathfrak{P}(Q)$\{x\}}}

    \end{description}

    % $s$ : exist($P$,$Q$) iff
     % $\downP{P}\cap\downP{Q\!\restriction\! s}\not=\emptyset$
    % $s$ : exist($P$,$Q$) iff
    % $\downP{P\!\restriction\!s}\cap\downP{Q|_{\mathcal{F}(P.\mathrm{fg})}\!\restriction\!s}\not=\emptyset$

    
  \item[\textnormal{exist$_\text{pl}$} New!] \mbox{}

    \begin{description}
      
    \item[general witness condition] \mbox{}

      $s:\text{exist}_{\text{pl}}(P,Q)$ iff $s$ :
  \record{\tfield{X}{exist$_{\text{pl}}^w(P)$}\\
    \tfield{f}{$((a:\mathfrak{T}(\text{X}))\rightarrow\mathfrak{P}(Q)\{a\})$}}

\end{description}

\item[\textnormal{no} New!] \mbox{}

  \begin{description}
    
  \item[general witness condition] \mbox{}

    $s:\text{no}(P,Q)$ iff $s$ :
    \record{\tfield{X}{$\text{no}^w(P)$}\\
      \tfield{f}{($(a:(\mathfrak{T}(P)\wedge\mathfrak{T}(Q)))\rightarrow$
        \record{\mfield{x}{$a$}{$\mathfrak{T}$(X)}})}}
    
  \item[particular witness condition] \mbox{}

    $s:\text{no}(P,Q)$ iff $s$ :
    \record{\tfield{X}{$\text{every}^w(P)$}\\
      \tfield{f}{$((x:\mathfrak{T}(X))\rightarrow\neg\mathfrak{P}(Q)\{x\})$}}

  \end{description}

        
    
\item[\textnormal{every} Revised!] \mbox{}
  % $s$ : every($P$,$Q$) iff
  % $\downP{P}\subseteq\downP{Q\!\restriction\!s}$

  \begin{description}

    
  \item[general witness condition] \mbox{}

    $s:\text{every}(P,Q)$ iff $s$ :
  \record{\tfield{X}{$\text{every}^w(P)$}\\
          \tfield{f}{$((a:\mathfrak{T}(\text{X}))\rightarrow\mathfrak{P}(Q)\{a\})$}}

      \end{description}

      
    \item[\textnormal{most} New!] \mbox{}

      \begin{description}
        
      \item[general witness condition] \mbox{}

        $s:\text{most}(P,Q)$ iff $s$ :
  \record{\tfield{X}{$\text{most}^w(P)$}\\
    \tfield{f}{$((a:\mathfrak{T}(\text{X}))\rightarrow\mathfrak{P}(Q)\{a\})$}}

\end{description}

\item[\textnormal{many$_a$} New!] \mbox{}

  \begin{description}
    
  \item[general witness condition] \mbox{}

    $s:\text{many}_a(P,Q)$ iff $s$ :
  \record{\tfield{X}{$\text{many}_a^w(P)$}\\
    \tfield{f}{$((a:\mathfrak{T}(\text{X}))\rightarrow\mathfrak{P}(Q)\{a\})$}}

\end{description}

\item[\textnormal{many$_p$} New!] \mbox{}

  \begin{description}

    
  \item[general witness condition] \mbox{}

    $s:\text{many}_p(P,Q)$ iff $s$ :
  \record{\tfield{X}{$\text{many}_p^w(P)$}\\
    \tfield{f}{$((a:\mathfrak{T}(\text{X}))\rightarrow\mathfrak{P}(Q)\{a\})$}}

\end{description}

\item[\textnormal{few$_a$} New!] \mbox{}

  \begin{description}

    
  \item[general witness condition] \mbox{}

    $s:\text{few}_a(P,Q)$ iff $s$ :
  \record{\tfield{X}{$\text{few}_a^w(P)$}\\
          \tfield{f}{($(a:(\mathfrak{T}(P)\wedge\mathfrak{T}(Q)))\rightarrow$
            \record{\mfield{x}{$a$}{$\mathfrak{T}$(X)}})}}
        
      \item[particular witness condition] \mbox{}

        $s:\text{few}_a(P,Q)$ iff $s$ :
  \record{\tfield{X}{$\overline{\text{few}_a^w(P)}$}\\
    \tfield{f}{$((x:\mathfrak{T}(X))\rightarrow\neg\mathfrak{P}(Q)\{x\})$}}
  
      \end{description}

      
    \item[\textnormal{few$_p$} New!] \mbox{}

      \begin{description}
        
      \item[general witness condition] \mbox{}

        $s:\text{few}_p(P,Q)$ iff $s$ :
  \record{\tfield{X}{$\text{few}_p^w(P)$}\\
          \tfield{f}{($(a:(\mathfrak{T}(P)\wedge\mathfrak{T}(Q)))\rightarrow$
            \record{\mfield{x}{$a$}{$\mathfrak{T}$(X)}})}}

        
      \item[particular witness condition] \mbox{}

        $s:\text{few}_p(P,Q)$ iff $s$ :
  \record{\tfield{X}{$\overline{\text{few}_p^w(P)}$}\\
          \tfield{f}{$((x:\mathfrak{T}(X))\rightarrow\neg\mathfrak{P}(Q)\{x\})$}}

      \end{description}

      
    \item[\textnormal{a\_few$_a$} New!] \mbox{}

      \begin{description}


       
      \item[general witness condition] \mbox{}

        $s:\text{a\_few}_a(P,Q)$ iff $s$ :
  \record{\tfield{X}{$\text{a\_few}_a^w(P)$}\\
    \tfield{f}{$((a:\mathfrak{T}(\text{X}))\rightarrow\mathfrak{P}(Q)\{a\})$}}

\end{description}

\item[\textnormal{a\_few$_p$} New!] \mbox{}

  \begin{description}
    
  \item[general witness condition] \mbox{}

    $s:\text{a\_few}_p(P,Q)$ iff $s$ :
  \record{\tfield{X}{$\text{a\_few}_p^w(P)$}\\
    \tfield{f}{$((a:\mathfrak{T}(\text{X}))\rightarrow\mathfrak{P}(Q)\{a\})$}}

\end{description}


      
  \end{description}

  
\item[with arity
  \textnormal{$\langle\textit{PlPpty},\textit{PlPpty}\rangle$}] \mbox{}
  
\begin{description}
    
\item[\textnormal{exactly\_$n$}] --- for $n$ a natural number,

  $s$ : exactly\_$n$($P$, $Q$) iff $s$ : at\_least\_$n$($P$, $Q$)$\wedge$at\_most\_$n$($P$, $Q$)

    % $s$ : exactly\_$n$($P$, $Q$) iff
    %       $\down{\mathcal{F}((Q\!\restriction\!        s).\text{fg}\mid_{\mathcal{F}((P\restriction s).\text{fg})})
    %     \text{ \d{$\wedge$} \smallrecord{\smalltfield{x}{card($n$)}}}}
    %   \not=\emptyset$

      
    \item[\textnormal{at\_least\_$n$}] --- for $n$ a natural
      number,

      $s$ : at\_least\_$n$($P$, $Q$) iff
          $\down{\mathcal{F}((Q\!\restriction\!        s).\text{fg}\mid_{\mathcal{F}(P.\text{fg})})
        \text{ \d{$\wedge$} \smallrecord{\smalltfield{x}{card\_at\_least($n$)}}}}
      \not=\emptyset$

      % $s$ : at\_least\_$n$($P$, $Q$) iff
      %     $\down{\mathcal{F}((Q\!\restriction\!        s).\text{fg}\mid_{\mathcal{F}((P\restriction s).\text{fg})})
      %   \text{ \d{$\wedge$} \smallrecord{\smalltfield{x}{card\_at\_least($n$)}}}}
      % \not=\emptyset$

      
    \item[\textnormal{at\_most\_$n$}] --- for $n$ a natural
      number,

      $s$ : at\_most\_$n$($P$, $Q$) iff
          $r:\mathcal{F}((Q\!\restriction\!        s).\text{fg}\mid_{\mathcal{F}(P.\text{fg})})
        \text{ implies } r:\text{ \smallrecord{\smalltfield{x}{card\_at\_most($n$)}}}$

      % $s$ : at\_most\_$n$($P$, $Q$) iff
      %     $r:\mathcal{F}((Q\!\restriction\!        s).\text{fg}\mid_{\mathcal{F}((P\restriction s).\text{fg})})
      %   \text{ implies } r:\text{ \smallrecord{\smalltfield{x}{card\_at\_most($n$)}}}$

\end{description}    

  
\item[with arity \textnormal{\{$\langle T\rangle\mid T$ is a type\}}]
  \mbox{}

  \begin{description}
    
  \item[\textnormal{be}] --- $e:\text{be}(a)$ iff $a\varepsilon e$

  \end{description}

  
\item[with arity
  \textnormal{$\langle\textit{Loc},\textit{Real}\rangle$}] \mbox{}
  \begin{description}
    
  \item[\textnormal{temp}] --- $e:\text{temp}(l,n)$ iff $n$ is
    the temperature at $l$ in $e$.

    
  

  \end{description}
  
\item[with arity
  \textnormal{$\langle\textit{Real},\textit{Real}\rangle$}] \mbox{}

  \begin{description}
    
  \item[\textnormal{less-than}] --- $e$ : less-than($n$, $m$) iff $n\varepsilon e$, $m\varepsilon e$ and $n<m$

  \end{description}

\item[with arity
  \textnormal{$\langle\textit{Type},\textit{Type},\textit{Topos}\rangle$}]
  \mbox{}

  \begin{description}

    
  \item[\textnormal{nec}] ---

    If $\mathbb{T}$ is a modal type system and $p\in\mathbb{T}$, then
    \begin{quote}
      $s:_p\mathrm{nec}(T,B,\tau)$ iff $s:_pB$, 
      $B\sqsubseteq_{\mathbb{T}}\tau.\mathrm{bg}$ and 
      $\tau(s)\sqsubseteq_{\mathbb{T}}T$
    \end{quote}

    
  \item[\textnormal{poss}] ---

    If $\mathbb{T}$ is a modal type system and $p\in\mathbb{T}$, then
    \begin{quote}
      $s:_p\mathrm{poss}(T,B,\tau)$ iff $s:_pB$, 
      $B\sqsubseteq_{\mathbb{T}}\tau.\mathrm{bg}$ and 
      $\tau(s)\top_{\mathbb{T}}T$
    \end{quote}

  \end{description}

  
\item[with arity
  \textnormal{$\langle\textit{RecType},\textit{RecType}\rangle$}] \mbox{}

  \begin{description}
    
  \item[\textnormal{pov}
    ] --- $e:\text{pov}(T_1,T_2)$ iff $T_2$
    is a point of view on $T_1$ in $e$.

    $e:\text{pov}(T_1,T_2)$ implies
    $\mathrm{labels}(T_2)\subseteq\mathrm{labels(T_1)}$

  \end{description}

  
\item[with arity
  \textnormal{$\langle\textit{Ind},\textit{RecType}\rangle$}] \mbox{}

  \begin{description}
    
  \item[\textnormal{ltm}] --- $e:\text{ltm}(a,T)$ iff $T$ is $a$'s
    long term memory in $e$.
    
  \item[\textnormal{rbelieve}] --- $e:\text{rbelieve}(a,T)$ iff
    $T$ is $a$'s religious beliefs in $e$.

    
  \item[\textnormal{des}] --- $e:\text{des}(a,T)$ iff $T$ is
    $a$'s desires in $e$.

  \end{description}
  
  

  
  
  


\end{description}

\subsubsection{Properties}

\begin{description}
  
\item[\textnormal{$P_1\&P_2$} New!] \mbox{}

  If $T$ is a type, $P_1:{^T\textit{Ppty}}$ and $P_2:{^T\textit{Ppty}}$,
then \textit{the conjunction of $P_1$ and
  $P_2$}, $P_1\&P_2$, is
\begin{quote}
  $\ulcorner\lambda r$:\smallrecord{
    \smalltfield{x}{$T$}} .
  \record{
    \tfield{e$_1$}{$P_1\{r.\text{x}\}$}\\
    \tfield{e$_2$}{$P_2\{r.\text{x}\}$}}$\urcorner$
\end{quote}

\end{description}

\subsubsection{Scales} (as in Chapter~\ref{ch:commonnouns})

% % \begin{description}
  
% % \item[\textnormal{$\zeta_{\text{temp}}$} New!] ---
% %   $\lambda r$:\textit{AmbTempFrame} . $r$.x : (\textit{AmbTempFrame}
% %   $\rightarrow$ \textit{Real})

  
% % \item[\textnormal{$\zeta_{\mathrm{height}}$} New!] ---
% %   $\lambda r$:\textit{LocFrame} . $r$.loc.z-coord : (\textit{LocFrame}
% %   $\rightarrow$ \textit{Real})

  
% % \item[\textnormal{$\zeta_{\text{age}}$} New!] ---  
% % $\lambda r$:\smallrecord{\smalltfield{x}{\textit{Ind}}\\
% %                          \smalltfield{age}{\textit{Real}}\\
% %                          \smalltfield{c$_{\mathrm{age}}$}{age\_of(x,age)}}
% %                        . $r$.age : (\smallrecord{\smalltfield{x}{\textit{Ind}}\\
% %                          \smalltfield{age}{\textit{Real}}\\
% %                          \smalltfield{c$_{\mathrm{age}}$}{age\_of(x,age)}}
% %                        $\rightarrow$ \textit{Real})

% % \end{description}



\subsubsection{Lexicon} 
\begin{description}
\item[\textnormal{Lex}] \mbox{}

  If $T_{\mathrm{phon}}$ is a phonological type (that is,
$T_{\mathrm{phon}}\sqsubseteq\textit{Phon}$) and $T_{\mathrm{sign}}$
is a sign type (that is, $T_{\mathrm{sign}}\sqsubseteq\textit{Sign}$), then we shall use
Lex($T_{\mathrm{phon}}$, $T_{\mathrm{sign}}$) to represent
\begin{quote}
(($T_{\mathrm{sign}}$ \d{$\wedge$}
\smallrecord{\smalltfield{s-event}{\smallrecord{\smalltfield{e}{$T_{\mathrm{phon}}$}}}})
\d{$\wedge$} \textit{NoDaughters})
\end{quote}

% \item[\textnormal{SemCommonNoun($p$)}] \mbox{}

%   If $p$ is a predicate with arity $\langle\textit{Ind}\rangle$, then SemCommonNoun($p$) is
%   \begin{quote}
%     $\lambda c$:\textit{Rec} . $\lambda
% r$:\smallrecord{\smalltfield{x}{\textit{Ind}}}
% . \record{\tfield{e}{$p$($r$.x)}}
% \end{quote}

% \item[\textnormal{Lex$_{\mathrm{CommonNoun}}$($T_{\mathrm{phon}}$,
%     $p$)}] \mbox{}

%   If $T_{\mathrm{phon}}$ is a phonological type and $p$ is a
%   predicate with arity $\langle\textit{Ind}\rangle$, then Lex$_{\mathrm{CommonNoun}}$($T_{\mathrm{phon}}$,
%   $p$) is
%   \begin{quote}
%     Lex($T_{\mathrm{phon}}$, \textit{N}) \d{$\wedge$}
%     \smallrecord{\smallmfield{cont}{SemCommonNoun($p$)}{\textit{PPpty}}}
%   \end{quote}

\item[\textnormal{SemCommonNoun($T_{\mathrm{bg}}$, $p$)}]
  \mbox{}

    If $p$ is a predicate with arity $\langle\textit{Ind}\rangle$ and
    $T_{\mathrm{bg}}$ is a type (of context), then
    SemCommonNoun($T_{\mathrm{bg}}$, $p$) is
  \begin{quote}
    $\ulcorner\lambda c$:$T_{\mathrm{bg}}$ . $\ulcorner\lambda
r$:\smallrecord{\smalltfield{x}{\textit{Ind}}}
. \record{\tfield{e}{$p$($r$.x)}}$\urcorner\urcorner$
\end{quote}

If $p$ is a predicate with arity $\langle\textit{Rec}\rangle$ and $T_{\mathrm{bg}}$ is a type (of context), then
    SemCommonNoun($T_{\mathrm{bg}}$, $p$) is
  \begin{quote}
    $\ulcorner\lambda c$:$T_{\mathrm{bg}}$ . $\ulcorner\lambda
r$:\smallrecord{\smalltfield{x}{\textit{Rec}}}
. \record{\tfield{e}{$p$($r$.x)}}$\urcorner\urcorner$
\end{quote}
  
%     \todo{Not sure this is used}If $p$ is a predicate with arity $\langle\textit{Rec},
%     \textit{Rec}\rangle$ and $T_{\mathrm{bg}}\sqsubseteq$\smallrecord{\smalltfield{$\mathfrak{c}$}{\textit{Rec}}} is a type (of context), then
%     SemCommonNoun($T_{\mathrm{bg}}$, $p$) is
%   \begin{quote}
%     $\lambda c$:$T_{\mathrm{bg}}$ . $\lambda
% r$:\textit{Rec}
% . \record{\tfield{e}{$p$($r$, $c.\mathfrak{c}$)}}
% \end{quote}

\item[\textnormal{Lex$_{\mathrm{CommonNoun}}$($T_{\mathrm{phon}}$,
    $T_{\mathrm{bg}}$, $p$)}] \mbox{}

    % If $T_{\mathrm{phon}}$ is a phonological type, $p$ is a
  % predicate with arity $\langle\textit{Ind}\rangle$ and
  % $T_{\mathrm{bg}}$ is a type (of context), then
  % Lex$_{\mathrm{CommonNoun}}$($T_{\mathrm{phon}}$, $T_{\mathrm{bg}}$,
  % $p$) is
  % \begin{quote}
  %   Lex($T_{\mathrm{phon}}$, \textit{N}) \d{$\wedge$}
  %   \smallrecord{\smallmfield{cont}{SemCommonNoun($T_{\mathrm{bg}}$,
  %       $p$)}{\textit{PPpty}}}
  % \end{quote}


  If $T_{\mathrm{phon}}$ is a phonological type, $p$ is a
  predicate with arity $\langle\textit{Ind}\rangle$ or $\langle\textit{Rec}\rangle$ and
  $T_{\mathrm{bg}}$ is a type (of context), then
  Lex$_{\mathrm{CommonNoun}}$($T_{\mathrm{phon}}$, $T_{\mathrm{bg}}$,
  $p$) is
  \begin{quote}
    Lex($T_{\mathrm{phon}}$, \textit{N}) \d{$\wedge$}
    \smallrecord{\smallmfield{cont}{SemCommonNoun($T_{\mathrm{bg}}$,
        $p$)}{\textit{PPpty}}}
  \end{quote}
  
\item[\textnormal{SemPropName($T_{\text{phon}}$)}] \mbox{}

  If $T_{\text{phon}}$ is a phonological type, then SemPropName($T_{\text{phon}}$) is
  \begin{quote}
    $\ulcorner\lambda c$:\smallrecord{
      \footnotesize{\textit{Cntxt}}\\
      \smalltfield{$\mathfrak{c}$}{\smallrecord{\smalltfield{x}{\textit{Ind}}\\
                         \smalltfield{e}{named(x, $T_{\mathrm{phon}}$)}}}} . $\lambda
                       P$:\textit{Ppty} . $P(c.\mathfrak{c})\urcorner$
  \end{quote}
  
\item[\textnormal{Lex$_{\mathrm{PropName}}$($T_{\mathrm{phon}}$
    )}] \mbox{}

  If $T_{\mathrm{phon}}$ is a phonological type,

  then Lex$_{\mathrm{PropName}}$($T_{\mathrm{phon}}$) is
  \begin{quote}
    Lex($T_{\mathrm{phon}}$, \textit{NP}) \d{$\wedge$}
\smallrecord{\smallmfield{cnt}{SemPropName($T_{\mathrm{phon}}$)}{\textit{PQuant}}}
\end{quote}

\item[\textnormal{SemPron} ] \mbox{}

  $\ulcorner\lambda c$:\smallrecord{
    \footnotesize{\textit{Cntxt}}\\
    \smalltfield{$\mathfrak{s}$}{\smallrecord{
        \smalltfield{x$_0$}{\textit{Ind}}}}} . $\lambda
  P$:\textit{Ppty}
  . $P$(\smallrecord{\field{x}{$c.\mathfrak{s}$.x$_0$}})$\urcorner$

\item[\textnormal{LexPron($T_{\text{phon}}$)}] \mbox{}

If $T_{\text{phon}}$ is a phonological type, then
LexPron($T_{\text{phon}}$) is
\begin{quote}
Lex($T_{\mathrm{phon}}$, \textit{NP}) \d{$\wedge$}
\smallrecord{\smallmfield{cont}{SemPron}{\textit{PQuant}}}
\end{quote}

\item[\textnormal{SemWhPron} New!] \mbox{}

  $\ulcorner\lambda c$:\smallrecord{
  \footnotesize{\textit{Cntxt}}\\
  \smalltfield{$\mathfrak{w}$}{\smallrecord{
      \smalltfield{x$_0$}{\textit{Ind}}}}}
. $\lambda P$:\textit{Ppty}
. $P$(\smallrecord{\field{x}{$c.\mathfrak{w}.\text{x}_0$}})$\urcorner$

\item[\textnormal{LexWhPron($T_{\text{phon}}$)} New!] \mbox{}

  If $T_{\text{phon}}$ is a phonological type, then
LexWhPron($T_{\text{phon}}$) is
\begin{quote}
Lex($T_{\mathrm{phon}}$, \textit{NP}) \d{$\wedge$}
\smallrecord{\smallmfield{cont}{SemWhPron}{\textit{PQuant}}}
\end{quote}

\item[\textnormal{SemNumeral($n$)}] \mbox{}

  If $n$ is a real number, then SemNumeral($n$) is
  \begin{quote}
    $\ulcorner\lambda c$:\textit{Cntxt} . $\lambda P$:\textit{Ppty}
    . $P$(\smallrecord{\field{x}{$n$}})$\urcorner$
  \end{quote}

  
\item[\textnormal{Lex$_{\mathrm{numeral}}$($T_{\mathrm{phon}}$, $n$)}] \mbox{}

    If $T_{\mathrm{phon}}$ is a phonological type and $n$ is a real
    number, then Lex$_{\mathrm{numeral}}$($T_{\mathrm{phon}}$, $n$) is
    \begin{quote}
      Lex($T_{\mathrm{phon}}$, \textit{NP}) \d{$\wedge$}
      \smallrecord{\smallmfield{cnt}{SemNumeral($n$)}{\textit{PQuant}}}
    \end{quote}
    

  
\item[\textnormal{SemIndefArt}] \mbox{}

  % $\ulcorner\lambda c$:\textit{Rec} . \\
% \hspace*{1em}$\lambda Q$:\textit{Ppty} . \\
% \hspace*{2em} $\lambda P$:\textit{Ppty}
% . \record{\mfield{restr}{$Q$}{\textit{Ppty}} \\
%           \mfield{scope}{$P$}{\textit{Ppty}} \\
%           \tfield{e}{exist(restr, scope)}}$\urcorner$

$\lambda Q$:\textit{Ppty} . \\
  \hspace*{1em}$\ulcorner\lambda c$:\textit{Cntxt} . \\
  \hspace*{2em}$\lambda P$:\textit{Ppty} . \\
  \hspace*{3em}\record{
    \mfield{restr}{$Q$}{\textit{Ppty}}\\
    \mfield{scope}{$P|_{\mathfrak{F}(\text{restr})}$}{\textit{Ppty}}\\
    \tfield{e}{exist(restr, scope)}}$\urcorner$



 

        
      \item[\textnormal{Lex$_{\mathrm{IndefArt}}$($T_{\mathrm{Phon}}$)}]
        \mbox{}

        If $T_{\mathrm{Phon}}$ is a phonological type, then
        Lex$_{\mathrm{IndefArt}}$($T_{\mathrm{Phon}}$) is
        \begin{quote}
          Lex($T_{\mathrm{Phon}}$, \textit{Det}) \d{$\wedge$}
          \smallrecord{\smallmfield{cont}{SemIndefArt}{(\textit{Ppty}$\rightarrow$\textit{PQuant})}}
        \end{quote}

        
      \item[\textnormal{SemUniversal}] \mbox{}

               $\lambda Q$:\textit{Ppty} . \\
  \hspace*{1em}$\ulcorner\lambda c$:\textit{Cntxt} . \\
  \hspace*{2em}$\lambda P$:\textit{Ppty} . \\
  \hspace*{3em}\record{
    \mfield{restr}{$Q$}{\textit{Ppty}}\\
    \mfield{scope}{$P|_{\mathfrak{F}(\text{restr})}$}{\textit{Ppty}}\\
    \tfield{e}{every(restr, scope)}}$\urcorner$

 

  
\item[\textnormal{Lex$_{\mathrm{Universal}}$($T_{\mathrm{Phon}}$)}]
        \mbox{}

        If $T_{\mathrm{Phon}}$ is a phonological type, then
        Lex$_{\mathrm{Universal}}$($T_{\mathrm{Phon}}$) is
        \begin{quote}
          Lex($T_{\mathrm{Phon}}$, \textit{Det}) \d{$\wedge$}
          \smallrecord{\smallmfield{cont}{SemUniversal}{(\textit{Ppty}$\rightarrow$\textit{PQuant})}}
        \end{quote}

        \item[\textnormal{SemDefArt}] \mbox{}

 %  $\lambda c$:\textit{Rec} . \\
% \hspace*{1em}$\lambda Q$:\textit{Ppty} . \\
% \hspace*{2em} $\lambda P$:\textit{Ppty}
% . \record{\mfield{restr}{$Q$}{\textit{Ppty}} \\
%           \mfield{scope}{$P$}{\textit{Ppty}} \\
%           \tfield{e}{the(restr, scope)}}

                    $\lambda Q$:\textit{Ppty} . \\
                    \hspace*{1em}$\ulcorner\lambda c$:\smallrecord{
                      \footnotesize{\textit{Cntxt}}\\
    \smalltfield{$\mathfrak{c}$}{\smallrecord{
        \smalltfield{e}{unique($Q$)}}}} . \\
  \hspace*{2em}$\lambda P$:\textit{Ppty} . \\
  \hspace*{3em}\record{
    \mfield{restr}{$Q\!\restriction\!c.\mathfrak{c}$.e}{\textit{Ppty}}\\
    \mfield{scope}{$P|_{\mathfrak{F}(\text{restr})}$}{\textit{Ppty}}\\
    \tfield{e}{every(restr, scope)}}$\urcorner$


        
      \item[\textnormal{Lex$_{\mathrm{DefArt}}$($T_{\mathrm{Phon}}$)}]
        \mbox{}

        If $T_{\mathrm{Phon}}$ is a phonological type, then
        Lex$_{\mathrm{IndefArt}}$($T_{\mathrm{Phon}}$) is
        \begin{quote}
          Lex($T_{\mathrm{Phon}}$, \textit{Det}) \d{$\wedge$}
          \smallrecord{\smallmfield{cont}{SemDefArt}{(\textit{Ppty}$\rightarrow$\textit{PQuant})}}
        \end{quote}

      \item[\textnormal{SemIntransVerb($T_{\mathrm{bg}}$, $p$)}]
        \mbox{}

        If $T_{\text{bg}}$ is a record type (for context) and $p$ is a
        predicate with arity $\langle\textit{Ind}\rangle$, then SemIntransVerb($T_{\mathrm{bg}}$, $p$) is
        \begin{quote}
          $\ulcorner\lambda c$:$T_{\mathrm{bg}}$ . $\ulcorner\lambda
          r$:\smallrecord{\smalltfield{x}{\textit{Ind}}}
          . \record{\tfield{e}{$p$($r$.x)}}$\urcorner\urcorner$
        \end{quote}

        If $T_{\text{bg}}\sqsubseteq$\smallrecord{\smalltfield{$\mathfrak{c}$}{\textit{Rec}}} is a record type (for context) and $p$ is a
        predicate with arity $\langle\textit{Rec}, \textit{Rec}\rangle$, then SemIntransVerb($T_{\mathrm{bg}}$, $p$) is
        \begin{quote}
          $\ulcorner\lambda c$:$T_{\mathrm{bg}}$ . $\ulcorner\lambda
          r$:\smallrecord{\smalltfield{x}{\textit{Rec}}}
          . \record{\tfield{e}{$p$($r$.x, $c.\mathfrak{c}$)}}$\urcorner\urcorner$
        \end{quote}

        
      \item[\textnormal{Lex$_{\mathrm{IntransVerb}}$($T_{\mathrm{phon}}$,
          $T_{\mathrm{bg}}$, $p$)}] \mbox{}

        % If $T_{\mathrm{phon}}$ is a phonological type,
        % $T_{\mathrm{bg}}$ a record type (for context) and $p$ is a
        % predicate with arity $\langle\textit{Ind}\rangle$, then Lex$_{\mathrm{IntransVerb}}$($T_{\mathrm{phon}}$,
        % $T_{\mathrm{bg}}$, $p$) is
        % \begin{quote}
        %   Lex($T_{\mathrm{phon}}$, \textit{V$_i$}) \d{$\wedge$}
        %   \smallrecord{\smallmfield{cnt}{SemIntransVerb($T_{\mathrm{bg}}$, $p$)}{\textit{PPpty}}}
        % \end{quote}

        If $T_{\mathrm{phon}}$ is a phonological type,
        $T_{\mathrm{bg}}\sqsubseteq$\smallrecord{\smalltfield{$\mathfrak{c}$}{\textit{Rec}}} a record type (for context) and $p$ is a
        predicate with arity $\langle\textit{Ind}\rangle$ or $\langle\textit{Rec}, \textit{Rec}\rangle$, then Lex$_{\mathrm{IntransVerb}}$($T_{\mathrm{phon}}$,
        $T_{\mathrm{bg}}$, $p$) is
        \begin{quote}
          Lex($T_{\mathrm{phon}}$, \textit{V$_i$}) \d{$\wedge$}
          \smallrecord{\smallmfield{cnt}{SemIntransVerb($T_{\mathrm{bg}}$, $p$)}{\textit{PPpty}}}
        \end{quote}

        
      \item[\textnormal{SemTransVerb($T_{\mathrm{bg}}, p$)}] \mbox{}

        If $T_{\text{bg}}$ is a record type (for context) and $p$ is a
        predicate with arity $\langle\textit{Ind},\textit{Ind}\rangle$, then SemTransVerb($T_{\mathrm{bg}}$, $p$) is
        \begin{quote}
          $\ulcorner\lambda c$:$T_{\mathrm{bg}}$ . $\lambda
          \mathcal{Q}$:\textit{Quant} . $\ulcorner\lambda
          r_1$:\smallrecord{\smalltfield{x}{\textit{Ind}}} . $\mathcal{Q}(\ulcorner\lambda r_2$:\smallrecord{\smalltfield{x}{\textit{Ind}}}
          . \record{\tfield{e}{$p$($r_1$.x, $r_2$.x)}}$\urcorner)\urcorner\urcorner$
        \end{quote}

        If $T_{\text{bg}}$ is a record type (for context) and $p$ is a
  predicate with arity $\langle\textit{Ind},\textit{Quant}\rangle$, then SemTransVerb($T_{\mathrm{bg}}$, $p$) is
  \begin{quote}
    $\ulcorner\lambda c$:$T_{\mathrm{bg}}$ . $\lambda
    \mathcal{Q}$:\textit{Quant} . $\ulcorner\lambda
    r$:\smallrecord{\smalltfield{x}{\textit{Ind}}}
    . \record{\tfield{e}{$p$($r$.x, $\mathcal{Q}$)}}$\urcorner)\urcorner$
  \end{quote}
        
\item[\textnormal{Lex$_{\mathrm{TransVerb}}$($T_{\mathrm{phon}}$,
          $T_{\mathrm{bg}}$, $p$)}] \mbox{}

        If $T_{\mathrm{phon}}$ is a phonological type,
        $T_{\mathrm{bg}}$ a record type (for context) and $p$ is a
        predicate with arity $\langle\textit{Ind},\textit{Ind}\rangle$
        or $\langle\textit{Ind},\textit{Quant}\rangle$, then Lex$_{\mathrm{TransVerb}}$($T_{\mathrm{phon}}$,
        $T_{\mathrm{bg}}$, $p$) is
        \begin{quote}
          Lex($T_{\mathrm{phon}}$, \textit{V$_t$}) \d{$\wedge$}
          \smallrecord{\smallmfield{cnt}{SemTransVerb($T_{\mathrm{bg}}$, $p$)}{\textit{PPpty}}}
        \end{quote}

        

        
      \item[\textnormal{SemBe}] \mbox{}

        % $\lambda c:T_{\text{bg}}$ . \\
%         \hspace*{1em}$\lambda\mathcal{Q}$:\textit{Quant} . \\
% \hspace*{2em} $\ulcorner\lambda r_1$:\smallrecord{\tfield{x}{\textit{Ind}}}
% . \\
% \hspace*{3em} $\mathcal{Q}$($\ulcorner\lambda
% r_2$:\smallrecord{\tfield{x}{\textit{Ind}}}
% . \record{\mfield{x}{$r_2$.x, $r_1$.x}{\textit{Ind}}\\
% \tfield{e}{be(x)}}$\urcorner$)$\urcorner$

        \begin{description}
          
        \item[\textnormal{SemBe$_{\text{ID}}$}] \mbox{}

          $\ulcorner\lambda c$:\smallrecord{
            \footnotesize{\textit{Cntxt}}\\
    \smalltfield{$\mathfrak{c}$}{\smallrecord{
        \smalltfield{ty}{\textit{Type}}}}} . \\
        \hspace*{1em}$\lambda\mathcal{Q}$:\textit{Quant} . \\
        \hspace*{2em} $\ulcorner\lambda r_1$:\smallrecord{
          \smalltfield{x}{$c.\mathfrak{c}$.ty}}
. \\
\hspace*{3em} $\mathcal{Q}$($\ulcorner\lambda
r_2$:\smallrecord{
  \smalltfield{x}{$c.\mathfrak{c}$.ty}}
. \record{\mfield{x}{$r_1$.x, $r_2$.x}{$c.\mathfrak{c}$.ty}\\
  \tfield{e}{be(x)}}$\urcorner$)$\urcorner\urcorner$

\item[\textnormal{SemBe$_{\text{scalar}}$}] \mbox{}

  $\ulcorner\lambda c$:\smallrecord{
    \footnotesize{\textit{Cntxt}}\\
    \smalltfield{$\mathfrak{c}$}{\smallrecord{
        \smalltfield{ty}{\textit{Type}}\\
      \smalltfield{sc}{(ty$\rightarrow$\textit{Real})}}}} . \\
        \hspace*{1em}$\lambda\mathcal{Q}$:\textit{Quant} . \\
        \hspace*{2em} $\ulcorner\lambda r_1$:\smallrecord{
          \smalltfield{x}{$c.\mathfrak{c}$.ty}}
. \\
\hspace*{3em} $\mathcal{Q}$($\ulcorner\lambda
r_2$:\smallrecord{
  \smalltfield{x}{\textit{Real}}}
. \record{\mfield{x}{$c.\mathfrak{c}$.sc($r_1$.x), $r_2$.x}{\textit{Real}}\\
  \tfield{e}{be(x)}}$\urcorner$)$\urcorner\urcorner$

\end{description}


\item[\textnormal{Lex$_{\mathrm{be}}$($T_{\mathrm{Phon}}$)}] \mbox{}

  If $T_{\mathrm{Phon}}$ is a phonological type, then
  Lex$_{\mathrm{be}_{\text{ID}}}$($T_{\mathrm{Phon}}$) is
\begin{quote}
  Lex($T_{\mathrm{Phon}}$,
\textit{V}) \d{$\wedge$}
\smallrecord{\smallmfield{cont}{SemBe$_{\text{ID}}$}{(\textit{Quant}$\rightarrow$\textit{Ppty})}}
\end{quote}

If $T_{\mathrm{Phon}}$ is a phonological type, then
  Lex$_{\mathrm{be}_{\text{scalar}}}$($T_{\mathrm{Phon}}$) is
\begin{quote}
  Lex($T_{\mathrm{Phon}}$,
\textit{V}) \d{$\wedge$}
\smallrecord{\smallmfield{cont}{SemBe$_{\text{scalar}}$}{(\textit{Quant}$\rightarrow$\textit{Ppty})}}
\end{quote}

\item[\textnormal{$\mathrm{FrameType}(p)$}] \mbox{}

  $\mathrm{FrameType}$ is a partial function on predicates, $p$, with
  arity $\langle\textit{Ind}\rangle$ which can be defined for
  particular agents and particular times, which obeys the constraint:
  \begin{quote}
    $\mathrm{FrameType}(p)\sqsubseteq$ \record{
    \tfield{x}{\textit{Ind}}\\
    \tfield{e}{$p$(x)}}
\end{quote}

\item[\textnormal{$p$\_frame}] \mbox{}

  \begin{enumerate} 
 
\item If $p$ is a predicate in the domain of $\mathrm{FrameType}$,
  then $p$\_frame is a predicate with arity $\langle\textit{Rec}\rangle$. 
 
\item $e:p\_\text{frame}(r)$ iff $r:\mathrm{FrameType}(p)$ and $e=r$ 
 
\end{enumerate}

\item[\textnormal{$p$\_pl}] \mbox{}

  \begin{enumerate} 
 
\item If $p$ is a singular predicate (i.e. there is no $p'$ such that
  $p=p'\_\text{pl}$) with arity $\langle T\rangle$, then
  $p\_\text{pl}$ is a predicate with arity $\langle\mathrm{plurality}(T)\rangle$ 
 
\item $e:p\_\text{pl}(A)$ if for all $a\in A$, $e:p(a)$ 
 
\end{enumerate} 
  

\item[\textnormal{CommonNounIndToFrame}] \mbox{}

  If $T_{\mathrm{phon}}$ is a phonological type, $p$ is a predicate with
arity $\langle\textit{Ind}\rangle$ and
$T_\mathrm{bg}$ is a record type (the ``background type'' or
``presupposition'') then \\ 
\mbox{CommonNounIndToFrame(Lex$_{\mathrm{CommonNoun}}$($T_{\mathrm{phon}}$,
  $T_\mathrm{bg}$, $p$))} =
\begin{quote}
  Lex$_{\mathrm{CommonNoun}}$($T_{\mathrm{phon}}$,
  $T_\mathrm{bg}$, $p$\_frame)
\end{quote}

\item[\textnormal{RestrictCommonNoun}] \mbox{}

  If $T_{\mathrm{phon}}$ is a phonological type, $p$ is a predicate,
$T_{\mathrm{bg}}$ and $T_{\mathrm{res}}$ are record types and $\Sigma$
is Lex$_{\mathrm{CommonNoun}}$($T_{\mathrm{phon}}$, $T_{\mathrm{bg}}$,
$p$), then RestrictCommonNoun($\Sigma$, $T_{\mathrm{res}}$) is
\begin{quote}
$\Sigma$
\fbox{\d{$\wedge$}} \record{
  \mfield{cont}{$\ulcorner\lambda c\!:\!T_{\mathrm{bg}}\ .\
    \ulcorner\text{SemCommonNoun}(T_{\mathrm{bg}},p)(c)\!\mid_{T_{\mathrm{res}}}\urcorner\urcorner$}{\textit{PPpty}}}
\end{quote}

\item[\textnormal{IntransVerbIndToFrame}] \mbox{}

  If $T_{\mathrm{phon}}$ is a phonological type, $p$ is a predicate with
arity $\langle\textit{Ind}\rangle$ and
$T_\mathrm{bg}$ is a record type (the ``background type'' or
``presupposition'') then \\ 
\mbox{IntransVerbIndToFrame(Lex$_{\mathrm{IntransVerb}}$($T_{\mathrm{phon}}$,
  $T_\mathrm{bg}$, $p$))} =
\begin{quote}
  Lex$_{\mathrm{IntransVerb}}$($T_{\mathrm{phon}}$,
  $T_\mathrm{bg}$, $p$\_frame)
\end{quote}

\item[\textnormal{PluralCommonNoun}] \mbox{}

  We assume that `pluralnoun' is a function that maps phonological
  types for singular common nouns to corresponding phonological types
  for plural common nouns.

  If $T_{\text{phon}}$ is a (singular) phonological type, $p$ is a
  singular predicate with arity $\langle T\rangle$ and $T_{\text{bg}}$
  is a record type then
  PluralCommonNoun(Lex$_{\text{CommonNoun}}$($T_{\text{phon}}$,
  $T_{\text{bg}}$, $p$)) =
  \begin{quote}
    Lex$_{\text{CommonNoun}}$(pluralnoun($T_{\text{phon}}$),
    $T_{\text{bg}}$, $p$\_pl)
  \end{quote}

  
\item[\textnormal{PluralIntransVerb}] \mbox{}

  We assume that `pluralverb' is a function that maps phonological
  types for singular verbs to corresponding phonological types
  for plural verbs.

  If $T_{\text{phon}}$ is a (singular) phonological type, $p$ is a
  singular predicate with arity $\langle T\rangle$ and $T_{\text{bg}}$
  is a record type then
  PluralIntransVerb(Lex$_{\text{IntransVerb}}$($T_{\text{phon}}$,
  $T_{\text{bg}}$, $p$)) =
  \begin{quote}
    Lex$_{\text{IntransVerb}}$(pluralverb($T_{\text{phon}}$),
    $T_{\text{bg}}$, $p$\_pl)
  \end{quote} 
        
\item[\textnormal{TransVerbToVerbPhrase} New!] \mbox{}

  If $T_{\text{phon}}$ is a phonological type, $T_{\text{bg}}$ a
  context type, $p$ is a predicate with arity
  $\langle\textit{Ind},\textit{Ind}\rangle$ or
  $\langle\textit{Ind},\textit{Quant}\rangle$ and $\Sigma$ is
  Lex$_{\text{TransVerb}}$($T_{\text{phon}}$, $T_{\text{bg}}$, $p$),
  then TransVerbToVerbPhrase($\Sigma$) is
  \begin{quote}
    $\Sigma$ \fbox{\d{$\wedge$}} \record{
      \mfield{cat}{vp}{\textit{Cat}}\\
      \mfield{cont}{$\varphi$}{\textit{PPpty}}}
  \end{quote}
  where $\varphi$ is
  \begin{quote}
    $\ulcorner\lambda c$:$\Sigma$.cont.bg\d{$\wedge$}\smallrecord{
      \smalltfield{$\mathfrak{g}$}{\smallrecord{
          \smalltfield{x$_0$}{\textit{Ind}}}}}
    . $\Sigma$.cont($c$)($\lambda P$:\textit{Ppty}
    . $P\{c.\mathfrak{g}.\text{x}_0\}$)$\urcorner$
  \end{quote}
  
  
  
\end{description}



\subsubsection{Constituent structure}
\begin{description}
\item[\textnormal{RuleDaughters($T_{\text{daughters}}$,
$T_{\text{mother}}$)}] \mbox{}

If $T_{\text{mother}}$ is a sign type and $T_{\text{daughters}}$ is a
type of strings of signs then
\begin{quote}
RuleDaughters($T_{\text{daughters}}$,
$T_{\text{mother}}$)
\end{quote}
is
\begin{quote}
  $\lambda u\! :\! T_{\text{daughters}}$\ . $T_{\text{mother}}$ \d{$\wedge$} \smallrecord{\smalltfield{syn}{\smallrecord{\smallmfield{daughters}{$u$}{$T_{\text{daughters}}$}}}}
\end{quote}

\item[\textnormal{ConcatPhon}] \mbox{}

  $\lambda
u$:\smallrecord{\smalltfield{s-event}{\smallrecord{\smalltfield{e}{\textit{Phon}}}}}$^+$\
. \\
\hspace*{1em}\record{\tfield{s-event}{\record{\mfield{e}{concat$_i$($u[i]$.s-event.e)}{\textit{Phon}}}}}

\item[\textnormal{$T_{\text{mother}}\longrightarrow T_{\text{daughter}_1},\ldots
    T_{\text{daughter}_n}$}] \mbox{}

  If $T_{\text{mother}}$ is a sign type and
  $T_{\text{daughter}_1},\ldots T_{\text{daughter}_n}$ are sign types,
  then
  \begin{quote}
    $T_{\text{mother}}\longrightarrow T_{\text{daughter}_1}\ldots
    T_{\text{daughter}_n}$
  \end{quote}
  represents
  \begin{quote}
RuleDaughters($T_{\text{mother}}$,
${T_{\text{daughter}_1}}^\frown\ldots^\frown T_{\text{daughter}_n}$)\d{\d{$\wedge$}}ConcatPhon 
\end{quote}

\item[\textnormal{$\alpha\text{@}\beta$} Revised!] \mbox{}

  If $\alpha$ : \smallrecord{\smalltfield{bg}{\textit{CntxtType}}\\
                           \smalltfield{fg}{(bg$\rightarrow$($T_1\rightarrow
                             T_2$))}} 
and $\beta$ : \smallrecord{\smalltfield{bg}{\textit{CntxtType}}\\
                           \smalltfield{fg}{(bg$\rightarrow T_1$)}}
                         then the \textit{combination of $\alpha$ and
    $\beta$  based on functional application}, $\alpha\text{@}\beta$, is
  \begin{quote}
   $\ulcorner\lambda c$:$[\alpha.\text{bg}]_{\mathfrak{c}\leadsto\mathfrak{c}.\text{f}}$
      \d{$\wedge$}$\mathrm{incr}([\beta.\text{bg}]_{\mathfrak{c}\leadsto\mathfrak{c}.\text{a}},\alpha.\text{bg})$
      . \\
      \hspace*{2em}$[\alpha]_{\mathfrak{c}\leadsto\mathfrak{c}.\text{f}}(c)(\mathrm{incr}([\beta.\text{fg}]_{\mathfrak{c}\leadsto\mathfrak{c}.\text{a}},\alpha.\text{bg})(c))\urcorner$

      
    \end{quote}

    


\item[\textnormal{ContForwardApp($T_{\text{arg}}$, $T_{\text{res}}$)}] \mbox{}

  If $T_{\text{arg}}$ and $T_{\text{res}}$ are types, then
  ContForwardApp($T_{\text{arg}}$, $T_{\text{res}}$) is
\begin{quote}
  $\lambda
u$:\smallrecord{\smalltfield{cont}{\smallrecord{\smalltfield{bg}{\textit{CntxtType}}\\
                                               \smalltfield{fg}{(bg$\rightarrow$($T_{\text{arg}}\rightarrow T_{\text{res}}$))}}}}$^{\frown}$
   \smallrecord{\smalltfield{cont}{\smallrecord{\smalltfield{bg}{\textit{CntxtType}}\\
                                               \smalltfield{fg}{(bg$\rightarrow T_{\text{arg}}$)}}}} . \\
\hspace*{2em}\smallrecord{\smallmfield{cont}{$u$[0].cont@$u$[1].cont}{\smallrecord{\smalltfield{bg}{\textit{CntxtType}}\\
                                                                                \smalltfield{fg}{(bg$\rightarrow
                                                                                  T_{\text{res}}$)}}}}
\end{quote}



% \item[\textnormal{$\alpha\text{@}\beta$}] \mbox{}

%   If $\alpha$ : \smallrecord{\smalltfield{bg}{\textit{RecType}}\\
%                            \smalltfield{fg}{(bg$\rightarrow$($T_1\rightarrow
%                              T_2$))}} 
% and $\beta$ : \smallrecord{\smalltfield{bg}{\textit{RecType}}\\
%                            \smalltfield{fg}{(bg$\rightarrow T_1$)}}
%                          then the \textit{combination of $\alpha$ and
%     $\beta$  based on functional application}, $\alpha\text{@}\beta$, is
% \begin{quote}
%   $\ulcorner\lambda c$:$[\alpha.\text{bg}]_{\mathfrak{c}\leadsto\mathfrak{c}.\text{f}}$
%       \d{$\wedge$}$\mathrm{incr}_{\mathfrak{s}.\text{x}}([\beta.\text{bg}]_{\mathfrak{c}\leadsto\mathfrak{c}.\text{a}},\alpha.\text{bg})$
%       . \\
%       \hspace*{2em}
% $[\alpha]_{\mathfrak{c}\leadsto\mathfrak{c}.\text{f}}(c)(\mathrm{incr}_{\mathfrak{s}.\text{x}}([\beta.\text{fg}]_{\mathfrak{c}\leadsto\mathfrak{c}.\text{a}},\alpha.\text{bg})(c))\urcorner$
      
% \end{quote}


% \item[\textnormal{ContForwardApp($T_{\text{arg}}$, $T_{\text{res}}$)}] \mbox{}

%   If $T_{\text{arg}}$ and $T_{\text{res}}$ are types, then
%   ContForwardApp($T_{\text{arg}}$, $T_{\text{res}}$) is
% \begin{quote}
%   $\lambda
% u$:\smallrecord{\smalltfield{cont}{$(T_{\text{arg}}\rightarrow
%     T_{\text{res}})$}}$^{\frown}$\smallrecord{\smalltfield{cont}{$T_{\text{arg}}$}} . \\
% \hspace*{2em}\smallrecord{\smallmfield{cont}{$u$[0].cont@$u$[1].cont}{$T_{\text{res}}$}}

% \end{quote}

\item[\textnormal{$T_{\text{mother}}\longrightarrow
    T_{\text{daughter}_1}\ T_{\text{daughter}_2}\ \mid\
    T_{\text{daughter}_1}'(T_{\text{daughter}_2}':T_{\text{arg}}):T_{\text{res}}$}]
  \mbox{}

  If $T_{\text{mother}}$, $T_{\text{daughter}_1}$ and
  $T_{\text{daughter}_2}$ are sign types and $T_{\text{arg}}$ and
  $T_{\text{res}}$ are content types, then
  \begin{quote}
    $T_{\text{mother}}\longrightarrow
    T_{\text{daughter}_1}\ T_{\text{daughter}_2}\ \mid\
    T_{\text{daughter}_1}'(T_{\text{daughter}_2}':T_{\text{arg}}):T_{\text{res}}$
  \end{quote}
  is
  \begin{quote}
  $T_{\text{mother}}\longrightarrow
    T_{\text{daughter}_1}\ T_{\text{daughter}_2}$ \d{\d{$\wedge$}}
    ContForwardApp($T_{\text{arg}}$, $T_{\text{res}}$)
  \end{quote}

  \item[\textnormal{$\alpha\text{@}_{\mathrm{wh}_{i,j}}\beta$} New!]
    \mbox{}

      If
  \begin{enumerate}
  \item $\alpha$ : \smallrecord{
      \smalltfield{bg}{\textit{CntxtType}}\\
      \smalltfield{fg}{(bg$\rightarrow$\textit{Quant})}},
    
  \item $\beta$ : \smallrecord{
      \smalltfield{bg}{\textit{CntxtType}}\\
      \smalltfield{fg}{(bg$\rightarrow$\textit{RecType})}},
    
  \item $\alpha$.bg $\sqsubseteq$ \smallrecord{
      \smalltfield{$\mathfrak{w}$}{\smallrecord{
          \smalltfield{x$_i$}{\textit{Ind}}}}} for some natural number,
    $i$, and
    
  \item $\beta$.bg $\sqsubseteq$ \smallrecord{
      \smalltfield{$\mathfrak{g}$}{\smallrecord{
          \smalltfield{x$_j$}{\textit{Ind}}}}} for some natural number,
    $j$,
  \end{enumerate}
  then \textit{the \textit{wh}$_{i,j}$-combination of $\alpha$ and
    $\beta$}, $\alpha\text{@}_{\mathrm{wh}_{i,j}}\beta$, is
  \begin{quote}
    $\ulcorner\lambda
    c$:([$\alpha$.bg$\ominus\mathrm{paths}_{\mathfrak{w}.\text{x}_i}(\alpha.\text{bg})]_{\mathfrak{c}\leadsto\mathfrak{c}.\text{f}}$\d{$\wedge$}\\
    \hspace*{5em}$\mathrm{incr}([\beta.\text{bg}\ominus\mathrm{paths}_{\mathfrak{g}.\text{x}_j}(\beta.\text{bg})]_{\mathfrak{c}\leadsto\mathfrak{c}.a},\alpha.\text{bg})$)
    . \\
    \hspace*{1em} $\mathfrak{P}(\ulcorner\lambda r_1$:$[\alpha.\text{bg}^{\mathfrak{w}.\text{x}_i}]_{\mathfrak{w}.\text{x}_i\leadsto\text{x}}$ . \\
    \hspace*{4em}$\alpha_{\mathfrak{c}\leadsto\mathfrak{c}.\text{f},\mathfrak{w}.\text{x}_i\leadsto\text{x}}(c[r_1])$
    ($\mathfrak{P}(\ulcorner\lambda r_2$:$[\beta.\text{bg}^{\mathfrak{g}.\text{x}_j}]_{\mathfrak{g}.\text{x}_j\leadsto\text{x}}$ . \\
    \hspace*{15em}$\mathrm{incr}(\beta_{\mathfrak{c}\leadsto\mathfrak{c}.\text{a},\mathfrak{g}.\text{x}_j\leadsto\text{x}},\alpha.\text{bg})(c[r_2])\urcorner)$)$\urcorner)\urcorner$
  \end{quote} 

\item[\textnormal{ContForwardApp$_{\text{@}_{\text{wh}_{i,j}}}$($T_{\text{fun}},T_{\text{arg}},T_{\text{res}}$)}
  New!] \mbox{}

  If $T_{\text{fun}}$, $T_{\text{arg}}$ and $T_{\text{res}}$ are types
such that if $\alpha:T_{\text{fun}}$ and $\beta:T_{\text{arg}}$, then
$\alpha\text{@}_{\text{wh}_{i,j}}\beta$ is defined and of type
$T_{\text{res}}$, then
\begin{quote}
  ContForwardApp$_{\text{@}_{\text{wh}_{i,j}}}$($T_{\text{fun}},T_{\text{arg}},T_{\text{res}}$)
\end{quote}
is
\begin{quote}
  $\lambda u$:\smallrecord{
    \smalltfield{cont}{$T_{\text{fun}}$}}$^\frown$\smallrecord{
    \smalltfield{cont}{$T_{\text{arg}}$}} . \smallrecord{
    \smallmfield{cont}{$u[0]$.cont@$_{\text{wh}_{i,j}}u[1]$.cont}{$T_{\text{res}}$}}
\end{quote}

\item[\textnormal{$T_{\text{mother}}\longrightarrow
    T_{\text{daughter}_1}\ T_{\text{daughter}_2}\ \mid\
    T_{\text{daughter}_1}'(_{\text{@}_{\text{wh}_{i,j}}}T_{\text{daughter}_2}':T_{\text{arg}}):T_{\text{res}}$}
  New!] \mbox{}

  If $T_{\text{mother}}$, $T_{\text{daughter}_1}$ and
  $T_{\text{daughter}_2}$ are sign
  types, $T_{\text{daughter}_1}\sqsubseteq$\smallrecord{
    \smallmfield{cont}{$c_1$}{\textit{Cont}}} where
  $c_1.\text{bg}\sqsubseteq$\smallrecord{
    \smalltfield{$\mathfrak{w}$}{\smallrecord{
        \smalltfield{x$_i$}{\textit{Ind}}}}}, $T_{\text{daughter}_2}\sqsubseteq$\smallrecord{
    \smallmfield{cont}{$c_2$}{\textit{Cont}}} where
  $c_2.\text{bg}\sqsubseteq$\smallrecord{
    \smalltfield{$\mathfrak{g}$}{\smallrecord{
        \smalltfield{x$_j$}{\textit{Ind}}}}} and $T_{\text{arg}}$ and
  $T_{\text{res}}$ are content types, then
  \begin{quote}
    $T_{\text{mother}}\longrightarrow
    T_{\text{daughter}_1}\ T_{\text{daughter}_2}\ \mid\
T_{\text{daughter}_1}'(_{\text{@}_{\text{wh}_{i,j}}}T_{\text{daughter}_2}':T_{\text{arg}}):T_{\text{res}}$
  \end{quote}
  is
  \begin{quote}
  $T_{\text{mother}}\longrightarrow
    T_{\text{daughter}_1}\ T_{\text{daughter}_2}$ \d{\d{$\wedge$}}
    ContForwardApp$_{\text{@}_{\text{wh}_{i,j}}}$($T_{\text{arg}}$, $T_{\text{res}}$)
  \end{quote} 



  
\item[\textnormal{$\alpha\text{@\!@}\beta$}] \mbox{}

  If $\alpha$ : ($T_1\rightarrow$ \smallrecord{\smalltfield{bg}{\textit{CntxtType}}\\
                           \smalltfield{fg}{(bg$\rightarrow T_2$)}}) 
                         and $\beta$ : \smallrecord{\smalltfield{bg}{\textit{CntxtType}}\\
                           \smalltfield{fg}{(bg$\rightarrow T_1$)}}
                         then the \textit{combination of $\alpha$ and
    $\beta$  based on functional application}, $\alpha\text{@\!@}\beta$, is
  \begin{quote}
    $\ulcorner\lambda c$:\record{
      \tfield{$\mathfrak{c}$}{\record{
          \tfield{s}{$\beta$.bg}\\
          \tfield{f}{$\alpha(\beta(s))$.bg}\\
          \mfield{a}{s.$\mathfrak{c}$}{\textit{PropCntxt}}}}\\
    \mfield{$\mathfrak{s}$}{$\mathfrak{c}$.s.$\mathfrak{s}$}{\textit{Assgnmnt}}}
      . \\*[\baselineskip]
      \hspace*{10em}$[\alpha]_{\mathfrak{c}\leadsto\mathfrak{c}.\text{f}}([\beta]_{\mathfrak{c}\leadsto\mathfrak{c}.\text{a}}(c))(c)\urcorner$
    \end{quote}
    
\item[\textnormal{ContForwardApp$_{\text{@\!@}}$($T_{\text{arg}}$,
    $T_{\text{res}}$)}] \mbox{}

  If $T_{\text{arg}}$ and $T_{\text{res}}$ are types, then
  ContForwardApp$_{\text{@\!@}}$($T_{\text{arg}}$, $T_{\text{res}}$) is
\begin{quote}
  $\lambda
u$:\smallrecord{\smalltfield{cont}{$(T_{\text{arg}}\rightarrow
    T_{\text{res}})$}}$^{\frown}$\smallrecord{\smalltfield{cont}{$T_{\text{arg}}$}} . \\
\hspace*{2em}\smallrecord{\smallmfield{cont}{$u$[0].cont@\!@$u$[1].cont}{$T_{\text{res}}$}}

\end{quote}
  
\item[\textnormal{$T_{\text{mother}}\longrightarrow
    T_{\text{daughter}_1}\ T_{\text{daughter}_2}\ \mid\
    T_{\text{daughter}_1}'(_{\text{@\!@}}T_{\text{daughter}_2}':T_{\text{arg}}):T_{\text{res}}$}]
  \mbox{}

  If $T_{\text{mother}}$, $T_{\text{daughter}_1}$ and
  $T_{\text{daughter}_2}$ are sign types and $T_{\text{arg}}$ and
  $T_{\text{res}}$ are content types, then
  \begin{quote}
    $T_{\text{mother}}\longrightarrow
    T_{\text{daughter}_1}\ T_{\text{daughter}_2}\ \mid\
    T_{\text{daughter}_1}'(_{\text{@\!@}}T_{\text{daughter}_2}':T_{\text{arg}}):T_{\text{res}}$
  \end{quote}
  is
  \begin{quote}
  $T_{\text{mother}}\longrightarrow
    T_{\text{daughter}_1}\ T_{\text{daughter}_2}$ \d{\d{$\wedge$}}
    ContForwardApp$_{\text{@\!@}}$($T_{\text{arg}}$, $T_{\text{res}}$)
  \end{quote}

  
\item[\textnormal{$\alpha\text{@}_{\&}\beta$} New!] \mbox{}

  If $T$ is a type, $\alpha:{^T\textit{PPpty}}$ and
  $\beta:{^T\textit{PPpty}}$ 
  then \textit{the property conjunction
    combination of $\alpha$ and $\beta$}, $\alpha\text{@}_{\&}\beta$,
  is
\begin{quote}
  $\lambda
  c$:$[\alpha.\text{bg}]_{\mathfrak{c}\leadsto\mathfrak{c}.\text{f}}$\d{$\wedge$}$\mathrm{incr}([\beta.\text{bg}]_{\mathfrak{c}\leadsto\mathfrak{c}.\text{a}},\alpha.\text{bg})$
        . $\alpha_{\mathfrak{c}\leadsto\mathfrak{c}.\text{f}}(c)\&\mathrm{incr}([\beta]_{\mathfrak{c}\leadsto\mathfrak{c}.\text{a}},\alpha.\text{bg})(c)$
      \end{quote}

      
    \item[\textnormal{ContForwardApp$_{\text{@}_{\&}}$($T$)} New!]
      \mbox{}

      If $T$ is a type, then ContForwardApp$_{\text{@}_{\&}}$($T$) is
  \begin{quote}
    $\lambda u$:\record{
      \tfield{cont}{${^T\textit{PPpty}}$}}$^\frown$\record{
      \tfield{cont}{${^T\textit{PPpty}}$}} .\\
    \hspace*{1em}\record{
      \mfield{cont}{$u[0].\text{cont}\text{@}_{\&}u[1].\text{cont}$}{${^T\textit{PPpty}}$}}
  \end{quote}

  
\item[\textnormal{$T_{\text{mother}}\longrightarrow T_{\text{daughter}_1}\
    T_{\text{daughter}_2}\ \mid\
    T_{\text{daughter}_1}'(_{\text{@}_{\&}}T_{\text{daughter}_2}':{^T\textit{PPpty}}):{^T\textit{PPpty}}$}
  New!] \mbox{}

  If $T$ is a type, $T_{\text{mother}}$, $T_{\text{daughter}_1}$ and
$T_{\text{daughter}_2}$ are sign types,
$T_{\text{daughter}_1}\sqsubseteq$ \record{
  \tfield{cont}{$^T\textit{PPpty}$}} and $T_{\text{daughter}_2}\sqsubseteq$ \record{
  \tfield{cont}{$^T\textit{PPpty}$}}, then
  \begin{quote}
    $T_{\text{mother}}\longrightarrow T_{\text{daughter}_1}\
    T_{\text{daughter}_2}\ \mid\
    T_{\text{daughter}_1}'(_{\text{@}_{\&}}T_{\text{daughter}_2}':{^T\textit{PPpty}}):{^T\textit{PPpty}}$
  \end{quote}
  is
  \begin{quote}
    $T_{\text{mother}}\longrightarrow T_{\text{daughter}_1}\
    T_{\text{daughter}_2}$ \d{\d{$\wedge$}}
    ContForwardApp$_{\text{@}_{\&}}$($T$)
  \end{quote}

\end{description}


\subsubsection{Action rules} (as in Chapter~\ref{ch:intensional})

% \begin{description}

  




% \item[\textnormal{\textsc{LexRes}}] \mbox{}

%   \begin{prooftree}
%     \hypo{\text{Lex}(T,C) \text{ resource}_A}
%     \hypo{u:_A T}
%     \infer[enth]2{:_A(\text{Lex}(T,C)\text{\d{$\wedge$}\smallrecord{\smalltfield{s-event}{\smallrecord{\smallmfield{e}{$u$}{$T$}}}}})}
%   \end{prooftree}

  
% \item[\textnormal{\textsc{ToposConclude}} New!] \mbox{}

%   \begin{prooftree}
%     \hypo{\tau:\textit{Topos}}
%     \hypo{\tau \text{ resource}_A}
%     \hypo{s:_A\tau.\text{bg}}
%     \infer[enth]3{:_A\tau(s)}
%   \end{prooftree}

  
% \item[\textnormal{\textsc{ToposPermit}} New!] \mbox{}

%   \begin{prooftree}
%     \hypo{\tau:\textit{Topos}}
%     \hypo{\tau \text{ resource}_A}
%     \hypo{s:_A\tau.\text{bg}}
%     \infer[enth]3{:_A\tau(s)!}
%   \end{prooftree}

    
% \item[\textnormal{\textsc{ToposOblige}} New!] \mbox{}

%   \begin{prooftree}
%       \hypo{\tau:\textit{Topos}}
%       \hypo{\tau \text{ resource}_A}
%       \hypo{s:_A\tau.\text{bg}}
%       \infer[enth]3[oblig]{:_A\tau(s)!}
%     \end{prooftree}

    
  


%   \end{description}



\subsection{Universal speech act resources} (as in Chapter~\ref{ch:infex})

% \subsubsection{Types}

% \begin{description}
  
% \item[\textnormal{\textit{Assertion}}] --- \record{
%   \tfield{s-event}{\textit{SEvent}}\\
%   \tfield{cont}{\textit{RecType}}\\
%   \tfield{illoc}{assert(s-event, cont)}
% }
% \item[\textnormal{\textit{Query}}] --- \record{
%   \tfield{s-event}{\textit{SEvent}}\\
%   \tfield{cont}{\textit{Question}}\\
%   \tfield{illoc}{query(s-event, cont)}
% }

% \item[\textnormal{\textit{Command}}] --- \record{
%   \tfield{s-event}{\textit{SEvent}}\\
%   \tfield{cont}{\textit{RecType}}\\
%   \tfield{illoc}{command(s-event, cont)}
% }

% \item[\textnormal{\textit{Acknowledgement}}] --- \record{
%   \tfield{s-event}{\textit{SEvent}}\\
%   \tfield{cont}{\textit{RecType}}\\
%   \tfield{illoc}{acknowledge(s-event, cont)}
% }

% \item[\textnormal{\textit{AssertionType}}] --- a basic type

%   $T:\textit{AssertionType}$ iff $T\sqsubseteq \textit{Assertion}$

  
% \item[\textnormal{\textit{QueryType}}] --- a basic type

%   $T:\textit{QueryType}$ iff $T\sqsubseteq \textit{Query}$

  
% \item[\textnormal{\textit{CommandType}}] --- a basic type

%   $T:\textit{CommandType}$ iff $T\sqsubseteq \textit{Command}$


 
% \item[\textnormal{\textit{AcknowledgementType}}] --- a basic type

%   $T:\textit{AcknowledgementType}$ iff $T\sqsubseteq \textit{Acknowledgement}$

% \end{description}

\subsection{Universal dialogue resources} (as in Chapter~\ref{ch:propnames})

% \subsubsection{Types}

% \begin{description}
% \item[\textnormal{\textit{InfoState}}] --- \record{
%     \tfield{private}{
%       \record{
%         \tfield{agenda}{$\mathrm{list}(\textit{RecType})$}}} \\
%     \tfield{shared}{
%       \record{
%         \tfield{latest-utterance}{\textit{Sign}$^*$}\\
%         \tfield{commitments}{\textit{RecType}}}}}
  
% \item[\textnormal{\textit{InitInfoState}}] --- \record{
%     \tfield{private}{
%       \record{
%         \mfield{agenda}{[ ]}{$\mathrm{list}(\textit{RecType})$}}} \\
%     \tfield{shared}{
%       \record{
%         \mfield{latest-utterance}{$\varepsilon$}{\textit{Sign}$^*$}\\
%         \mfield{commitments}{\textit{Rec}}{\textit{RecType}}}}}  

  
% \item[\textnormal{\textit{GameBoard}} New!] --- a basic type

%   $T$ : \textit{GameBoard} iff $T\sqsubseteq$ \textit{InfoState}
  
% \item[\textnormal{\textit{TotalInfoState}} New!] --- \record{\tfield{ltm}{\textit{RecType}} \\
%         \tfield{gb}{(ltm$\rightarrow$\textit{GameBoard})}}


% \end{description}

% \subsubsection{Update functions and action rules}

% %(as in Chapter~\ref{ch:infex})

% \begin{description}
% \item[\textnormal{f$_{\textsc{PlanAckAss}}$}] $\lambda r$:\textit{InfoState} . \\
%   \hspace*{4em}$\lambda u$:\textit{Assertion} . \\
%   \hspace*{6em}
%   \smallrecord{
%     \smalltfield{private}{\smallrecord{
%         \smalltfield{agenda}{\smallrecord{
%             \smalltfield{fst}{\smallrecord{
%                 \smalltfield{s-event}{\textit{SEvent} \d{$\wedge$} \smallrecord{
%                     \smallmfield{sp}{$u$.s-event.au}{\textit{Ind}}\\
%                     \smallmfield{au}{$u$.s-event.sp}{\textit{Ind}}}}\\
%                 \smallmfield{cont}{$u$.cont}{\textit{Cont}}\\
%                 \smalltfield{illoc}{acknowledge(s-event, cont)}}}\\
%             \smallmfield{rst}{$r$.private.agenda}{$\mathrm{list}(\textit{RecType})$}}}}}\\
%     \smalltfield{shared}{\smallrecord{
%         \smallmfield{latest-utterance}{$u$}{\textit{Assertion}}}}}
  
% \item[\textnormal{\textsc{PlanAckAss}}]
%   \begin{prooftree}
%     \hypo{s_{i,A}:_A T_{\mathrm{curr}}}
%     \hypo{T_{\mathrm{curr}}\sqsubseteq\mathrm{domtype}(\text{f}_{\textsc{PlanAckAss}})}
%     \hypo{u^*:_A T_{\mathrm{utt}}}
%     \hypo{T_{\mathrm{utt}}\sqsubseteq\textit{Assertion}}
%     \infer[enth]4{s_{i+1,A}:_A
%       T_{\mathrm{curr}}\text{\fbox{\d{$\wedge$}}}(\text{f}_{\textsc{PlanAccAss}}(s_{i,A})(u^*)\text{\d{$\wedge$}}\text{\smallrecord{\smalltfield{shared}{\smallrecord{
%               \smalltfield{latest-utterance}{$T_{\mathrm{utt}}$}}}}})}
%   \end{prooftree}

  
% \item[\textnormal{f$_{\textsc{IntegAck}}$}]
%   $\lambda r$:\textit{InfoState} . \\
%   \hspace*{2em}$\lambda u$:\textit{Acknowledgement} . \\
%   \hspace*{4em}\smallrecord{
%     \smalltfield{shared}{\smallrecord{
%         \smallmfield{commitments}{\smallrecord{
%             \smalltfield{prev}{$r$.shared.commitments}}\d{$\wedge$}$u$.cont}{\textit{RecType}}\\
%         \smallmfield{latest-utterance}{$u$}{\textit{Acknowledgement}}}}}

  
% \item[\textnormal{\textsc{IntegAck}}]
%    \begin{prooftree}
%     \hypo{s_{i,a}:_A T_{\mathrm{curr}}}
%     \hypo{T_{\mathrm{curr}}\sqsubseteq\mathrm{domtype}(\text{f}_{\mathrm{IntegAck}})}
%     \hypo{u^*:_A T_{\mathrm{utt}}}
%     \hypo{T_{\mathrm{utt}}\sqsubseteq\textit{Acknowledgement}}
%     \infer[enth]4{s_{i+1,A}:_A
%       T_{\mathrm{curr}}\text{\fbox{\d{$\wedge$}}}(\text{f}_{\textsc{IntegAck}}(s_{i,A})(u^*)\text{
%         \d{$\wedge$} \smallrecord{\smalltfield{shared}{\smallrecord{
%              \smalltfield{latest-utterance}{$T_{\mathrm{utt}}$}}}}})} 
%  \end{prooftree}

 
% \item[\textnormal{\textsc{ExecTopAgenda}}]
%   \begin{prooftree}
%     \hypo{s_{i,A}:_A\textit{InfoState}\text{\d{$\wedge$}
%         \smallrecord{\smalltfield{private}{\smallrecord{
%               \smalltfield{agenda}{\smallrecord{
%                   \smalltfield{fst}{\textit{RecType}}\\
%                   \smalltfield{rst}{$\mathrm{list}(\textit{RecType})$}}}}}}}}
%     \infer[enth]1{:_A
%       s_{i,A}.\text{private}.\text{agenda}.\text{fst}!}
%   \end{prooftree}

  
% \item[\textnormal{\textsc{DowndateAgenda}}]
%   \mbox{}

%   \hspace*{-2.5em}
%   \begin{prooftree}
%     \hypo{s_{i,A}:_A T_{\mathrm{curr}}}
%     \hypo{T_{\mathrm{curr}}\sqsubseteq\text{
%         \smallrecord{
%           \smalltfield{private}{\smallrecord{
%               \smalltfield{agenda}{\smallrecord{
%                   \smalltfield{fst}{\textit{RecType}}\\
%                   \smalltfield{rst}{$\mathrm{list}(\textit{RecType})$}}}}}}}}
%     \hypo{u^*:_A s_{i,A}.\text{private}.\text{agenda}.\text{fst}}
%     \infer[enth]3{s_{i+1,A}:_A
%       T_{\mathrm{curr}}\text{\fbox{\d{$\wedge$}}
%         \smallrecord{
%           \smalltfield{private}{\smallrecord{
%               \smallmfield{agenda}{$s_{i,A}$.private.agenda.rst}{$\mathrm{list}(\textit{RecType})$}}}}}}
%   \end{prooftree}
  
% \item[\textnormal{\textsc{AccGB}} New!] See p.~\pageref{ex:AccGBfinal}.

  
% \item[\textnormal{\textsc{AccLTM}} New!] See p.~\pageref{ex:AccLTM}.
  
% \item[\textnormal{\textsc{AccNM}} New!] See p.~\pageref{ex:AccNM}.
  
% \item[Control regime for accommodation New!] \mbox{}

%   \begin{subex} 
 
% \item if there is a labelling, $\eta$, such that
% $s_{i,A}^{\text{tot}}.\text{gb}(s_{i,A}^{\text{tot}}).\text{ltm}.\text{shared}.\text{commitments}\sqsubseteq[u^*.\text{cont}.\text{bg}]_\eta$,
%   then use \text{AccGB} with $\eta$ 
 
% \item else if there is a labelling, $\eta$, such that
%   $s_{i,A}^{\text{tot}}.\text{ltm}\sqsubseteq[u^*.\text{cont}.\text{bg}]_\eta$
%   then use \text{AccLTM} with $\eta$

  
% \item else use \textsc{AccNM}
 
% \end{subex} 

% \end{description}

\subsection{English resources} 

\subsubsection{Types and predicates} (as in Chapter~\ref{ch:intensional})

 % \begin{description}

  
% \item[Basic phonological  types for words] \mbox{}

%   \{``Dudamel'', ``is'', ``a'', ``conductor'', ``Beethoven'',
%   ``composer'', ``Uchida'', ``pianist'', ``aha'', ``ok'', ``leaves''
%   , ``hugs'', ``dog'', ``nine'',
%   ``ninety'', ``find'' \textbf{New!}, ``seek'' \textbf{New!},
%   ``worship'' \textbf{New!}\}

% %\item [Witnesses for basic types] \mbox{}

% %  \begin{description}
% % \item[\textnormal{\textit{Ind}}] --- dudamel, beethoven, uchida :
% %   \textit{Ind} \textbf{No longer necessary for interpretation of
% %     proper names!}
% %   \end{description}

  
% \item[Predicates] \mbox{}
  
%   \begin{description}
  
%   \item[with arity \textnormal{$\langle\textit{Ind}\rangle$}]
%     \{conductor, composer, pianist, leave,  dog,
%     passenger\}
    
%   \item[with arity
%     \textnormal{$\langle\textit{Ind},\textit{Quant}\rangle$}] \{hug
%     \textbf{Revised!}, find \textbf{New!}, seek \textbf{New!}, worship
%     \textbf{New!}, want$_Q$ \textbf{New!}\}

%       $e$ : worship($a$,$\mathcal{Q}$) iff for some $T$
% \begin{enumerate} 
 
% \item $e$ : rbelieve($a$, $T$) 
 
% \item $T$ $\sqsubseteq_{\leadsto}$ $\mathcal{Q}$($\lambda
%   r$:\smallrecord{\smalltfield{x}{\textit{Ind}}}
%   . worship$^\dagger$($a$, $r$.x))
 
% \end{enumerate}
% \textbf{or} for some $T'$
% \begin{enumerate} 
 
% \item $e$ :$_{\underline{\varepsilon}}$ rbelieve($a$, $T$)

% \item $e$ :$_{\underline{\varepsilon}}$ pov($T'$, $T$)
 
% \item $T$\fbox{\d{$\wedge$}}$T'$ $\sqsubseteq_{\leadsto}$ $Q$($\lambda
%   r$:\smallrecord{\smalltfield{x}{\textit{Ind}}}
%   . worship$^\dagger$($a$, $r$.x)) 

% \end{enumerate}

% \bigskip

%     We restrict our attention to modal systems, $\mathbb{T}$, such
%     that
%     \begin{enumerate}
    
%     \item if $p\in\{\text{hug},\text{find}\}$ then
%     \begin{quote}
%       $p(a,\mathcal{Q})\approx_{\mathbb{T}}\mathcal{Q}(\ulcorner\lambda
%       r$:\smallrecord{\smalltfield{x}{\textit{Ind}}} . \smallrecord{\smalltfield{e}{$p^{\dagger}(a,
%           r.\text{x})$}}$\urcorner)$
%     \end{quote}
    
    
    
%   \item $\text{successful}(\text{seek}(a,\mathcal{Q}))\sqsubseteq_{\mathbb{T}}
%     \text{find}(a,\mathcal{Q})$

    
%   \item want$_Q$($a$,$Q$) $\approx_{\mathbb{T}}$
% want$^\dagger$($a$, $Q$($\ulcorner\lambda
% r$:\smallrecord{\smalltfield{x}{\textit{Ind}}} . have($a$, $r$.x)$\urcorner$))
% \end{enumerate}
  

%     \item[with arity
%   \textnormal{$\langle\textit{Rec},\textit{Rec}\rangle$}] --- \{rise
%   \}
  

%       $e$ : rise$(r,c)$ if
%   \begin{quote}
%     $r$ : \textit{AmbTempFrame},\\
%     $c$ : \textit{TempRiseEventCntxt} and \\
%     $e$ : \textit{TempRiseEvent}$(c)$ \d{$\wedge$}
%     \smallrecord{
%       \smalltfield{e}{\smallrecord{
%           \smallmfield{t$_0$}{$r$}{\textit{AmbTempFrame}}}}}
%   \end{quote}
%   \textbf{or} if
%   \begin{quote}
%     $r$ : \textit{PriceFrame},\\
%     $c$ : \textit{PriceRiseEventCntxt} and \\
%     $e$ : \textit{PriceRiseEvent}$(c)$ \d{$\wedge$}
%     \smallrecord{
%       \smalltfield{e}{\smallrecord{
%           \smallmfield{t$_0$}{$r$}{\textit{PriceFrame}}}}}
%   \end{quote}
%   \textbf{or} if
%   \begin{quote}
%     $r$ : \textit{LocFrame},\\
%     $c$ : \textit{LocRiseEventCntxt} and \\
%     $e$ : \textit{LocRiseEvent}$(c)$ \d{$\wedge$}
%     \smallrecord{
%       \smalltfield{e}{\smallrecord{
%           \smallmfield{t$_0$}{$r$}{\textit{LocFrame}}}}}
%   \end{quote}

  

  
% \item[with arity \textnormal{$\langle\textit{Rec}\rangle$}] ---
%   \{temperature\}
  
% $e$ : temperature$(r)$ if 
%   \begin{quote}
%     $r$ : \textit{AmbTempFrame} and $e=r$
%   \end{quote}

  
% \item[with arity
%   \textnormal{$\langle\textit{Ind},\textit{TravelFrame}\rangle$}] ---
%   \{take\_journey\}

%   $s$ : take\_journey($a$, $e$) iff $s=e$ and $e$.traveller = $a$

  
% \item[with arity
%   \textnormal{$\langle\textit{Ind},\textit{Ppty}\rangle$}] ---
%   \{want$_P$\}

%  We restrict our attention to modal systems, $\mathbb{T}$, such
%  that
%  \begin{quote}
%    want$_P$($a$, $P$) $\approx_{\mathbb{T}}$ want$^\dagger$($a$,
%    $P$(\smallrecord{\field{x}{$a$}}))
%  \end{quote}
  

% \item[with arity
%   \textnormal{$\langle\textit{Ind},\textit{RecType}\rangle$}]
%   --- \{believe \textbf{New!}, want$^{\dagger}$ \textbf{New!}\}

%   $e$ : believe($a$, $T$) if
%   \begin{quote}
%     $e$ : ltm($a$, $T'$) \\
%     and $T'\sqsubseteq_{\leadsto}T$
%   \end{quote}
%   \textbf{or} if
%   \begin{quote}
%     $e$ :$_{\underline{\varepsilon}}$ believe($a$, $T_1$)\\
%     $e'$ :$_{\underline{\varepsilon}}$ pov($T_2$, $T_1$)\\
%     and $T_1$\fbox{\d{$\wedge$}}$T_2 \sqsubseteq_{\leadsto}T$
%   \end{quote}

%   \bigskip

%   $e$ : want$^{\dagger}$($a$, $T$) if for some $T'$\\
%   \hspace*{2em} $e$ : des($a$, $T'$) \\
%   \hspace*{2em} and $T'\sqsubseteq_{\leadsto}T$

%   \textbf{or} if for some $T_1$ and $T_2$\\
%   \hspace*{2em} $e$ :$_{\underline{\varepsilon}}$ want$^{\dagger}$($a$, $T_1$)\\
%   \hspace*{2em} $e$ :$_{\underline{\varepsilon}}$ pov($T_2$, $T_1$) \\
%   \hspace*{2em} and $T_1$\fbox{\d{$\wedge$}}$T_2
%   \sqsubseteq_{\leadsto}T$
  
% \end{description}

% \item[Frame types] \mbox{}

%   \begin{description}

    
%   \item[\textnormal{\textit{DogFrame}}] ---
%     \record{
%       \tfield{x}{\textit{Ind}}\\
%       \tfield{e}{dog(x)}\\
%       \tfield{age}{\textit{Real}}\\
%       \tfield{c$_{\mathrm{age}}$}{age\_of(x,age)}}
                    
%   \item[\textnormal{\textit{TravelFrame}}] ---
%     \record{
%       \tfield{traveller}{\textit{Ind}}\\
%       \tfield{source}{\textit{Loc}}\\
%       \tfield{goal}{\textit{Loc}}}

    
%   \item[\textnormal{\textit{PassengerFrame}}] ---
%     \record{\tfield{x}{\textit{Ind}}\\
%               \tfield{e}{passenger(x)}\\
%               \tfield{journey}{\textit{TravelFrame}}\\
%               \tfield{c$_{\mathrm{travel}}$}{take\_journey(x, journey)}}


%           \end{description}

          
        
  
  

% \end{description}

 \subsubsection{Grammar} 

\begin{description}



\item[Lexical sign types] \mbox{}

  Let \textit{Lexicon} be the set of lexical sign types defined
  inductively as follows.  The
  following set is included in \textit{Lexicon}.

\begin{tabbing}
    \{\=Lex$_{\mathrm{PropName}}$(``Dudamel''), \\
    \> Lex$_{\mathrm{PropName}}$(``Beethoven''), \\
    \> Lex$_{\mathrm{Pron}}$(``he''), \\
    \> Lex$_{\mathrm{numeral}}$(``nine'', 9), \\
    \> Lex$_{\mathrm{numeral}}$(``ninety'', 90), \\ 
    \> Lex$_{\mathrm{IndefArt}}$(``a''), \\
    \> Lex$_{\mathrm{Universal}}$(``every''), \\
\> Lex$_{\mathrm{DefArt}}$(``the''),\\
\> Lex$_{\text{CommonNoun}}$(``composer'', \textit{Rec}, composer),\\
\> Lex$_{\text{CommonNoun}}$(``conductor'', \textit{Rec}, conductor), \\
\> Lex$_{\text{CommonNoun}}$(``dog'', \textit{Rec}, dog) (= $\Sigma_{\text{``dog''}}$), \\
\> RestrictCommonNoun(CommonNounIndToFrame($\Sigma_{\text{``dog''}}$),
\textit{DogFrame}),\\
\> Lex$_{\mathrm{CommonNoun}}$(``passenger'', \textit{Rec}, passenger) ($=\Sigma_{\text{``passenger''}}$), \\
\> RestrictCommonNoun(CommonNounIndToFrame($\Sigma_{\text{``passenger''}}$),
\textit{PassengerFrame}), \\
\> Lex$_{\text{CommonNoun}}$(``temperature'', \textit{Rec},
temperature) (= $\Sigma_{\text{``temperature''}}$), \\
\> RestrictCommonNoun($\Sigma_{\text{``temperature''}}$,
\textit{AmbTempFrame}),\\
\> Lex$_{\mathrm{IntransVerb}}$(``leave'', \textit{Rec}, leave), \\
\> Lex$_{\mathrm{IntransVerb}}$(``run'', \textit{Rec}, run), \\
\> Lex$_{\mathrm{IntransVerb}}$(``rise'', \smallrecord{\smalltfield{$\mathfrak{c}$}{\textit{TempRiseEventCntxt}}},
rise), \\
\> Lex$_{\mathrm{IntransVerb}}$(``rise'', \smallrecord{\smalltfield{$\mathfrak{c}$}{\textit{PriceRiseEventCntxt}}},
rise), \\
\> Lex$_{\mathrm{IntransVerb}}$(``rise'', \smallrecord{\smalltfield{$\mathfrak{c}$}{\textit{LocRiseEventCntxt}}},
rise), \\
\> Lex$_{\mathrm{TransVerb}}$(``hug'', \textit{Rec}, hug), \\
\> Lex$_{\mathrm{TransVerb}}$(``find'', \textit{Rec}, find), \\
\> Lex$_{\mathrm{TransVerb}}$(``seek'', \textit{Rec}, seek), \\
\> Lex$_{\mathrm{TransVerb}}$(``worship'', \textit{Rec}, worship), \\
\> Lex$_{\mathrm{be}_{\text{ID}}}$(``is''), \\
\> Lex$_{\mathrm{be}_{\text{scalar}}}$(``is''), \\
\> Lex(``ok'', \textit{S}),  \\
\> Lex(``aha'', \textit{S})  \}
\end{tabbing}

\begin{description}
  
\item[Transitive verbs as verb phrases New!] \mbox{}

If $\Sigma$ = Lex$_{\text{TransVerb}}$($T_{\text{Phon}}$,
$T_{\text{bg}}$, $p$), for some $T_{\text{Phon}}$, $T_{\text{bg}}$ and
$p$, and $\Sigma\in\textit{Lexicon}$, then
TransVerbToVerbPhrase($\Sigma$) $\in$ \textit{Lexicon}.
\end{description}

\item[Constituent structure rule components] \mbox{} 
  \begin{description}

    \item[\textnormal{CnstrIsA}] \mbox{}

  $\lambda
u$:\textit{V}\d{$\wedge$}\smallrecord{\smalltfield{s-event}{\smallrecord{\smalltfield{e}{``is''}}}}$^{\frown}$\textit{NP}\d{$\wedge$}\smallrecord{\smalltfield{syn}{\smallrecord{\smalltfield{daughters}{\textit{Det}\d{$\wedge$}\smallrecord{\smalltfield{s-event}{\smallrecord{\smalltfield{e}{``a''}}}} \\
                                                                    \hspace*{5em}$^{\frown}$
\textit{N}\d{$\wedge$}\smallrecord{\smalltfield{cont}{\textit{Ppty}}}}
}}}. \\
\hspace*{1em} \textit{VP}\d{$\wedge$}\smallrecord{\smallmfield{cont}{$u$[2].syn.daughters[2].cont}{\textit{Ppty}}} 

  \end{description}
  


\item[Constituent structure rules] \mbox{}

Let \textit{CSRules} be the set of constituent structure rules,
defined inductively as follows.  The following set is included in \textit{CSRules}.
  
  \begin{tabbing}
    \{\=\textit{S} $\longrightarrow$ \textit{NP VP} $\mid$ \textit{NP}$'$(\textit{VP}$'$:\textit{Ppty}):\textit{RecType},\\
    \>\textit{NP} $\longrightarrow$ \textit{Det N} $\mid$
    \textit{Det}$'$($_{\text{@\!@}}$\textit{N}$'$:\textit{PPpty}):\textit{PQuant},\\
    \>\textit{VP} $\longrightarrow$ \textit{V} \textit{NP}
    \d{\d{$\wedge$}} CnstrIsA, \\
    \>\textit{VP} $\longrightarrow$ \textit{V} \textit{NP} $\mid$
    \textit{V}$'$(\textit{NP}$'$:\textit{Quant}):\textit{Ppty}\}
  \end{tabbing}

  \begin{description}

    
  \item[Relative clauses New!] \mbox{}

    If $i$ and $j$ are natural numbers, then
    \begin{quote}
      \textit{Rel} $\longrightarrow$ \textit{NP}$_{\text{wh}_i}$
      \textit{S}/$j$ $\mid$
      \textit{NP}$_{\text{wh}_i}'$($_{\text{@}_{\text{wh}_{i,j}}}$\textit{S}/$j'$:\textit{PRecType}):\textit{PPpty}
    \end{quote}
    is a member of \textit{CSRules}

    \bigskip

    If $T$ is a type, then
    \begin{quote}
      $\textit{N}\longrightarrow{^T\textit{N}}\ {^T\textit{Rel}}\
      \mid\
      {^T\textit{N}}'(_{\text{@}_\&}{^T\textit{Rel}}':{^T\textit{PPpty}}):{^T\textit{PPpty}}$
    \end{quote}
    is a member of \textit{CSRules}

\end{description}

\end{description}


\section{Summary}

In this chapter we looked at a witness-based account of
quantification where we started by characterizing types of witness sets
for quantifiers.  This provides us with an
account of generalized quantifiers which is more in line with the
ideas expressed by
\cite{PurverGinzburg2004,GinzburgPurver2008,LueckingGinzburg2019} who
argue that clarification and anaphoric phenomena in dialogue motivate an approach
where quantifiers represent sets rather than sets of properties as in
Montague's classical approach.  We have argued that our approach
suggests the possibility of accounting for a range of anaphoric
phenomena and will provide some more detailed techniques for the
treatment of anaphora in Chapter~\ref{ch:underspec}.

In addition our witness-based account provides a natural approach to
a probabilistic account of quantification and we have suggested that
estimations of probability are used in dialogue exchanges involving
quantification in cases where it is obvious that the dialogue
participants could not know whether the quantified statement is true
but is able to estimate the probability of its truth based on the
dialogue participant's previous experience or knowledge.

We presented an account of witness conditions for quantification
ptypes based on two general patterns, one for monotone increasing
quantifiers and one for monotone decreasing quantifiers.  For a number
of quantifiers there is in addition a specific witness condition,
equivalent to the general one, which increases anaphoric possibilities
and which also provide types more closely related to the DRT treatment
of quantifiers.

Finally, in preparation for our treatment of quantifier scope
ambiguity and binding in Chapter~\ref{ch:underspec}, we sketched a
treatment of long distance dependencies where \textit{wh}-phrases are
treated as quantifiers which bind pronoun interpretations as arguments
to verbs which are in the content but not realized syntactically.
This is similar to proposals in categorial grammar \citep{Steedman2012}.

%%% Local Variables: 
%%% mode: latex
%%% TeX-master: "ttl"
%%% End: