Docs / Studies / Studies.Dowty1979

Word Meaning and Montague Grammar: The Semantics of Verbs and Times in Generative Semantics and in Montague’s PTQ

Dowty, D. R. (1979). Springer

Source Bibliography Paper

In interval semantics a sentence is true at an interval of a world, and the progressive of a sentence is true at an interval that a longer interval of the sentence's truth extends into the future. On Bennett and Partee's analysis the longer interval lies in the same world, so John was drawing a circle entails John drew a circle, the imperfective paradox, and John was watching television when he fell asleep (28) requires the watching to have gone on after he fell asleep. Dowty makes the progressive modal. A first version (24) asks for some world exactly like the actual one up to the interval where the sentence is true at the longer interval, which gets (28) right but makes both the coin is coming up heads and the coin is coming up tails true of a coin in the air. The final version (25) quantifies over the inertia worlds, a primitive of the model: worlds exactly like the actual one up to the interval, in which events then take their natural course. A single longer interval must be one of the sentence's truth in every inertia world, so the coin comes up neither heads nor tails, and Bennett and Partee's progressive is the case where the actual world is the only inertia world.

For activities, true at every subinterval larger than a moment of an interval of their truth, the progressive at an interval larger than a moment entails the activity there, since the inertia worlds agree with the actual one up to it. Dowty observes that the entailment from x is V-ing to x has V-ed still fails for activities, like waltzing, whose shortest intervals are long, since the progressive holds within the first of them.

Implementation notes

  • Dowty's relation of an interval to a longer one, "I ⊂ I' and I is not a final subinterval for I'", is NonemptyInterval.NonfinalSubinterval (NonemptyInterval.nonfinalSubinterval_iff).
  • Sentences are sets of intervals at each world, the interval properties the aspect operators of the event semantics produce. Time is a linear order; the scenarios use the natural numbers, where Dowty takes the reals.
  • Exactly like up to a time is HistoricalAlternatives. Inertia worlds are an arbitrary function of a world and an interval; the theorems that need them to be historical alternatives take that as a hypothesis, together with the agreement of the sentence on intervals up to the time.
  • Dowty's branching-time progressive (p. 152) is stated over histories, which p. 153 lets take the role of worlds; branchingProg reads it so.

Errata

  • The branching-time progressive (p. 152) takes, for each inertia history, some longer interval of the sentence's truth, while (25) fixes one longer interval for every inertia world. The first is strictly weaker (they differ): when the inertia worlds complete a circle at different times, it makes John is drawing a circle true and (25) false. So the choice between the two formalizations matters for the progressive, contrary to p. 154. The branching definition also drops (25)'s requirement that the interval not be a final subinterval of the longer one, which its own gloss on p. 151 ("extending into some ... possible future") presupposes.

TODO

  • BECOME (11), (11'), Cresswell's AND (19), the futurate progressive of §3.7 and the stative progressives of §3.8.2 are not formalized.

References

  • Dowty 1979, Word Meaning and Montague Grammar: The Semantics of Verbs and Times in Generative Semantics and in Montague’s PTQ
  • Bennett & Partee 1972, Toward the Logic of Tense and Aspect in English
  • Taylor 1977, Tense and Continuity

Interval semantics

L88–91
L93–96
L98–102

Bennett and Partee's progressive is (25) with the actual world as its only inertia world.

theorem prog_singletonL106–109
{W : Type u_1} {T : Type u_2} [LinearOrder T] (φ : Sentence W T) :
prog (fun (w : W) (x : NonemptyInterval T) => {w}) φ = bennettPartee φ

Built from , ,

On Bennett and Partee's analysis the progressive of a sentence entails that the sentence is true at some interval of the actual world.

theorem exists_mem_of_mem_bennettParteeL111–114
{W : Type u_1} {T : Type u_2} [LinearOrder T] {φ : Sentence W T} {w : W} {I : NonemptyInterval T} (h : I ∈ bennettPartee φ w) :
∃ (I' : NonemptyInterval T), I' ∈ φ w

Built from ,

L116–118

An activity true at an interval is true at its subintervals larger than a moment (Taylor's (57), p. 166). When the inertia worlds are exactly like the actual one up to an interval larger than a moment, and the activity's truth at that interval is a fact of history, the progressive of the activity there entails the activity.

theorem mem_of_mem_progL120–132
{W : Type u_1} {T : Type u_2} [LinearOrder T] {φ : Sentence W T} {w : W} {I : NonemptyInterval T} {history : HistoricalAlternatives W T} {inertia : W → NonemptyInterval T → Set W} (hInr : ∀ (w : W) (I : NonemptyInterval T), inertia w I ⊆ history.metaphysicalBase w I.toProd.2) (hagree : ∀ v ∈ history.metaphysicalBase w I.toProd.2, I ∈ φ v ↔ I ∈ φ w) (hsub : ∀ (v : W) (J J' : NonemptyInterval T), J ≤ J' → ¬J.IsPoint → J' ∈ φ v → J ∈ φ v) (hne : (inertia w I).Nonempty) (hI : ¬I.IsPoint) (h : I ∈ prog inertia φ w) :
I ∈ φ w

Built from ,

Scenarios

Time is the natural numbers, and worlds are Bool.

L143
L145
L147–149

A coin in the air (pp. 147–148)

In world true the coin comes up heads over [0, 1], in world false tails. Both worlds are alike at 0, and both outcomes are a natural course of events, so both are inertia worlds.

Falling asleep in front of the television (28)

In world true John watches television over [0, 1] and falls asleep at 1; in world false, exactly like it up to 1, he watches on until 3. Watching is true at every subinterval of the watching.

A circle completed at different times

Both worlds are inertia worlds, and the drawing of the circle is completed over [0, 1] in one and over [0, 2] in the other.

Waltzing (p. 172)

Waltzing is true only of intervals of at least three steps, within the waltz from 0 to 6.

L222–223
L225–230

The paper's judgments

(24) gets the television right where Bennett and Partee's analysis does not, and (25) gets the coin right where (24) does not.

theorem truthValue_rowsL234–250
:
(iv 0 0 possibleProg_heads._proof_1 ∈ prog (fun (x : Bool) (x_1 : NonemptyInterval ℕ) => Set.univ) heads true ↔ Examples.coin_heads.feature? "truthValue" = some "true") ∧ (iv 0 0 possibleProg_heads._proof_1 ∈ prog (fun (x : Bool) (x_1 : NonemptyInterval ℕ) => Set.univ) tails true ↔ Examples.coin_tails.feature? "truthValue" = some "true") ∧ (iv 1 1 not_bennettPartee_watch._proof_1 ∈ possibleProg splitAfterOne watch true ↔ Examples.ex28.feature? "truthValue" = some "true") ∧ ¬(iv 0 0 possibleProg_heads._proof_1 ∈ possibleProg splitAfterZero heads true ↔ Examples.coin_heads.feature? "truthValue" = some "true") ∧ ¬(iv 1 1 not_bennettPartee_watch._proof_1 ∈ bennettPartee watch true ↔ Examples.ex28.feature? "truthValue" = some "true")

Built from , , , , , , , ,