Docs / Studies / Studies.Portner1998

The Progressive in Modal Semantics

Portner, P. (1998). Language, 74(4), 760–787

Portner keeps Dowty's idea that the progressive is a necessity operator over inertia worlds and explains which worlds those are with Kratzer's ordering semantics. The progressive of an event e under a description P quantifies over the best worlds of a circumstantial modal base, Circ(e, P), the facts relevant to whether e is completed as an event of type P, ranked by an ordering source NI(e), the propositions that e is not interrupted; it is true when in every such world some event of type P includes e as a nonfinal part. This is the progressive of the event semantics, Aspect.InProgress.

Since the modal base is fixed by what is internal to the event, a bus that hits Max halfway across the street is no part of it, and Max was crossing the street (11) comes out true where Dowty's inertia worlds, which contain the bus, make it false. Since the base also depends on the description, the same walk makes (11) true and Max was walking into the path of an oncoming bus (39) true, the latter under a base that includes the bus; no single base does both. A Mary of ordinary abilities was not wiping out the Roman army, whose defeat no world compatible with her abilities contains; a Mary who did wipe it out has the abilities that put such worlds in the base. These scenarios decide the paper's judgments, where the imperfective of the event semantics over the actual world alone, inside which the progressive over a totally realistic base falls (Aspect.PROG_subset_IMPF), gets (11) wrong.

Implementation notes

The scenarios take their events to be intervals of natural numbers, as in Landman1992, and constant backgrounds over three worlds.
The interval forms (14) and (32) quantify over inertia worlds before the longer interval, the reverse of Dowty's (3); the reversal is a weakening (Dowty1979.not_branchingProg_subset_prog).

TODO

The activity argument of §4.2 (Max is running, so he has run) needs temporal subevents, and the winning race (35) and the context dependence of (4) and (47) are not formalized.

References

Portner 1998, The Progressive in Modal Semantics
Dowty 1979, Word Meaning and Montague Grammar: The Semantics of Verbs and Times in Generative Semantics and in Montague’s PTQ formalized
Landman 1992, The Progressive formalized
Kratzer 1991, Modality

Declarations

L59–61

The bus (11), (39)

Max's walk so far is the event [0, 1]. In world crosses he gets across, his crossing being [0, 3]; in world hit, the actual one, the bus hits him, his walk into its path being [0, 2]; in world turnsAround he turns back.

A modal base fixed by the event alone cannot make both (11) and (39) true, so the base must depend on the description (p. 779).

theorem not_prog_crossing_and_walkIntoBus L114–124

(f : Modality.Background Bus) (hne : (Modality.bestWorlds f notInterrupted Bus.hit).Nonempty) :

¬(Aspect.InProgress (fun (x : NonemptyInterval ℕ) (x_1 : Bus → NonemptyInterval ℕ → Prop) => f) (fun (x : NonemptyInterval ℕ) => notInterrupted) (Dowty1979.iv 0 1 prog_crossing._proof_1) crossing Bus.hit ∧ Aspect.InProgress (fun (x : NonemptyInterval ℕ) (x_1 : Bus → NonemptyInterval ℕ → Prop) => f) (fun (x : NonemptyInterval ℕ) => notInterrupted) (Dowty1979.iv 0 1 prog_crossing._proof_1) walkIntoBus Bus.hit)

Built from , , ,

Dowty's progressive makes (11) false: the bus's hitting Max is the normal course of events, so the actual world is the inertia world, and there he does not cross (p. 764).

theorem not_dowtyProg_bus L126–130

Dowty1979.iv 0 1 prog_crossing._proof_1 ∉ Dowty1979.prog (fun (x : Bus) (x_1 : NonemptyInterval ℕ) => {Bus.hit}) (Landman1992.sentenceOf crossing) Bus.hit

Built from ,

L132–135

The Roman army (18)

Mary's fighting so far is the event [0, 1]. In world wipesOut she destroys the army, her wiping it out being [0, 10]; in killsDozens she defeats a few dozen soldiers; in killedEarly she is killed at once.

The paper's judgments

The progressive decides the paper's judgments, where Dowty's inertia worlds and the imperfective of the event semantics make (11) false.

theorem truthValue_rows L185–204

(Aspect.InProgress circ (fun (x : NonemptyInterval ℕ) => notInterrupted) (Dowty1979.iv 0 1 prog_crossing._proof_1) crossing Bus.hit ↔ Examples.ex11.feature? "truthValue" = some "true") ∧ (Aspect.InProgress circ (fun (x : NonemptyInterval ℕ) => notInterrupted) (Dowty1979.iv 0 1 prog_crossing._proof_1) walkIntoBus Bus.hit ↔ Examples.ex39.feature? "truthValue" = some "true") ∧ (Aspect.InProgress (fun (x : NonemptyInterval ℕ) (x_1 : Army → NonemptyInterval ℕ → Prop) => ordinary) (fun (x : NonemptyInterval ℕ) => defeatsSoldiers) (Dowty1979.iv 0 1 prog_crossing._proof_1) wipeOut Army.killedEarly ↔ Examples.ex18_ordinary.feature? "truthValue" = some "true") ∧ (Aspect.InProgress (fun (x : NonemptyInterval ℕ) (x_1 : Army → NonemptyInterval ℕ → Prop) => ⊥) (fun (x : NonemptyInterval ℕ) => defeatsSoldiers) (Dowty1979.iv 0 1 prog_crossing._proof_1) wipeOut Army.wipesOut ↔ Examples.ex18_hero.feature? "truthValue" = some "true") ∧ ¬(Dowty1979.iv 0 1 prog_crossing._proof_1 ∈ Dowty1979.prog (fun (x : Bus) (x_1 : NonemptyInterval ℕ) => {Bus.hit}) (Landman1992.sentenceOf crossing) Bus.hit ↔ Examples.ex11.feature? "truthValue" = some "true") ∧ ¬((Aspect.IMPF (fun (w : Bus) (x : NonemptyInterval ℕ) => {w}) crossing Bus.hit).Nonempty ↔ Examples.ex11.feature? "truthValue" = some "true")

Built from , , , , , , , ,