Iatridou et al. (2001): Observations about the form and meaning of the perfect

Iatridou, Anagnostopoulou and Izvorski give the perfect a perfect time span, whose right boundary tense sets and whose left boundary the argument of a perfect-level adverbial sets, in or throughout which there is a bounded or unbounded eventuality. The adverbial is read inclusive or durative, quantifying over the subintervals of the span, and the aspect of the participle makes the eventuality bounded, the perfective, or unbounded, the imperfective, the progressive and the Bulgarian neutral. The universal perfect is the durative reading of an unbounded eventuality and holds at both boundaries by assertion; the inclusive reading is silent about the boundaries, which is why an unmodified perfect, whose covert adverbial is inclusive, is never universal and why the anteriority of the present perfect is derived rather than encoded. A bounded eventuality that takes time holds throughout no span, so a perfect on a perfective participle, as in Greek, has no universal perfect, except where an activity fills the span exactly.

Main statements

• universal_at_rb, universal_at_lb: the universal perfect holds at both boundaries of the span.
• inclusive_silent_at_rb, unmodified_not_universal: the inclusive perfect does not assert the eventuality at the right boundary, so an unmodified perfect is never universal.
• span_lb_before_event: the left boundary is the adverbial's and may precede the eventuality.
• no_universal_of_prfv, bounded_activity_fills: a perfective participle blocks the universal perfect except for an activity filling the span.
• experiential_ends_by_rb, universal_not_anterior, future_perfect_underspecified: the anteriority of the perfect is derived from the span and tense.

Implementation notes

• The features [unbounded] and [bounded] of the paper's footnote 5 are Aspect.UNBOUNDED, the span inside the run time of an event, and Aspect.PRFV, the run time inside the span. The readings of the adverbial are Aspect.durative and Aspect.inclusive, quantification over the subintervals of the span, which the paper phrases both as every subinterval and as the points of the span. Over subintervals the durative unbounded reading is one event containing the span, the last paraphrase in (18b).
• The paper glosses inclusive as properly included in prose and writes plain existential quantification over the span in (18e) and (19c); the formulas are followed, and the consequence the prose draws, that neither boundary is asserted to be part of the eventuality, is inclusive_silent_at_rb.
• The adverbial classes of (16), the two levels of adverbials and the position of for, (23)–(24), are lexical and syntactic premises. Perfect-level since t₀ admits the spans starting at t₀ under either reading; ever since, at least since, always and perfect-level for are durative; lately and the covert adverbial are inclusive; and a sentence-initial for is perfect-level because it has merged above the eventuality. The study states the consequences of the readings, not the classification.
• The Greek perfect participle is built on the perfective stem only, the Bulgarian imperfective and neutral participles are unbounded, and in English the progressive realizes [unbounded] on nonstatives while statives are nonprogressive under either feature, (42). These enter as the aspect operator the theorems take. The neutral is the paper's [unbounded] participle, not Smith's neutral viewpoint ViewpointType.neutral, whose definition the paper finds unclear.

TODO

• Vlach's stativity test separates the Bulgarian neutral, which fails it, (49a), from the imperfective, though both have the subinterval property; the test turns on the framing of a when-clause, which footnote 5 says the interval features do not predict.
• The Greek and Bulgarian participle facts belong in their languages' fragments once these record the aspect of the perfect participle.
• The individual-level facts (8) and (25)–(26), the reduced relatives of the addendum and the account of sentence-initial for by Merge height are syntactic and left in prose.

References

• [IAI01]
• [Mit88]
• [Vla93]
• [Dow79]
• [Smi97]

The four expansions of (43)

The perfect asserts a span in or throughout which there is a bounded or unbounded eventuality, (43), and the four combinations are (44a–d).

theorem IatridouEtAl2001.durative_unbounded {W : Type u_1} {T : Type u_2} {E : Type u_3} [LinearOrder T] [Event.TemporalTrace E T] {P : W → E → Prop} : Aspect.durative (Aspect.UNBOUNDED P) = Aspect.UNBOUNDED P

