2.1 Dependent typing

In this paper, we shall extend the simple type theory with dependent function types ( $\Pi$ -types) and a type $N$ of natural numbers (see Section 2.2.1 for a more detailed description).

To give semantic interpretations to action verbs as exemplified in the variable polyadicity problem, we shall employ dependent types $\mbox{TV-ADV}(n)$ and $\mbox{IV-ADV}(n)$ to help us describe the types of adverbial modification phrases for transitive verbs like ‘butter’ and intransitive verbs like ‘talk’, respectively. For specific numbers, we have

\begin{align*} \begin{array}{lcl} \mbox{TV-ADV}(0) & = & {\textbf {e}}\to {\textbf {e}}\to {\textbf {t}} \\ \mbox{TV-ADV}(1) & = & \mbox{ADV} \to {\textbf {e}}\to {\textbf {e}}\to {\textbf {t}} \\ \mbox{TV-ADV}(2) & = & \mbox{ADV} \to \mbox{ADV} \to {\textbf {e}}\to {\textbf {e}}\to {\textbf {t}} \\ \ldots \ \ldots && \\ &&\\[-12pt] \mbox{IV-ADV}(0) & = & {\textbf {e}}\to {\textbf {t}} \\ \mbox{IV-ADV}(1) & = & \mbox{ADV} \to {\textbf {e}}\to {\textbf {t}} \\ \mbox{IV-ADV}(2) & = & \mbox{ADV} \to \mbox{ADV} \to {\textbf {e}}\to {\textbf {t}} \\ \ldots \ \ldots && \\ && \\[-32pt] \nonumber \end{array} \end{align*}

where $\mbox{ADV}=({\textbf {e}}\to {\textbf {t}})\to ({\textbf {e}}\to {\textbf {t}})$ is the type of adverbial modification phrases. For instance, for transtive verbs like $butter$ , their semantic types are the following $\Pi$ -type:

\begin{equation*} \Pi n\colon N.\ \mbox{TV-ADV}(n) \end{equation*}

Any object $f$ of this type will first take a number argument $n$ , then $f(n)$ is of type $\mbox{ADV} \to \ldots \to \mbox{ADV} \to {\textbf {e}}\to {\textbf {e}}\to {\textbf {t}}$ , where $\mbox{ADV}$ occurs $n$ times. If $f$ is $butter$ , we then have

\begin{align*} \begin{array}{lcl} butter(0) & \colon & \mbox{TV-ADV}(0)\ =\ {\textbf {e}}\to {\textbf {e}}\to {\textbf {t}} \\ butter(1) & \colon & \mbox{TV-ADV}(1)\ =\ \mbox{ADV} \to {\textbf {e}}\to {\textbf {e}}\to {\textbf {t}} \\ butter(2) & \colon & \mbox{TV-ADV}(2)\ =\ \mbox{ADV} \to \mbox{ADV} \to {\textbf {e}}\to {\textbf {e}}\to {\textbf {t}} \\ \ldots && \end{array} \end{align*}

This is exactly what we have hoped for. More formal definitions will be given below.

2.2 Proposed solution to the variable polyadicity problem

In this section, we describe the formal mechanisms that extend Church’s simple type theory in order to define type-valued functions such as $\mbox{TV-ADV}$ . We shall first describe the system ${\mathcal{C}}^+$ , an extension of Church’s simple type theory $\mathcal{C}$ (Church Reference Church1940), as employed in Montague’s semantics (Montague Reference Montague1974), with dependent function types and a type of natural numbers, and then the proposed solution to the variable polyadicity problem.Footnote ⁸

2.2.1 The underlying type theory ${\mathcal{C}}^+$

Let $\mathcal{C}$ be Church’s simple type theory (Church Reference Church1940) as employed by Montague for formal semantics (Montague Reference Montague1974).Footnote ⁹ The type system $\mathcal{C}^+$ extends $\mathcal{C}$ with the type $N$ of natural numbers and dependent function types ( $\Pi$ -types). The inference rules for $\mathcal{C}^+$ consist of those for $\mathcal{C}$ and those for type constructors $\Pi$ and $N$ , all listed in Appendix A. We now give brief explanations of $\Pi$ -types and $N$ .

