Pancheva (2003): Aspectual Makeup of Perfect Participles and the Interpretations of the Perfect

Pancheva gives the perfect one meaning: a perfect time span of which the reference interval is a final subinterval. The readings come from the viewpoint aspect the perfect embeds. The unbounded aspect, the span inside the run time of an event, gives the universal perfect; the neutral, the span overlapping an event that starts after it does, and the bounded, the run time properly inside the span, give two experiential perfects; and a resultative aspect over telic predicates, the span overlapping into the run time of the event's result state, gives the resultative perfect. Greek lacks the universal perfect because its perfect does not embed the unbounded aspect. When the span may start arbitrarily early the experiential and resultative perfects say only how the eventuality or the result state stands to the right boundary of the reference interval, and at a moment of reference the universal and the two experiential perfects are the three perfects of the older account by Iatridou, Anagnostopoulou and Izvorski.

Main statements

• universal_iff_unbounded, universal_at_rb: the universal perfect asserts the eventuality throughout the reference interval.
• neutral_experiential_iff, bounded_experiential_iff: the neutral experiential says the eventuality has begun by the right boundary of the reference interval, the bounded one that it has ended by it.
• resultative_state_at_rb, resultative_perfect_iff: the resultative perfect asserts the result state at the right boundary and beyond.
• bounded_perfect_iff_prfv_perfect: the proper containment of the bounded aspect makes no difference under the perfect.
• bounded_experiential_of_ends_at_rb: the bounded experiential is compatible with the eventuality holding at the moment of reference.
• universal_iff_durative_unbounded, neutral_experiential_iff_inclusive_unbounded, bounded_experiential_iff_inclusive_bounded: at a moment of reference the three perfects are those of Iatridou, Anagnostopoulou and Izvorski.
• neutral_span_not_covered, bounded_span_not_covered: without the unbounded aspect no perfect is universal.

Implementation notes

• The perfect is Aspect.perfect and the unbounded aspect Aspect.UNBOUNDED. The neutral relation of (7b) is strict, the interval having a point before every point of the event, so it is not Smith's neutral viewpoint ViewpointType.neutral, which lets the interval start with the event (neutral_subset_smith_neutral).
• The resultative takes a predicate of result states and their events, which only telic predicates denote, so an activity such as run in (5) has no resultative perfect by its type. The paper's formula (17) reads only the run time of the state.
• Theorems that let the perfect time span start before any given time assume that time has no first moment (NoMinOrder); without a perfect-level adverbial, which the paper's formulas do not include, the left boundary of the span is free.

TODO

• The claim that (16a–b) are incompatible with the utterance time lying in the event time does not follow from (15b): an event ending exactly at the utterance time satisfies it (bounded_experiential_of_ends_at_rb), as footnote 8's remark on endpoints anticipates. What follows is that the event does not continue past it (bounded_experiential_not_beyond_rb).
• The spell-out tables (20)–(21), the sequence-of-tense contrasts (24)–(25) and (37)–(39), and the parallelism argument (31) are left in prose; the paper proposes no formal account of the latter two.
• Perfect-level adverbials such as since 2000 in (1a) are not part of the paper's formulas.

References

• [Pan03]
• [IAI01]
• [Smi97]

The interval relations of (7b) and (17)

def Pancheva2003.OverlapsFromBefore {T : Type u_2} [LinearOrder T] (i j : NonemptyInterval T) : Prop

OverlapsFromBefore i j, the relation of the neutral aspect, holds when the two intervals overlap and i begins strictly before j.

Equations

• Pancheva2003.OverlapsFromBefore i j = (i.Overlaps j ∧ i.toProd.1 < j.toProd.1)

def Pancheva2003.OverlapsInto {T : Type u_2} [LinearOrder T] (i j : NonemptyInterval T) : Prop

OverlapsInto i j, the relation of the resultative aspect, holds when i begins strictly before j, the two overlap, and j ends strictly after i.

Equations

• Pancheva2003.OverlapsInto i j = (i.toProd.1 < j.toProd.1 ∧ j.toProd.1 ≤ i.toProd.2 ∧ i.toProd.2 < j.toProd.2)