An unbounded eventuality throughout the span, (44a), is one event whose run time contains the span.

theorem IatridouEtAl2001.inclusive_unbounded_iff {W : Type u_1} {T : Type u_2} {E : Type u_3} [LinearOrder T] [Event.TemporalTrace E T] {P : W → E → Prop} {w : W} {i : NonemptyInterval T} : i ∈ Aspect.inclusive (Aspect.UNBOUNDED P) w ↔ ∃ (e : E), P w e ∧ (Event.τ e).Overlaps i

An unbounded eventuality in the span, (44b), is one event whose run time overlaps it.

theorem IatridouEtAl2001.inclusive_prfv {W : Type u_1} {T : Type u_2} {E : Type u_3} [LinearOrder T] [Event.TemporalTrace E T] {P : W → E → Prop} : Aspect.inclusive (Aspect.PRFV P) = Aspect.PRFV P

A bounded eventuality in the span, (44c), is one event whose run time lies inside it.

theorem IatridouEtAl2001.not_durative_prfv {W : Type u_1} {T : Type u_2} {E : Type u_3} [LinearOrder T] [Event.TemporalTrace E T] {P : W → E → Prop} {w : W} {i : NonemptyInterval T} (h : ∀ (e : E), P w e → (Event.τ e).toProd.1 < (Event.τ e).toProd.2) : i ∉ Aspect.durative (Aspect.PRFV P) w

A bounded eventuality that takes time, a telic one in (44d), holds throughout no span, since the span's points are among its subintervals and contain no such eventuality.

theorem IatridouEtAl2001.durative_prfv_of_eq {W : Type u_1} {T : Type u_2} {E : Type u_3} [LinearOrder T] [Event.TemporalTrace E T] {P : W → E → Prop} {w : W} {i : NonemptyInterval T} (hP : Aspect.HasSubintervalProperty P) {e : E} (he : P w e) (hτ : Event.τ e = i) : i ∈ Aspect.durative (Aspect.PRFV P) w

A bounded eventuality with the subinterval property whose run time is the span fills it, satisfying throughout and boundedness at once, the activity of (44d).

Point 1: the universal perfect at both boundaries

theorem IatridouEtAl2001.durative_at_rb {W : Type u_1} {T : Type u_2} [LinearOrder T] {p : W → Set (NonemptyInterval T)} {w : W} {t : T} (h : (w, t) ∈ Aspect.PERF (Aspect.durative p)) : NonemptyInterval.pure t ∈ p w

A durative perfect asserts the predicate at the right boundary, the time tense supplies, and so does one restricted by any adverbial.

theorem IatridouEtAl2001.durative_at_lb {W : Type u_1} {T : Type u_2} [LinearOrder T] {p : W → Set (NonemptyInterval T)} {w : W} {t t₀ : T} (h : (w, t) ∈ Aspect.PERF fun (x : W) => {pts : NonemptyInterval T | pts.toProd.1 = t₀} ∩ Aspect.durative p x) : NonemptyInterval.pure t₀ ∈ p w

With since t₀ a durative perfect asserts the predicate at the left boundary.

theorem IatridouEtAl2001.unbounded_pure_iff {W : Type u_1} {T : Type u_2} {E : Type u_3} [LinearOrder T] [Event.TemporalTrace E T] {P : W → E → Prop} {w : W} {t : T} : NonemptyInterval.pure t ∈ Aspect.UNBOUNDED P w ↔ ∃ (e : E), P w e ∧ t ∈ Event.τ e

The non-strict imperfective holds at a moment when the moment lies in the run time of an event.

theorem IatridouEtAl2001.universal_at_rb {W : Type u_1} {T : Type u_2} {E : Type u_3} [LinearOrder T] [Event.TemporalTrace E T] {P : W → E → Prop} {w : W} {t : T} (h : (w, t) ∈ Aspect.PERF (Aspect.durative (Aspect.UNBOUNDED P))) : ∃ (e : E), P w e ∧ t ∈ Event.τ e

