Viewpoint aspect

This file defines viewpoint aspect, which in Smith's theory, following Klein, relates the topic time to the situation time. A relation between the reference time and the run time of an event gives an operator from event predicates to interval properties, at each world a set of reference intervals, and the operator of a viewpoint is that of its relation; the imperfective, perfective and prospective operators of Knick and Sharf are instances. The perfect takes an interval property to a set of world-time points through a perfect time span, which a perfect-level adverbial in the sense of Iatridou, Anagnostopoulou and Izvorski restricts. An interval adverbial is read durative, the predicate holding at every subinterval of its interval, or inclusive, at some subinterval, as Dowty, Mittwoch and Vlach distinguish them.

Main definitions

• Aspect.ofRel: the operator of a relation between reference time and run time.
• Aspect.IMPF: the imperfective.
• Aspect.PRFV: the perfective.
• Aspect.UNBOUNDED: Pancheva's non-strict imperfective.
• Aspect.perfect: the perfect as an operator on interval properties, whose reference interval is a final subinterval of the perfect time span; Aspect.PERF is its value at a point.
• Aspect.durative, Aspect.inclusive: the durative and inclusive readings of an interval adverbial.

Main results

• Aspect.prfv_eq_upperClosure: the perfective holds on the upper closure of the predicate's run times.
• Aspect.unbounded_eq_lowerClosure: the non-strict imperfective holds on their lower closure.
• Aspect.inclusive_eq_upperClosure: the inclusive reading is the upper closure.

Implementation notes

• Of Klein's relations, TT INCL TSit is the imperfective, TT AT TSit the perfective, TT AFTER TSit the perfect and TT BEFORE TSit the prospective. Smith's neutral viewpoint includes the initial point of the situation and at least one internal stage.
• The operators follow Knick and Sharf's equations, with a boundary a time point where the paper has a final or initial subinterval. The predicate applies to the outer reference time, which beneath the perfect is the perfect time span.
• A perfect-level adverbial is a set of spans, which the perfect intersects with the interval property, PERF (adv ∩ p ·): since t₀ admits the spans starting at t₀, Knick and Sharf's domain restriction tᵣ the spans starting in tᵣ, and the covert adverbial of an unmodified perfect every span.
• Event predicates range over any event domain with a temporal trace (Event.TemporalTrace).
• An interval property is a family of sets of intervals indexed by worlds, W → Set (NonemptyInterval T), so that mathlib's order closures and lower and upper sets apply to it directly; the perfect yields a set of world-time points.

References

• [Smi97]
• [Kle94]
• [KS26]
• [Pan03]
• [IAI01]
• [Dow79]
• [Mit88]
• [Vla93]

def Aspect.ViewpointType.ttTSitRelation {T : Type u_1} [LinearOrder T] (v : ViewpointType) (tt tsit : NonemptyInterval T) : Prop

v.ttTSitRelation tt tsit is the relation the viewpoint v imposes between the topic time and the situation time, which is inclusion in the situation, containment of the situation, posteriority, anteriority, and, for the neutral viewpoint, containment of the situation's start.

Equations

• Aspect.ViewpointType.imperfective.ttTSitRelation tt tsit = (tt < tsit)
• Aspect.ViewpointType.perfective.ttTSitRelation tt tsit = (tsit ≤ tt)
• Aspect.ViewpointType.perfect.ttTSitRelation tt tsit = tsit.IsBefore tt
• Aspect.ViewpointType.prospective.ttTSitRelation tt tsit = tt.IsBefore tsit
• Aspect.ViewpointType.neutral.ttTSitRelation tt tsit = (tsit.toProd.1 ∈ tt)

@[instance_reducible]

instance Aspect.instDecidableTtTSitRelation {T : Type u_1} [LinearOrder T] (v : ViewpointType) (tt tsit : NonemptyInterval T) : Decidable (v.ttTSitRelation tt tsit)

Equations

• One or more equations did not get rendered due to their size.

Operators

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

The aspect operator of a relation R gives, at each world, the reference intervals that stand in R to the run time of some event of the predicate.

Equations

• Aspect.ofRel R P w = {t : NonemptyInterval T | ∃ (e : E), R t (Event.τ e) ∧ P w e}

@[simp]

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

theorem Aspect.ofRel_mono {T : Type u_1} [LinearOrder T] {W : Type u_2} {E : Type u_3} [Event.TemporalTrace E T] {R S : NonemptyInterval T → NonemptyInterval T → Prop} (h : ∀ (t s : NonemptyInterval T), R t s → S t s) (P : W → E → Prop) (w : W) : ofRel R P w ⊆ ofRel S P w

The operator is monotone in the relation.

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

The operator of a viewpoint is the operator of its relation between the topic time and the situation time.

Equations

• v.denote P = Aspect.ofRel v.ttTSitRelation P

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

The imperfective, (25), holds where the reference time is properly contained in the run time of an event of the predicate.

Equations

• Aspect.IMPF P = Aspect.ViewpointType.imperfective.denote P

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