theorem Pancheva2003.overlapsFromBefore_iff {T : Type u_2} [LinearOrder T] (i j : NonemptyInterval T) : OverlapsFromBefore i j ↔ i.Overlaps j ∧ ∃ t ∈ i, t ∉ j ∧ ∀ t' ∈ j, t < t'

The neutral relation is the paper's, the intervals overlapping and i having a point before every point of j.

theorem Pancheva2003.overlapsInto_iff {T : Type u_2} [LinearOrder T] (i j : NonemptyInterval T) : OverlapsInto i j ↔ i.Overlaps j ∧ ∃ (t : T) (t' : T), t ∈ i ∧ t ∉ j ∧ t' ∈ j ∧ t' ∉ i ∧ t < t'

The resultative relation is the paper's, the intervals overlapping, i having a point outside j, and j having a later point outside i.

The viewpoint aspects of (7b) and (17)

def Pancheva2003.BOUNDED {W : Type u_1} {T : Type u_2} {E : Type u_3} [LinearOrder T] [Event.TemporalTrace E T] (P : W → E → Prop) : W → Set (NonemptyInterval T)

The bounded aspect, (7b), holds where the run time of an event of the predicate is properly contained in the reference interval.

Equations

• Pancheva2003.BOUNDED P = Aspect.ofRel (fun (i j : NonemptyInterval T) => j < i) P

def Pancheva2003.NEUTRAL {W : Type u_1} {T : Type u_2} {E : Type u_3} [LinearOrder T] [Event.TemporalTrace E T] (P : W → E → Prop) : W → Set (NonemptyInterval T)

The neutral aspect, (7b), holds where the reference interval overlaps the run time of an event of the predicate and begins strictly before it.

Equations

• Pancheva2003.NEUTRAL P = Aspect.ofRel Pancheva2003.OverlapsFromBefore P

def Pancheva2003.RESULTATIVE {W : Type u_1} {T : Type u_2} {E : Type u_3} {S : Type u_4} [LinearOrder T] [Event.TemporalTrace S T] (P : W → S → E → Prop) : W → Set (NonemptyInterval T)

The resultative aspect, (17), holds of a predicate of result states and their events where the reference interval overlaps into the run time of the result state.

Equations

• Pancheva2003.RESULTATIVE P w = {i : NonemptyInterval T | ∃ (e : E) (s : S), Pancheva2003.OverlapsInto i (Event.τ s) ∧ P w s e}

theorem Pancheva2003.bounded_subset_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) : BOUNDED P w ⊆ Aspect.PRFV P w

The bounded aspect is the perfective with proper containment, footnote 8.

theorem Pancheva2003.neutral_subset_smith_neutral {W : Type u_1} {T : Type u_2} {E : Type u_3} [LinearOrder T] [Event.TemporalTrace E T] (P : W → E → Prop) (w : W) : NEUTRAL P w ⊆ Aspect.ViewpointType.neutral.denote P w

The paper's neutral entails Smith's neutral viewpoint, but not conversely, since the latter admits a reference interval that starts with the event.

What each perfect asserts at the reference interval

theorem Pancheva2003.universal_iff_unbounded {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.perfect (Aspect.UNBOUNDED P) w ↔ i ∈ Aspect.UNBOUNDED P w

The universal perfect, (11), asserts the eventuality throughout the reference interval, and conversely, since the unbounded aspect has the subinterval property.

theorem Pancheva2003.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} {i : NonemptyInterval T} (h : i ∈ Aspect.perfect (Aspect.UNBOUNDED P) w) : ∃ (e : E), P w e ∧ i.toProd.2 ∈ Event.τ e

The universal perfect holds at the right boundary of the reference interval, the time tense locates.

theorem Pancheva2003.neutral_experiential_begun_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} {i : NonemptyInterval T} (h : i ∈ Aspect.perfect (NEUTRAL P) w) : ∃ (e : E), P w e ∧ (Event.τ e).toProd.1 ≤ i.toProd.2

The neutral experiential, (12), places the beginning of the event time inside the span, so the eventuality has begun by the right boundary of the reference interval.

theorem Pancheva2003.bounded_experiential_ended_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} {i : NonemptyInterval T} (h : i ∈ Aspect.perfect (BOUNDED P) w) : ∃ (e : E), P w e ∧ (Event.τ e).toProd.2 ≤ i.toProd.2