The universal perfect holds at the right boundary, the utterance time in the present perfect, so (6a–b) are contradictions, and a past or future time in the past and future perfect, (7).

theorem IatridouEtAl2001.universal_at_lb {W : Type u_1} {T : Type u_2} {E : Type u_3} [LinearOrder T] [Event.TemporalTrace E T] {P : W → E → Prop} {w : W} {t t₀ : T} (h : (w, t) ∈ Aspect.PERF fun (x : W) => {pts : NonemptyInterval T | pts.toProd.1 = t₀} ∩ Aspect.durative (Aspect.UNBOUNDED P) x) : ∃ (e : E), P w e ∧ t₀ ∈ Event.τ e

With since t₀ the universal perfect holds at t₀, the observation of [Mit88].

theorem IatridouEtAl2001.universal_of_covers {W : Type u_1} {T : Type u_2} {E : Type u_3} [LinearOrder T] [Event.TemporalTrace E T] {P : W → E → Prop} {w : W} {t t₀ : T} {e : E} (he : P w e) (h₀ : t₀ ≤ t) (h₁ : (Event.τ e).toProd.1 ≤ t₀) (h₂ : t ≤ (Event.τ e).toProd.2) : (w, t) ∈ Aspect.PERF fun (x : W) => {pts : NonemptyInterval T | pts.toProd.1 = t₀} ∩ Aspect.durative (Aspect.UNBOUNDED P) x

One eventuality covering the span from t₀ to t makes the universal perfect with since t₀ true at t, (2a) and (18a).

Point 2: an unmodified perfect is silent about the right boundary

theorem IatridouEtAl2001.inclusive_silent_at_rb {W : Type u_1} {T : Type u_2} {E : Type u_3} [LinearOrder T] [Event.TemporalTrace E T] {w : W} {t : T} {e₀ : E} (h : (Event.τ e₀).toProd.2 < t) : (w, t) ∈ Aspect.PERF (Aspect.inclusive (Aspect.UNBOUNDED fun (x : W) (e : E) => e = e₀)) ∧ ∀ (e : E), (fun (x : W) (e : E) => e = e₀) w e → t ∉ Event.τ e

The inclusive perfect, the reading of the covert adverbial, is true of an eventuality that ended before the time of tense, so it does not assert the eventuality there, and She has been sick and I have been cooking can go on but she is fine now and but I'm done now, (9)–(12) and (15).

theorem IatridouEtAl2001.unmodified_not_universal {W : Type u_1} {T : Type u_2} {E : Type u_3} [LinearOrder T] [Event.TemporalTrace E T] {w : W} {t : T} {e₀ : E} (h : (Event.τ e₀).toProd.2 < t) : ¬∀ (P : W → E → Prop), (w, t) ∈ Aspect.PERF (Aspect.inclusive (Aspect.UNBOUNDED P)) → (w, t) ∈ Aspect.PERF (Aspect.durative (Aspect.UNBOUNDED P))

An unmodified perfect does not entail the universal perfect, which is therefore never its reading.

Point 3: the span is not the E–R interval

theorem IatridouEtAl2001.span_lb_before_event {W : Type u_1} {T : Type u_2} {E : Type u_3} [LinearOrder T] [Event.TemporalTrace E T] {w : W} {t lb : T} {e₀ : E} (h₁ : lb < (Event.τ e₀).toProd.1) (h₂ : (Event.τ e₀).toProd.2 ≤ t) : (w, t) ∈ Aspect.PERF fun (x : W) => {pts : NonemptyInterval T | pts.toProd.1 = lb} ∩ Aspect.inclusive (Aspect.PRFV fun (x : W) (e : E) => e = e₀) x

With since 1991 the span starts in 1991 while its only eventuality lies in the fall of 1993, (28), so the left boundary is set by the adverbial, not by the eventuality.

Point 4: the aspect of the participle

