Instantiation of sorted properties

A property of eventualities is instantiated at a reference interval by the temporal relation its sort selects: the runtime of an event is included in the interval, the runtime of a state overlaps it ([kamp-rohrer-1983], [partee-1984], [KR93]), and a property of times applies to the interval. Reference intervals are Interval (WithTop T), so that an interval may run to the end of time and the null interval is ⊥. On a bounded interval the eventive clause is the perfective viewpoint PRFV of [klein-1994], and the imperfective IMPF entails the stative clause.

Main definitions

• Aspect.SortedProperty — a property of events, of states, or of times.
• Aspect.At — the instantiation relation AT(t, w, P).

Main results

• Aspect.At.mono — instantiation of an eventuality is monotone in the interval.
• Aspect.at_Ici_eventive_iff, Aspect.at_Ici_stative_iff — instantiation at a ray: the event starts no earlier, the state persists at or past.
• Aspect.at_eventive_withTop_iff_prfv — on a bounded interval, eventive instantiation is PRFV.

References

• [H. Kamp and C. Rohrer, Tense in Texts (1983)][kamp-rohrer-1983]
• [B. Partee, Nominal and Temporal Anaphora (1984)][partee-1984]
• H. Kamp and U. Reyle, From Discourse to Logic (1993)
• [W. Klein, Time in Language (1994)][klein-1994]

inductive Aspect.SortedProperty (W : Type u_3) (T : Type u_4) [LinearOrder T] : Type (max u_3 u_4)

A property sorted by what it is a property of: events, states, or times.

• eventive {W : Type u_3} {T : Type u_4} [LinearOrder T] (P : W → Event T → Prop) : SortedProperty W T
• stative {W : Type u_3} {T : Type u_4} [LinearOrder T] (P : W → Event T → Prop) : SortedProperty W T
• temporal {W : Type u_3} {T : Type u_4} [LinearOrder T] (P : W → Interval (WithTop T) → Prop) : SortedProperty W T

def Aspect.SortedProperty.IsEventuality {W : Type u_1} {T : Type u_2} [LinearOrder T] : SortedProperty W T → Prop

A property of eventualities rather than of times.

Equations

• (Aspect.SortedProperty.temporal P).IsEventuality = False
• x✝.IsEventuality = True

def Aspect.At {W : Type u_1} {T : Type u_2} [LinearOrder T] (t : Interval (WithTop T)) (w : W) : SortedProperty W T → Prop

At t w Q: the property Q is instantiated in w at the interval t, by inclusion of the runtime for events, overlap for states, and application for properties of times.

Equations

• Aspect.At t w (Aspect.SortedProperty.eventive P) = ∃ (e : Event T), P w e ∧ ↑e.τ.withTop ≤ t
• Aspect.At t w (Aspect.SortedProperty.stative P) = ∃ (e : Event T), P w e ∧ ¬Disjoint (↑e.τ.withTop) t
• Aspect.At t w (Aspect.SortedProperty.temporal P) = P w t

theorem Aspect.exists_mem_of_at {W : Type u_1} {T : Type u_2} [LinearOrder T] {Q : SortedProperty W T} {r : Interval (WithTop T)} {w : W} (hQ : Q.IsEventuality) (h : At r w Q) : ∃ (x : WithTop T), x ∈ r

An eventuality instantiated at an interval gives the interval a time.

theorem Aspect.not_at_bot {W : Type u_1} {T : Type u_2} [LinearOrder T] {Q : SortedProperty W T} {w : W} (hQ : Q.IsEventuality) : ¬At ⊥ w Q

Nothing is instantiated at the null interval but a property of times.

theorem Aspect.At.mono {W : Type u_1} {T : Type u_2} [LinearOrder T] {Q : SortedProperty W T} {r r' : Interval (WithTop T)} {w : W} (hQ : Q.IsEventuality) (h : r ≤ r') (hr : At r w Q) : At r' w Q

Instantiation of an eventuality is monotone in the interval.

@[simp]

theorem Aspect.at_Ici_eventive_iff {W : Type u_1} {T : Type u_2} [LinearOrder T] {P : W → Event T → Prop} {w : W} {t : T} : At (Interval.Ici t) w (SortedProperty.eventive P) ↔ ∃ (e : Event T), P w e ∧ t ≤ e.τ.toProd.1

An event is instantiated at the ray from t when it starts no earlier than t.

@[simp]

theorem Aspect.at_Ici_stative_iff {W : Type u_1} {T : Type u_2} [LinearOrder T] {P : W → Event T → Prop} {w : W} {t : T} : At (Interval.Ici t) w (SortedProperty.stative P) ↔ ∃ (e : Event T), P w e ∧ t ≤ e.τ.toProd.2

A state is instantiated at the ray from t when it persists at or past t.

theorem Aspect.at_eventive_withTop_iff_prfv {W : Type u_1} {T : Type u_2} [LinearOrder T] {P : W → Event T → Prop} {w : W} {i : NonemptyInterval T} : At (↑i.withTop) w (SortedProperty.eventive P) ↔ PRFV P w i

On a bounded interval, eventive instantiation is the perfective viewpoint.

theorem Aspect.at_stative_withTop_of_impf {W : Type u_1} {T : Type u_2} [LinearOrder T] {P : W → Event T → Prop} {w : W} {i : NonemptyInterval T} (h : IMPF P w i) : At (↑i.withTop) w (SortedProperty.stative P)

The imperfective viewpoint entails stative instantiation: proper inclusion of the interval in the runtime gives overlap.