Dependent function types ( $\Pi$ -types). The dependent function type ( $\Pi$ -type) is a typical form of dependent type. If $A$ is a type, and $B[x]$ is also a type, where $B[x]$ can depend on an object $x$ of type $A$ , then $\Pi x:A.B[x]$ is a type. An object of $\Pi x:A.B[x]$ is a function $f$ that satisfies the following condition: for any $a\colon A$ , the type of $f(a)$ is $B[a]$ . Note that the type $B[a]$ of $f(a)$ , the result of applying $f$ to $a$ , depends on the input $a$ – that is why the $\Pi$ -type is a dependent type.

Here is a very simple example: assume that $Human$ is the type of human beings and, for any $x\colon Human$ , $Parent(x)$ is the type of parents of $x$ , then the $\Pi$ -type $\Pi x:Human. Parent(x)$ contains the functions $f$ as its objects: for any $h\colon Human$ , the type of $f(h)$ is $Parent(h)$ ; that is, $f(h)$ is either the father or the mother of $h$ .

The formal inference rules for the $\Pi$ -types can be found in Appendix A.2. Note that a (non-dependent) function type is just a special form of a $\Pi$ -type: $A\to B$ is just a notation for $\Pi x:A.B$ when $x$ does not occur free in $B$ .

The type $N$ of natural numbers. Besides the usual introduction, elimination and definition rules (see Appendix A.3), $N$ also has a large elimination rule:

\begin{equation*} \frac {{{\Gamma }\vdash n{\kern.5pt}\colon{\kern-1pt} N\ \ \ {\Gamma }\vdash C\ type\ \ \ {\Gamma },\ x:N,\ Y\ type \vdash f(x,Y) \ type}} {{\Gamma }\vdash {\mathcal E}_{N}(C,f,n)\ type} \end{equation*}

The above rule states that the elimination operator ${\mathcal E}_{N}$ is also large so that it allows one to define type-valued functions with $N$ as their domain – see the equality laws in Appendix A.3, according to which one can use induction on natural numbers to define functions (and, in particular, type-valued functions by means of large elimination). These include functions like $\mbox{TV-ADV}$ that is used to form dependent types $\mbox{TV-ADV}(n)$ , as informally described above and to be formally defined below.

Large elimination has been studied by many authors (see, e.g., Dybjer Reference Dybjer2000 for a discussion in the context of induction-recursion). An alternative to large elimination is to introduce a type universe that contains (the names of) $N$ and $\Pi$ -types as its objects. The presence of such a universe also allows one to define type-valued functions such as $\mbox{TV-ADV}$ . That is why, in full modern type theoies such as Martin-Löf’s type theory (Nordström, Petersson and Smith Reference Nordström, Petersson and Smith1990) and UTT (Luo Reference Luo1994) (see Section 4.1), we do not need large elimination anymore since they already contain universes. In a way, to allow large elimination for $N$ , we have opted for ‘simplicity’ without introducing another notion (i.e., type universe). However, it should be noted that, to do it this way, we have not gone beyond ordinary dependent type theory.

2.2.2 Description of the proposal

Let $\mbox{ADV} = ({\textbf {e}}\to {\textbf {t}})\to ({\textbf {e}}\to {\textbf {t}})$ (as above). The (semantics of) transitive verbs such as $butter$ have type

(11) \begin{align} butter \colon \Pi n\colon N.\ \mbox{TV-ADV}(n) \end{align}

where $\mbox{TV-ADV}$ is a type-valued function, defined by induction on $N$ as:

(12) \begin{align} &\mbox{TV-ADV}(0) = {\textbf {e}}\to {\textbf {e}}\to {\textbf {t}} \end{align}

(13) \begin{align} &\mbox{TV-ADV}(n+1) = \mbox{ADV} \to \mbox{TV-ADV}(n) \end{align}

Similarly, the intransitive verbs such as $talk$ have type

(14) \begin{align} talk \colon \Pi n\colon N.\ \mbox{IV-ADV}(n) \end{align}