The bounded experiential, (15), places the whole event time inside the span, so the eventuality has ended by the right boundary of the reference interval.

theorem Pancheva2003.resultative_state_at_rb {W : Type u_1} {T : Type u_2} {E : Type u_3} {S : Type u_4} [LinearOrder T] [Event.TemporalTrace S T] {Q : W → S → E → Prop} {w : W} {i : NonemptyInterval T} (h : i ∈ Aspect.perfect (RESULTATIVE Q) w) : ∃ (e : E) (s : S), Q w s e ∧ i.toProd.2 ∈ Event.τ s ∧ (Event.τ s).Overlaps i ∧ i.toProd.2 < (Event.τ s).toProd.2

The resultative perfect, (18), asserts the result state at the right boundary of the reference interval, overlapping the reference interval and continuing past it.

The perfects when the span may start early

Without a perfect-level adverbial the left boundary of the span is free, and when time has no first moment the experiential and resultative perfects reduce to conditions at the right boundary of the reference interval.

theorem Pancheva2003.neutral_experiential_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} [NoMinOrder T] : i ∈ Aspect.perfect (NEUTRAL P) w ↔ ∃ (e : E), P w e ∧ (Event.τ e).toProd.1 ≤ i.toProd.2

The neutral experiential asserts exactly that an eventuality has begun by the right boundary of the reference interval.

theorem Pancheva2003.bounded_experiential_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} [NoMinOrder T] : i ∈ Aspect.perfect (BOUNDED P) w ↔ ∃ (e : E), P w e ∧ (Event.τ e).toProd.2 ≤ i.toProd.2

The bounded experiential asserts exactly that an eventuality has ended by the right boundary of the reference interval.

theorem Pancheva2003.resultative_perfect_iff {W : Type u_1} {T : Type u_2} {E : Type u_3} {S : Type u_4} [LinearOrder T] [Event.TemporalTrace S T] {Q : W → S → E → Prop} {w : W} {i : NonemptyInterval T} [NoMinOrder T] : i ∈ Aspect.perfect (RESULTATIVE Q) w ↔ ∃ (e : E) (s : S), Q w s e ∧ (Event.τ s).toProd.1 ≤ i.toProd.2 ∧ i.toProd.2 < (Event.τ s).toProd.2

The resultative perfect asserts exactly that a result state holds at the right boundary of the reference interval and continues beyond it.

theorem Pancheva2003.bounded_perfect_iff_prfv_perfect {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} [NoMinOrder T] : i ∈ Aspect.perfect (BOUNDED P) w ↔ i ∈ Aspect.perfect (Aspect.PRFV P) w

The proper containment of footnote 8 makes no difference under the perfect, since the span may start earlier, so the bounded aspect and the perfective give the same perfect.

theorem Pancheva2003.neutral_experiential_of_universal {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} [NoMinOrder T] (h : i ∈ Aspect.perfect (Aspect.UNBOUNDED P) w) : i ∈ Aspect.perfect (NEUTRAL P) w

A universal perfect is also a neutral experiential one, so (13) is compatible with the eventuality holding at the utterance time and beyond.

theorem Pancheva2003.neutral_experiential_of_bounded {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} [NoMinOrder T] (h : i ∈ Aspect.perfect (BOUNDED P) w) : i ∈ Aspect.perfect (NEUTRAL P) w

The bounded experiential is the stronger of the two, (15b) over (12b).

(13) against (16)

theorem Pancheva2003.neutral_experiential_of_ongoing {W : Type u_1} {T : Type u_2} {E : Type u_3} [LinearOrder T] [Event.TemporalTrace E T] {w : W} {t : T} [NoMinOrder T] {e₀ : E} (h₁ : (Event.τ e₀).toProd.1 ≤ t) (h₂ : t < (Event.τ e₀).toProd.2) : NonemptyInterval.pure t ∈ Aspect.perfect (NEUTRAL fun (x : W) (e : E) => e = e₀) w ∧ t ∈ Event.τ e₀

The neutral experiential is true of an eventuality going on at the moment of reference, I have been sick lately, (13).