theorem IatridouEtAl2001.no_universal_of_prfv {W : Type u_1} {T : Type u_2} {E : Type u_3} [LinearOrder T] [Event.TemporalTrace E T] {P : W → E → Prop} {w : W} {t : T} (h : ∀ (e : E), P w e → (Event.τ e).toProd.1 < (Event.τ e).toProd.2) : (w, t) ∉ Aspect.PERF (Aspect.durative (Aspect.PRFV P))

A perfective participle on a predicate whose eventualities take time, a telic or a stative that the perfective makes inchoative, has no universal perfect, so none with any adverbial, in Greek (30) and (34), Bulgarian (35) and the English nonprogressives of (41).

theorem IatridouEtAl2001.prfv_pure_iff {W : Type u_1} {T : Type u_2} {E : Type u_3} [LinearOrder T] [Event.TemporalTrace E T] {P : W → E → Prop} {w : W} {t : T} : NonemptyInterval.pure t ∈ Aspect.PRFV P w ↔ ∃ (e : E), P w e ∧ Event.τ e = NonemptyInterval.pure t

The perfective holds at a moment when an event's run time is that moment.

theorem IatridouEtAl2001.bounded_activity_fills {W : Type u_1} {T : Type u_2} {E : Type u_3} [LinearOrder T] [Event.TemporalTrace E T] {P : W → E → Prop} {w : W} {t t₀ : T} {e : E} (hP : Aspect.HasSubintervalProperty P) (he : P w e) (h₀ : t₀ ≤ t) (hτ : Event.τ e = { fst := t₀, snd := t, fst_le_snd := h₀ }) : ((w, t) ∈ Aspect.PERF fun (x : W) => {pts : NonemptyInterval T | pts.toProd.1 = t₀} ∩ Aspect.durative (Aspect.PRFV P) x) ∧ ∃ (e' : E), P w e' ∧ t ∈ Event.τ e'

A perfective participle on an activity with apo 1990 mexri tora 'from 1990 until now' is true when an eventuality fills the span exactly, and then holds at the utterance time like a universal perfect, (45).

Point 5: anteriority derived

theorem IatridouEtAl2001.experiential_ends_by_rb {W : Type u_1} {T : Type u_2} {E : Type u_3} [LinearOrder T] [Event.TemporalTrace E T] {P : W → E → Prop} {w : W} {t : T} (h : (w, t) ∈ Aspect.PERF (Aspect.inclusive (Aspect.PRFV P))) : ∃ (e : E), P w e ∧ (Event.τ e).toProd.2 ≤ t

An experiential perfect places the end of its eventuality by the time of tense, before the utterance time in the present perfect and before a past time in the pluperfect, (1).

theorem IatridouEtAl2001.universal_not_anterior {W : Type u_1} {T : Type u_2} {E : Type u_3} [LinearOrder T] [Event.TemporalTrace E T] {P : W → E → Prop} {w : W} {t : T} (h : (w, t) ∈ Aspect.PERF (Aspect.durative (Aspect.UNBOUNDED P))) : ∃ (e : E), P w e ∧ ¬(Event.τ e).toProd.2 < t

The universal perfect is not anterior, since its eventuality has not ended at the time of tense, so an anteriority operator in the perfect would make it underivable.

theorem IatridouEtAl2001.future_perfect_underspecified {W : Type u_1} {T : Type u_2} {E : Type u_3} [LinearOrder T] [Event.TemporalTrace E T] {w : W} {t now : T} {e₁ e₂ : E} (h₁ : (Event.τ e₁).toProd.2 < now) (h₂ : now < (Event.τ e₂).toProd.1) (h₂' : (Event.τ e₂).toProd.2 ≤ t) : (∃ (P : W → E → Prop), (w, t) ∈ Aspect.PERF (Aspect.inclusive (Aspect.PRFV P)) ∧ ∀ (e : E), P w e → (Event.τ e).toProd.2 < now) ∧ ∃ (P : W → E → Prop), (w, t) ∈ Aspect.PERF (Aspect.inclusive (Aspect.PRFV P)) ∧ ∀ (e : E), P w e → now < (Event.τ e).toProd.1

In the future perfect the right boundary follows the utterance time now, and the eventuality may end before now or start after it.