The subinterval property

This file defines the subinterval property of Bennett and Partee and of Dowty. A predicate of events has it when every subinterval of the run time of an event it holds of is the run time of an event it holds of, which is to say that its run times form a lower set. States and activities have the property: if John slept from one to three, he slept from one to two. Accomplishments and achievements lack it, since no proper part of the building of a house is the building of a house. The property draws only this line, and does not separate states from activities or accomplishments from achievements.

For a predicate with the property the imperfective entails the perfective at the same reference time, Mary was running entailing Mary ran: the reference time lies inside the run time of a running, so it is itself the run time of a running. The entailment does not characterize the property, since a predicate may validate it without being closed under subintervals.

Dowty states the property of sentences true at intervals. For an interval property, a set of intervals at each world, it says that the set is a lower set, mathlib's IsLowerSet, so it needs no name of its own. The non-strict and the strict imperfective have it whatever the predicate, and so does the negated perfective, the complement of an upper set: an interval containing no event of the predicate has no subinterval containing one. A durative claim, the predicate at every subinterval of a span, has it too, and for a lower set the durative claim and the perfect are the set itself.

Main definitions

• Aspect.HasSubintervalProperty: the run times of the predicate form a lower set at every world.

Main results

• Aspect.hasSubintervalProperty_iff_witnesses: every subinterval of the run time of an event of the predicate is the run time of an event of the predicate.
• Aspect.HasSubintervalProperty.impf_subset_prfv: the imperfective entails the perfective.
• Aspect.not_hasSubintervalProperty_snd_eq: the predicate of events that end when a durative event ends lacks the property.
• Aspect.exists_prfv_of_impf_not_hasSubintervalProperty: a predicate may validate the entailment and lack the property.
• Aspect.isLowerSet_impf, Aspect.isLowerSet_compl_prfv: the imperfective and the negated perfective have the property as interval properties, as the non-strict imperfective does (Aspect.isLowerSet_unbounded).
• Aspect.durative_eq_of_isLowerSet, Aspect.perfect_eq_of_isLowerSet: for an interval property with the property, the durative claim and the perfect are the property itself.

Implementation notes

The property is divisive reference, Mereology.DIV, of the predicate's run times, so it is stated on mathlib's IsLowerSet. The viewpoint operators quantify over events of the world of evaluation, so the entailment is the extensional one. The imperfective paradox proper, on which John was building a house is true though no house is ever built, needs a modal progressive and is not modelled.

References

• [BP72]
• [Dow79]

def Aspect.HasSubintervalProperty {W : Type u_1} {T : Type u_2} {E : Type u_3} [LinearOrder T] [Event.TemporalTrace E T] (P : W → E → Prop) : Prop

A predicate of events has the subinterval property when its run times form a lower set at every world.

Equations

• Aspect.HasSubintervalProperty P = ∀ (w : W), IsLowerSet (Event.τ '' {e : E | P w e})

theorem Aspect.hasSubintervalProperty_iff_witnesses {W : Type u_1} {T : Type u_2} {E : Type u_3} [LinearOrder T] [Event.TemporalTrace E T] {P : W → E → Prop} : HasSubintervalProperty P ↔ ∀ (e : E) (w : W), P w e → ∀ t ≤ Event.τ e, ∃ (e' : E), Event.τ e' = t ∧ P w e'

A predicate has the subinterval property exactly when every subinterval of the run time of one of its events is the run time of one of its events.

theorem Aspect.HasSubintervalProperty.mem_image_of_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 : NonemptyInterval T} (h : HasSubintervalProperty P) (ht : t ∈ UNBOUNDED P w) : t ∈ Event.τ '' {e : E | P w e}

Under the subinterval property an interval inside the run time of an event of the predicate is a run time of the predicate.

theorem Aspect.HasSubintervalProperty.unbounded_subset_prfv {W : Type u_1} {T : Type u_2} {E : Type u_3} [LinearOrder T] [Event.TemporalTrace E T] {P : W → E → Prop} (h : HasSubintervalProperty P) (w : W) : UNBOUNDED P w ⊆ PRFV P w

Under the subinterval property the non-strict imperfective entails the perfective.

theorem Aspect.HasSubintervalProperty.impf_subset_prfv {W : Type u_1} {T : Type u_2} {E : Type u_3} [LinearOrder T] [Event.TemporalTrace E T] {P : W → E → Prop} (h : HasSubintervalProperty P) (w : W) : IMPF P w ⊆ PRFV P w

Under the subinterval property the imperfective entails the perfective.

theorem Aspect.not_hasSubintervalProperty_snd_eq {W : Type u_1} {T : Type u_2} {E : Type u_3} [LinearOrder T] [Event.TemporalTrace E T] [Nonempty W] {e : E} (he : (Event.τ e).toProd.1 < (Event.τ e).toProd.2) : ¬HasSubintervalProperty fun (x : W) (e' : E) => (Event.τ e').toProd.2 = (Event.τ e).toProd.2

The predicate of events that end when a durative event ends lacks the subinterval property, as the building of a house holds of no proper part that lacks the result.

theorem Aspect.exists_prfv_of_impf_not_hasSubintervalProperty : ∃ (P : Unit → NonemptyInterval ℤ → Prop), (∀ (w : Unit), IMPF P w ⊆ PRFV P w) ∧ ¬HasSubintervalProperty P

The entailment from the imperfective to the perfective does not characterize the subinterval property. The predicate of events that are instantaneous or run from 0 to 2 validates it, every reference time containing an instant, and the interval from 0 to 1 is a subinterval of one of its run times without being one.

Interval properties

theorem Aspect.isLowerSet_impf {W : Type u_1} {T : Type u_2} {E : Type u_3} [LinearOrder T] [Event.TemporalTrace E T] (P : W → E → Prop) (w : W) : IsLowerSet (IMPF P w)

The imperfective has the subinterval property whatever the predicate.

theorem Aspect.isLowerSet_compl_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) : IsLowerSet (PRFV P w)ᶜ

Negation yields the subinterval property, since an interval containing no event of the predicate has no subinterval containing one.

theorem Aspect.isLowerSet_durative {W : Type u_1} {T : Type u_2} [LinearOrder T] (w : W) (p : W → Set (NonemptyInterval T)) : IsLowerSet (durative p w)

A durative claim has the subinterval property whatever the interval property.

theorem Aspect.durative_eq_of_isLowerSet {W : Type u_1} {T : Type u_2} [LinearOrder T] {w : W} {p : W → Set (NonemptyInterval T)} (hp : IsLowerSet (p w)) : durative p w = p w

For an interval property with the subinterval property, the durative claim is the property itself.

theorem Aspect.perfect_eq_of_isLowerSet {W : Type u_1} {T : Type u_2} [LinearOrder T] {w : W} {p : W → Set (NonemptyInterval T)} (hp : IsLowerSet (p w)) : perfect p w = p w

For an interval property with the subinterval property, the perfect is the property itself.