where $\mbox{IV-ADV}$ is defined as:

(15) \begin{align} &\mbox{IV-ADV}(0) = {\textbf {e}}\to {\textbf {t}} \end{align}

(16) \begin{align} &\mbox{IV-ADV}(n+1) = \mbox{ADV} \to \mbox{IV-ADV}(n) \end{align}

Then, intransitive/transitive verb phrases such as talk/butter can be defined as the following Example 2.1 shows.

Example 2.1 (butter). Let $\mbox{BUTTER} \colon {\textbf {e}}\to {\textbf {e}}\to {\textbf {t}}$ be the semantic interpretation of ‘butter’ in a sentence with no adverbial modification phrases such as ( 1) . Then, the semantics of transitive verb ‘butter’, of type (11), can be defined as follows, where in (18), $n\in \omega$ and $\overline {adv}_k$ stands for the sequence $adv_1,\ldots ,adv_k$ for $k\ge 0$ (when $k=0$ , $\overline {adv}_k$ is the empty sequence):

(17) \begin{align} &butter(0) = \mbox{BUTTER} (or, butter(0,x,y) = \mbox{BUTTER}(x,y)) \end{align}

(18) \begin{align} &butter(n+1, \overline {adv}_{n+1}, x, y) = butter(n, \overline {adv}_n, x, y)\ \&\ adv_{n+1}(\mbox{BUTTER}(x),y) \end{align}

The sentence (2), repeated here as (19), has semantics (20), where $j,\ toast\colon {\textbf {e}}$ and $with\_knife,\ in\_kitchen\colon \mbox{ADV}$ (as explained in Section 1.1):

(19) \begin{align} & \textit{John buttered the toast with the knife in the kitchen.} \end{align}

(20) \begin{align} &butter(2,with\_knife,in\_kitchen,j,toast) \end{align}

Actually, (20) is equal to the following formula:

(21) \begin{align} \mbox{BUTTER}(j,toast)\ \&\ with\_knife(\mbox{BUTTER}(j),toast)\ \&\ in\_kitchen(\mbox{BUTTER}(j),toast) \end{align}

which is the basic semantics $\mbox{BUTTER}(j,toast)$ in conjunction with two formulas that interpret the adverbial modification phrases. It is not difficult to see the equality between (20) and (21): it can easily be verified by means of the above definition of $butter$ in (17) and (18), according to which we have

(22) \begin{align} &butter(2,with\_knife,in\_kitchen,j,toast) \\ &= butter(1,with\_knife,j,toast) \ \&\ in\_kitchen(\mbox{BUTTER}(j),toast) \nonumber \\ &= butter(0,j,toast)\ \&\ with\_knife(\mbox{BUTTER}(j),toast)\ \&\ in\_kitchen(\mbox{BUTTER}(j),toast) \nonumber \\&= \mbox{BUTTER}(j,toast)\ \&\ with\_knife(\mbox{BUTTER}(j),toast)\ \&\ in\_kitchen(\mbox{BUTTER}(j),toast)\nonumber \end{align}

What we have shown, as illustrated by the above example for $butter$ , is that the extra types in $\mathcal{C}^+$ ( $\Pi$ -types and $N$ ) can provide useful means to manipulate logical expressions in semantic construction. In particular, we can represent semantic interpretations so that they can take one of the following two forms:

• • VP-form:Footnote ¹⁰ A semantic interpretation of an action verb can take a ‘VP-form’ where its semantics takes as arguments the adverbial modifiers as well as the subject/object. For instance, the semantics of ‘butter’ takes a VP-form in (20) to interpret (19).

• • Conjunctive form: The VP-form of a semantic interpretation is the same as (or equal to) a ‘conjunctive form’ where the base meaning of the action verb, applied to its subject/object, is in conjunction with the semantics of each of the adverbial modifiers. For instance, (21) is the conjunctive form of the semantics of (19), where the base meaning of ‘butter’ is $\mbox{BUTTER}$ and each adverbial modifier is interpreted as $adv(\mbox{BUTTER}(j),toast)$ with $adv$ being the semantics of the modifier.