theorem Pancheva2003.neutral_experiential_of_over {W : Type u_1} {T : Type u_2} {E : Type u_3} [LinearOrder T] [Event.TemporalTrace E T] {w : W} {t : T} [NoMinOrder T] {e₀ : E} (h : (Event.τ e₀).toProd.2 < t) : NonemptyInterval.pure t ∈ Aspect.perfect (NEUTRAL fun (x : W) (e : E) => e = e₀) w ∧ t ∉ Event.τ e₀

The neutral experiential is also true of an eventuality over before the moment of reference, so it does not assert the eventuality there, (13).

theorem Pancheva2003.bounded_experiential_not_beyond_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} {i : NonemptyInterval T} (h : i ∈ Aspect.perfect (BOUNDED P) w) : ∃ (e : E), P w e ∧ ¬i.toProd.2 < (Event.τ e).toProd.2

The bounded experiential never lets the eventuality continue past the reference interval, I have been sick previously, (16).

theorem Pancheva2003.bounded_experiential_of_ends_at_rb {W : Type u_1} {T : Type u_2} {E : Type u_3} [LinearOrder T] [Event.TemporalTrace E T] {w : W} {t : T} [NoMinOrder T] {e₀ : E} (h : (Event.τ e₀).toProd.2 = t) : NonemptyInterval.pure t ∈ Aspect.perfect (BOUNDED fun (x : W) (e : E) => e = e₀) w ∧ t ∈ Event.τ e₀

Yet the bounded experiential is true of an eventuality whose last moment is the moment of reference, so on closed intervals (16) is compatible with the utterance time lying in the event time, against the paper's claim.

Consistency with Iatridou, Anagnostopoulou and Izvorski

theorem Pancheva2003.perf_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} {t : T} : (w, t) ∈ Aspect.PERF (Aspect.inclusive (Aspect.UNBOUNDED P)) ↔ ∃ (e : E), P w e ∧ (Event.τ e).toProd.1 ≤ t

The inclusive unbounded perfect of the older account holds exactly when an eventuality has begun by the time of tense.

theorem Pancheva2003.neutral_experiential_iff_inclusive_unbounded {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} [NoMinOrder T] : NonemptyInterval.pure t ∈ Aspect.perfect (NEUTRAL P) w ↔ (w, t) ∈ Aspect.PERF (Aspect.inclusive (Aspect.UNBOUNDED P))

At a moment of reference the neutral experiential is the older account's inclusive perfect of an unbounded eventuality.

theorem Pancheva2003.bounded_experiential_iff_inclusive_bounded {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} [NoMinOrder T] : NonemptyInterval.pure t ∈ Aspect.perfect (BOUNDED P) w ↔ (w, t) ∈ Aspect.PERF (Aspect.inclusive (Aspect.PRFV P))

At a moment of reference the bounded experiential is the older account's inclusive perfect of a bounded eventuality.

theorem Pancheva2003.universal_iff_durative_unbounded {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.perfect (Aspect.UNBOUNDED P) w ↔ (w, t) ∈ Aspect.PERF (Aspect.durative (Aspect.UNBOUNDED P))

At a moment of reference the universal perfect is the older account's durative perfect of an unbounded eventuality, with the covert adverbial.

Greek and Portuguese

theorem Pancheva2003.neutral_span_not_covered {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 : i ∈ Aspect.perfect (NEUTRAL P) w) : ∃ (pts : NonemptyInterval T), i.FinalSubinterval pts ∧ ∃ (e : E), P w e ∧ ¬pts ≤ Event.τ e

A perfect over the neutral aspect never has its span inside the run time of its eventuality, so a perfect that cannot embed the unbounded aspect, as in Greek, has no universal reading.

theorem Pancheva2003.bounded_span_not_covered {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 : i ∈ Aspect.perfect (BOUNDED P) w) : ∃ (pts : NonemptyInterval T), i.FinalSubinterval pts ∧ ∃ (e : E), P w e ∧ ¬pts ≤ Event.τ e

A perfect over the bounded aspect never has its span inside the run time of its eventuality.

theorem Pancheva2003.universal_not_ended_before_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} {i : NonemptyInterval T} (h : i ∈ Aspect.perfect (Aspect.UNBOUNDED P) w) : ∃ (e : E), P w e ∧ ¬(Event.τ e).toProd.2 < i.toProd.2

A perfect over the unbounded aspect, the only one the Portuguese perfect embeds, never places the eventuality wholly before the right boundary of the reference interval, so it has no experiential reading.