The progressive

import Linglib.Semantics.Aspect.Progressive · namespace Aspect

The progressive is a modal operator. An event is in progress toward an event type when, in every best world of a circumstantial modal base for the event under that description, ranked by an ordering source of propositions that the event is not interrupted, some event of the type includes it as a nonfinal part. The base holds the facts relevant to whether the event is completed as an event of the type, so an event can be in progress toward a completion that never happens: Mary was drawing a circle does not entail Mary drew a circle. As an interval property, the progressive holds at the run times of the events in progress, and composes with the perfect and the tenses like the other viewpoint operators.

Over a totally realistic modal base the actual world is the only best world: there the progressive falls inside the imperfective over the actual world alone, which requires an actual event of the type, and the inference from progressive to perfective returns.

Main definitions

Aspect.NonfinalPart: an event includes another as a part whose run time is a nonfinal subinterval of its own.
Aspect.InProgress: an event is in progress toward an event type.
Aspect.PROG: the progressive as an interval property.

Implementation notes

Events are ordered by part-of, the mereological order of the event domain.
The modal base depends on the event and on its description, the ordering source on the event alone.

References

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

Declarations

e' includes e as a nonfinal part: e is part of e', and the run time of e is a nonfinal subinterval of that of e'.

def NonfinalPart L51–53

{E : Type u_1} {T : Type u_3} [PartialOrder E] [LinearOrder T] [Event.TemporalTrace E T] (e e' : E) :

Prop

NonfinalPart e e' = (e ≤ e' ∧ (Event.τ e).NonfinalSubinterval (Event.τ e'))

Used by InProgress, inProgress_iff, NonfinalPart.lt, InProgress.exists_of_isTotallyRealistic

Used in Portner1998

e is in progress toward the event type P at w when in every best world of the circumstantial base circ e P under the ordering source ni e, the propositions that e is not interrupted, some event of type P includes e as a nonfinal part.

def InProgress L55–60

{E : Type u_1} {W : Type u_2} {T : Type u_3} [PartialOrder E] [LinearOrder T] [Event.TemporalTrace E T] (circ : E → (W → E → Prop) → Modality.Background W) (ni : E → Modality.Background W) (e : E) (P : W → E → Prop) :

W → Prop

InProgress circ ni e P = Modality.necessity (circ e P) (ni e) fun (v : W) => ∃ (e' : E), NonfinalPart e e' ∧ P v e'

Built from

Used by PROG, inProgress_iff, mem_PROG, InProgress.exists_of_isTotallyRealistic

Used in Portner1998

The progressive of P holds at the run times of the events in progress toward P.

def PROG L62–65

W → Set (NonemptyInterval T)

PROG circ ni P w = Event.τ '' {e : E | InProgress circ ni e P w}

Built from

Used by mem_PROG, PROG_subset_IMPF

Over totally realistic modal bases the progressive falls inside the imperfective over the world of evaluation alone.

theorem PROG_subset_IMPF L85–92

{E : Type u_1} {W : Type u_2} {T : Type u_3} [PartialOrder E] [LinearOrder T] [Event.TemporalTrace E T] {circ : E → (W → E → Prop) → Modality.Background W} {ni : E → Modality.Background W} {P : W → E → Prop} {w : W} (hf : ∀ (e : E), (circ e P).IsTotallyRealistic) :

PROG circ ni P w ⊆ IMPF (fun (w : W) (x : NonemptyInterval T) => {w}) P w

Built from