For sentences with adverbial modifications, the VP-forms allow us to represent their semantic interpretations as formulas in terms of variable polyadicity of action verbs (cf., Davidson’s variable polyadicity problem – see Section 1.1), while the conjunctive form, equal to the VP-form, brings about many advantages obtainable from an event-based semantics.

An action verb has a single semantics, although it is parameterised by different numbers $n$ when used in semantic constructions for sentences with $n$ adverbial modifiers. For example, $butter$ is the semantics for ‘butter’ and $butter(n)$ is the predicate to be used for sentences with $n$ adverbial modifiers. For different numbers $n$ , $butter(n)$ ’s are different predicates – they take different numbers of arguments (in particular, $n$ adverbial modifiers) to form logical propositions. The relationship between $butter(n)$ for different $n$ is as expected. For example, for $butter$ we haveFootnote ¹¹

(23) \begin{align} butter(n+1,\overline {adv}_{n+1},x,y) \supset butter(n,\overline {adv}_{n},x,y) \end{align}

where $adv_i$ ’s are semantics of the adverbial modifiers. Because of the above, we can deduce, for example,

(24) \begin{align} &butter(2,with\_knife,in\_kitchen,j,toast) \\ &\supset butter(1,with\_knife,j,toast) \nonumber \\ &\supset butter(0,j,toast)\nonumber \end{align}

Note that because $butter(0,j,toast) = \mbox{BUTTER}(j,toast)$ by definition, we have that (the VP-form of) the semantics of (2) implies that of (1), as expected.

In general, we have

• • for the semantics $TV$ of any transitive verb phrase such as ‘butter’,

  \begin{equation*} \qquad TV(n+1,\overline {adv}_{n+1},x,y) \supset TV(n,\overline {adv}_{n},x,y) \end{equation*}

• • for the semantics $IV$ of any intransitive verb phrase such as ‘talk’,

  \begin{equation*} \qquad IV(n+1,\overline {adv}_{n+1},x) \supset IV(n,\overline {adv}_{n},x) \end{equation*}

Note that, just like event semantics, we have obtained the expected inference relationships between such sentences concerning their adverbial modifiers without resorting to meaning postulates (or events).

Commutativity of adverbial modifiers is an (arguably small) advantage of event semantics (see, e.g., Landman’s lecture notes; Landman Reference Landman2000), although one might have to impose meaning postulates to achieve this in the Montague semantics (c.f., Footnote 2). For instance, the semantics of the following two sentences should be logically equivalent (their adverbial modifiers are swapped):

(25) \begin{align} \textrm {John buttered the toast with the knife in the kitchen.} \end{align}

(26) \begin{align} \textrm {John buttered the toast in the kitchen with the knife.} \end{align}

This commutativity is true for our proposed semantic representation because it has the conjunctive form (and because the conjunction operator $\&$ is commutative). To explain this in more details, the VP-forms of the semantics of (25) and (26) are (27) and (28), respectively, with the arguments $with\_knife$ and $in\_kitchen$ swapped:

(27) \begin{align} butter(2,with\_knife,in\_kitchen,j,toast) \end{align}

(28) \begin{align} butter(2,in\_kitchen,with\_knife,j,toast) \end{align}

It is not difficult to see that their corresponding conjunctive forms are only different because two of the conjuncts are swapped, and therefore, those two conjunctive forms are logically equivalent. As a consequence, the VP-forms (27) and (28) are logically equivalent, too.

Remark. The above proposal has been implemented in the Coq proof development system (The Coq Team (2007)) for the ‘butter’ example, including the above inference relationship (23) as a theorem – see Appendix B.1 .

2.3 Remarks

Our above proposal is based on the extension $\mathcal{C}^+$ of simple type theory. Two remarks about the above approach are in order, and they will be further elaborated in Section 4.