The perfective, (28), holds where the run time of an event of the predicate is contained in the reference time.

Equations

• Aspect.PRFV P = Aspect.ViewpointType.perfective.denote P

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

The prospective holds where the reference time precedes an event of the predicate.

Equations

• Aspect.PROSP P = Aspect.ViewpointType.prospective.denote P

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

The non-strict imperfective, (7b) of [Pan03], holds where the reference time is contained, not necessarily properly, in the run time of an event of the predicate.

Equations

• Aspect.UNBOUNDED P = Aspect.ofRel (fun (x1 x2 : NonemptyInterval T) => x1 ≤ x2) P

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

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

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

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

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

theorem Aspect.unbounded_eq_lowerClosure {T : Type u_1} [LinearOrder T] {W : Type u_2} {E : Type u_3} [Event.TemporalTrace E T] {P : W → E → Prop} {w : W} : UNBOUNDED P w = ↑(lowerClosure (Event.τ '' {e : E | P w e}))

The non-strict imperfective holds on the lower closure of the predicate's run times.

theorem Aspect.prfv_eq_upperClosure {T : Type u_1} [LinearOrder T] {W : Type u_2} {E : Type u_3} [Event.TemporalTrace E T] {P : W → E → Prop} {w : W} : PRFV P w = ↑(upperClosure (Event.τ '' {e : E | P w e}))

The perfective holds on the upper closure of the predicate's run times.

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

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

def Aspect.PERF {T : Type u_1} [LinearOrder T] {W : Type u_2} (p : W → Set (NonemptyInterval T)) : Set (Reference.Index W T)

The perfect, (22b), holds at the world-time points whose time is the right boundary, (22a), of some perfect time span belonging to the interval property.

Equations

• Aspect.PERF p = {s : Reference.Index W T | ∃ pts ∈ p s.world, pts.toProd.2 = s.time}

@[simp]

theorem Aspect.mem_perf {T : Type u_1} [LinearOrder T] {W : Type u_2} {w : W} {p : W → Set (NonemptyInterval T)} {t : T} : (w, t) ∈ PERF p ↔ ∃ pts ∈ p w, pts.toProd.2 = t

theorem Aspect.perf_mono {T : Type u_1} [LinearOrder T] {W : Type u_2} {p q : W → Set (NonemptyInterval T)} (h : ∀ (w : W), p w ⊆ q w) : PERF p ⊆ PERF q

def Aspect.atPoint {T : Type u_1} [LinearOrder T] {W : Type u_2} (p : W → Set (NonemptyInterval T)) : Set (Reference.Index W T)

atPoint p holds at the world-time points whose degenerate interval belongs to p, as the non-perfect forms are evaluated.

Equations

• Aspect.atPoint p = {s : Reference.Index W T | NonemptyInterval.pure s.time ∈ p s.world}

def Aspect.perfect {T : Type u_1} [LinearOrder T] {W : Type u_2} (p : W → Set (NonemptyInterval T)) : W → Set (NonemptyInterval T)

perfect p holds at a reference interval that is a final subinterval of some perfect time span belonging to p, the perfect as an operator on interval properties.

Equations

• Aspect.perfect p w = {i : NonemptyInterval T | ∃ pts ∈ p w, i.FinalSubinterval pts}

theorem Aspect.perf_eq_atPoint_perfect {T : Type u_1} [LinearOrder T] {W : Type u_2} (p : W → Set (NonemptyInterval T)) : PERF p = atPoint (perfect p)

The perfect at a point is the perfect at the degenerate reference interval of that point.

theorem Aspect.perfect_mono {T : Type u_1} [LinearOrder T] {W : Type u_2} {p q : W → Set (NonemptyInterval T)} (h : ∀ (w : W), p w ⊆ q w) (w : W) : perfect p w ⊆ perfect q w

Durative and inclusive readings

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

durative p holds at a span when p holds at every subinterval of it, the durative reading of an interval adverbial, throughout.

Equations

• Aspect.durative p w = {i : NonemptyInterval T | Set.Iic i ⊆ p w}

def Aspect.inclusive {T : Type u_1} [LinearOrder T] {W : Type u_2} (p : W → Set (NonemptyInterval T)) : W → Set (NonemptyInterval T)

inclusive p holds at a span when p holds at some subinterval of it, the inclusive reading of an interval adverbial, in.

Equations

• Aspect.inclusive p w = {i : NonemptyInterval T | ∃ j ∈ p w, j ≤ i}

theorem Aspect.inclusive_eq_upperClosure {T : Type u_1} [LinearOrder T] {W : Type u_2} {w : W} {p : W → Set (NonemptyInterval T)} : inclusive p w = ↑(upperClosure (p w))

The inclusive reading is the upper closure of the interval property.

theorem Aspect.inclusive_eq_of_isUpperSet {T : Type u_1} [LinearOrder T] {W : Type u_2} {w : W} {p : W → Set (NonemptyInterval T)} (hp : IsUpperSet (p w)) : inclusive p w = p w

On an upper set the inclusive reading is the set itself.

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