1. 1. First of all, the approach is natural from a type-theoretical point of view (c.f., Section 4.1). In fact, $\mathcal{C}^+$ is (essentially) a subsystem of UTT (Luo Reference Luo1994), one of the modern type theories (Martin-Löf Reference Martin-Löf1984; The Coq Team 2007; HoTT 2013) implemented in proof assistants with applications such as formalisations of mathematics and program verification (and also linguistic semantics; Chatzikyriakidis and Luo Reference Chatzikyriakidis and Luo2017; Luo Reference Luo2024). One may take this as saying that the proposal is not based on a change of the underlying logic made specifically to solve the variable polyadicity problem (c.f., Footnote 6); instead, it is based on a formal system studied for a much more general purpose.

2. 2. Compared with events in event semantics, the extensions to obtain $\mathcal{C}^+$ from $\mathcal{C}$ is non-ontological and may be called, in Quine’s terminology (Quine Reference Quine1951), ideological (c.f., Section 4.2). In other words, we have employed additional mechanisms for manipulating logical expressions. They may also be called syntactical mechanisms and have nothing to do with ontological existence.

3.1 Event talks and time

The notion of event is closely related to time, as an event is naturally associated with the time at which it occurs. However, there seems to be an important difference: tense and aspect exist in language and, therefore, times already occur in expressions in most (if not all) sentences, while events do not – events only occur in some sentences that refer to them directly. Put in another way, time appears at the surface level in most sentences, whilst events do not. That explains why it is natural for people to consider semantic frameworks with time as one of their key elements, whilst having events as an ontological commitment may be more questionable.

Parsons (Reference Parsons1990) gave some examples of ‘event talks’ as evidence for event semantics – the following are such examples given by Parsons, where (29) involves explicit event reference, while (30)’s reference to events is implicit.

(29) \begin{align} &\textrm {After the singing of the Marseillaise, John saluted the flag.} \end{align}

(30) \begin{align} &\textrm {After the Marseillaise was sung, John saluted the flag.} \end{align}

Using event semantics, one can model these sentences as (31), where $after(e',e)$ is the formula expressing that event $e'$ happens after event $e$ .

(31) \begin{align} &\exists e.\ saluting(e)\ \&\ ag(e)=j\ \&\ pt(e)=flag \ \&\ \\ &\exists e'.\ singing(e') \ \&\ pt(e')=M \ \&\ after(e',e)\nonumber \end{align}

If we use $t_e$ to express the time at which event $e$ takes place, then $after(e',e)$ can be equivalently expressed as $t_e \lt t_{e'}$ .

Many of such cases as the above are concerned with times at which events take place, and their semantics can be given in a semantic framework that already has times expressible for dealing with tensed sentences, without resorting to events. For example, in such a framework, the semantics of (29) or (30) can be given as (32):

(32) \begin{align} \exists t,t'.\ sing(j,M,t)\ \&\ salute(j,flag,t')\ \&\ t\lt t' \end{align}

where a semantic predicate for an action verb takes one more argument, expressing the time that the action takes place. For example, $sing(j,M)$ becomes $sing(j,M,t)$ , and similarly for $salute$ .Footnote ¹²

Another example Parsons considers involves event quantification: for the sentence (33), he gives event semantics (34), where the formula $IN(e,e')$ is undefined:

(33) \begin{align} &\textrm {In every burning, oxygen is consumed.} \end{align}

(34) \begin{align} &{\forall } e.\ burning(e)\supset \exists e'.\ consuming(e')\ \&\ pt(e')=O_2\ \&\ IN(e,e') \end{align}

Such sentences can also be given semantics in a timed framework, without using events. For instance, the above sentence (33) may be given the following semantics (35).

(35) \begin{align} {\forall } x {\forall } t.\ burn(x,t) \supset consume(O_2,t) \end{align}

To rephrase (35), in every burning $x$ that takes place at $t$ , oxygen is consumed at $t$ as well. We contend that this also represents the semantics correctly, without using events.

3.2 Perception words

Another case that Parsons (Reference Parsons1990) puts forward is how to give suitable semantics to a sentence that features a perceptual verb followed by a clause lacking explicit tense, as exemplified by the following sentence.

(36) \begin{align} \textrm {Mary saw John leave.} \end{align}

Let’s assume that the semantic type of ‘see’ be ${\textbf {e}}\to {\textbf {e}}\to {\textbf {t}}$ . The question is what the semantic type of ‘leave’ should be. A usual semantics for verbs would not work for, if $leave$ were of type ${\textbf {e}}\to {\textbf {t}}$ , then (37) would not be well-typed and, hence, cannot be considered as the semantics of (36):

(37) \begin{align} (\#) see(m,leave(j)) \end{align}

One may ask: what if we take $see$ ’s type to be ${\textbf {e}}\to {\textbf {t}}\to {\textbf {t}}$ ? Yes, in that case, (37) would be well-typed. However, there is a problem: in that case, (37) would not be suitable as the semantics of (36) because it is closer to the meaning of the following sentence with a that-clause:

(38) \begin{align} \textrm {Mary saw that John left.} \end{align}

The above (38) has a different meaning from (36): with the that-clause, it means that Mary became aware that the leaving event took place (usually without seeing it directly).

In event semantics, the above problem can be resolved because individual-like entities (events of type $\textbf {e}$ ) are introduced for actions associated with verbs and the verbs are all interpreted as predicates over events, of type ${\textbf {e}}\to {\textbf {t}}$ . For example, the event semantics of (36) can be (39):

(39) \begin{align} &\exists e.\ see(e)\ \&\ ag(e)=m \ \&\ \\ &\exists e'.\ leave(e')\ \&\ ag(e')=j \ \&\ pt(e)=e'\nonumber \end{align}

The key is that the entity $e'$ is now available to be the patient of $e$ ; that is, $e'$ is the event seen in the event $e$ . The event-based analysis models this by treating the embedded clause as an event perceived by the subject.

We contend that interpretating such sentences involving perceptual verbs does not necessarily require us to use event semantics, where events are introduced in general as ontological commitments for all sentences. Instead, we’d only need to do something in such special cases as interpreting perceptual verbs with tenseless clauses. Note that the introduction of events has essentially turned an action (John’s leaving in (36)) into an entity (the event $e'$ in (39)), so that one can use $e'$ in semantic construction. A similar thing can be done without introducing events in general – here is our proposal, which we explain for sentence (36).

We assume that, as usual, the verbs ‘see’ and ‘leave’ have semantic types (40) and (41), respectively, where we choose to use $\textrm {LEAVE}$ instead of $leave$ because we will use the latter below for the general semantics of ‘leave’ for which $\textrm {LEAVE}$ becomes a special case:

(40) \begin{align} see\colon {\textbf {e}}\to {\textbf {e}}\to {\textbf {t}} \end{align}

(41) \begin{align} \textrm {LEAVE}\colon {\textbf {e}}\to {\textbf {t}} \end{align}

In order to interpret (36), we consider a special mapping $\mathbf{E}$ , of type ${\textbf {t}}\to {\textbf {e}}$ , which turns a logical formula into an entity: for example, $\mathbf{E}(\textrm {LEAVE}(j))\colon {\textbf {e}}$ .Footnote ¹³ Then, the sentence (36) can be interpreted as (42):

(42) \begin{align} see(m, \mathbf{E}(\textrm {LEAVE}(j))) \end{align}

We emphasise that introducing the mapping $\mathbf{E}$ is only for the interpretation of such sentences involving perceptual verbs, not in general. Put in another way, event-like entities are not introduced in general as ontological commitments, but only when they are absolutely needed in special cases (and, in this case, for perceptual verbs).

There is a further issue one may raise: what if one adds adverbial modifiers to the senseless verb ‘leave’ in (36), as exemplified by the following sentences (43) and (44), where one and two adverbial modifiers are added, respectively:

(43) \begin{align} &\textrm {Mary saw John leave quickly.} \end{align}

(44) \begin{align} &\textrm {Mary saw John leave quickly and quietly.} \end{align}

To interpret such sentences as (36), (43) and (44) in general, we need to consider the general interpretation of verb phrases when a verb (e.g., ‘leave’) takes arbitrarily many adverbial modifiers (c.f., the definition of $butter$ in Section 2.2.2). For ‘leave’, its semantics is of the following type (for intransitive verbs, as (14) in Section 2.2.2):

(45) \begin{align} leave \colon \Pi n\colon N.\ \mbox{IV-ADV}(n) \end{align}

where $\mbox{IV-ADV}$ ’s definition is given in (15) and (16) in Section 2.2.2. We can now define the semantics of the ‘leave-phrases’ as follows:

(46) \begin{align} &leave(0,x) = \textrm {LEAVE}(x) \end{align}

(47) \begin{align} &leave(n+1, \overline {adv}_{n+1}, x) = leave(n, \overline {adv}_n, x)\ \&\ adv_{n+1}(\textrm {LEAVE}, x) \end{align}

The semantics of (36), (43) and (44) can now be given as (48), (49) and (50), respectively.

(48) \begin{align} &see(m, \mathbf{E}(leave(0,j))) \end{align}

(49) \begin{align} &see(m, \mathbf{E}(leave(1,quickly,j))) \end{align}

(50) \begin{align} &see(m, \mathbf{E}(leave(2,quickly,quietly,j))) \end{align}

In order to obtain the desired inference relationships between sentences with such a structure, we need to impose the following meaning postulate: for $see$ and $leave$ , we assume (51), where $x\colon e$ , $n\colon N$ and $adv_i\colon ({\textbf {e}}\to {\textbf {t}})\to ({\textbf {e}}\to {\textbf {t}})$ .

(51) \begin{align} see(x, \mathbf{E}(leave(n+1, \overline {adv}_{n+1}, x))) \supset see(x, \mathbf{E}(leave(n, \overline {adv}_n, x))) \end{align}

Of course, because of (51) and the transitivity of logical implication, we can prove the following (52):

(52) \begin{align} see(x,\mathbf{E}(leave(n, \overline {adv}_n, x)))\supset see(x,\mathbf{E}(leave(m, \overline {adv}_m, x))) \end{align}

for any natural numbers $m\le n$ .

With this, it is easy to see that (50) $\supset$ (49) $\supset$ (48), that is, informally we have: (44) implies (43) implies (36), as expected.

Note that the meaning postulate (51) does not cover everything we expect to hold. For example, consider the following sentence (53), where ‘and’ connects two clauses ‘John leave’ and ‘Kevin run’. Then, intuitively, it would be the case that (53) implies (36) which, strictly speaking, is not covered by (51). However, in this case, one may argue that (54) rephrases (53) and therefore, because (54) implies (36), we are OK.

(53) \begin{align} &\textrm {Mary saw John leave and Kevin run.} \end{align}

(54) \begin{align} &\textrm {Mary saw John leave and Mary saw Kevin run.} \end{align}

3.3 Nominalisation: A discussion

The introduction of an entity to stand for an action has naturally provided an elegant solution to semantic understanding of nominalisation. For example, consider the sentence (55), where both ‘talked’ and its nominalisation ‘the talk’ occur. In its event semantics (56), the event variable $e$ is the entity that corresponds to the talking action performed by John.

(55) \begin{align} \textrm {John talked and the talk was interesting.} \end{align}

(56) \begin{align} \exists e.\ talking(e)\ \&\ ag(e)=j\ \&\ interesting(e) \end{align}

Because of the existence of the entity $e$ , one can then form $interesting(e)$ to say that the talking action is interesting as if it is the event $e$ . In this way, event semantics establishes the connection between action verbs and their nominalisations naturally, which one might even consider as a side effect when trying to resolve the VP problem.

It is arguable whether event semantics is essential in resolving the nominalisation problem. In the literature, there exist different approaches to deal with nominalisation including, for example, Chierchia’s work (Chierchia Reference Chierchia1984, Reference Chierchia1985). In these approaches, event semantics is not used. However, one may also argue that somehow event-like structures are employed in these approaches including, for instance, discourse referents in Discourse Representation Theory (Kamp Reference Kamp1981; Kamp and Reyle Reference Kamp and Reyle1993; Heim Reference Heim1982). In this paper, we shall not discuss these approaches in detail.