The AT Relation

@cite{condoravdi-2002}

Temporal instantiation of eventuality predicates, dispatching on eventuality sort. Events require temporal inclusion (τ(e) ⊆ t); states require temporal overlap (τ(e) ∘ t). This distinction, due to @cite{kamp-rohrer-1983} and @cite{partee-1984}, is the bridge between eventuality classification and temporal operators (tense, aspect, modals).

Key Definitions

• atEvent / atState: sort-specific instantiation at an interval
• at': unified dispatch on Dynamicity
• atEventForward / atStateForward / atForward: instantiation in the future of a point — @cite{condoravdi-2002}'s [t,_) expansion

Bridge to Klein's Aspect Operators

• prfv_iff_atEvent: PRFV and atEvent are definitionally equal
• impf_implies_atState: IMPF (proper inclusion) implies atState (overlap)

AT at an Interval

def Semantics.Tense.Modal.AtOperator.atEvent {W : Type u_1} {Time : Type u_2} [LinearOrder Time] (P : Events.EventPred W Time) (w : W) (t : Core.Time.Interval Time) : Prop

Temporal instantiation of an eventive predicate at interval t: ∃e[P(w)(e) ∧ τ(e) ⊆ t]. Events must be fully contained in the reference interval.

Equations

• Semantics.Tense.Modal.AtOperator.atEvent P w t = ∃ (e : Semantics.Events.Event Time), P w e ∧ e.runtime.subinterval t

def Semantics.Tense.Modal.AtOperator.atState {W : Type u_1} {Time : Type u_2} [LinearOrder Time] (P : Events.EventPred W Time) (w : W) (t : Core.Time.Interval Time) : Prop

Temporal instantiation of a stative predicate at interval t: ∃e[P(w)(e) ∧ τ(e) ∘ t]. States need only overlap the reference interval.

Equations

• Semantics.Tense.Modal.AtOperator.atState P w t = ∃ (e : Semantics.Events.Event Time), P w e ∧ e.runtime.overlaps t

def Semantics.Tense.Modal.AtOperator.at' {W : Type u_1} {Time : Type u_2} [LinearOrder Time] (sort : Features.Dynamicity) (P : Events.EventPred W Time) (w : W) (t : Core.Time.Interval Time) : Prop

@cite{condoravdi-2002} [19]: unified AT relation dispatching on eventuality sort.

at' .dynamic P w t = atEvent P w t (event ⊆ interval) at' .stative P w t = atState P w t (state ∘ interval)

Equations

• Semantics.Tense.Modal.AtOperator.at' Features.Dynamicity.dynamic P w t = Semantics.Tense.Modal.AtOperator.atEvent P w t
• Semantics.Tense.Modal.AtOperator.at' Features.Dynamicity.stative P w t = Semantics.Tense.Modal.AtOperator.atState P w t

@[simp]

theorem Semantics.Tense.Modal.AtOperator.at'_dynamic {W : Type u_1} {Time : Type u_2} [LinearOrder Time] (P : Events.EventPred W Time) (w : W) (t : Core.Time.Interval Time) : at' Features.Dynamicity.dynamic P w t = atEvent P w t

@[simp]

theorem Semantics.Tense.Modal.AtOperator.at'_stative {W : Type u_1} {Time : Type u_2} [LinearOrder Time] (P : Events.EventPred W Time) (w : W) (t : Core.Time.Interval Time) : at' Features.Dynamicity.stative P w t = atState P w t

theorem Semantics.Tense.Modal.AtOperator.atState_of_atEvent {W : Type u_1} {Time : Type u_2} [LinearOrder Time] (P : Events.EventPred W Time) (w : W) (t : Core.Time.Interval Time) (h : atEvent P w t) : atState P w t

Eventive instantiation is stronger than stative: if the event is contained in the interval, it certainly overlaps it.

AT with Forward Expansion

@cite{condoravdi-2002} [22]–[23]: modals expand the evaluation time forward to [t, _) — the interval from t to the end of time. Since Interval requires finite bounds, we express the constraints directly: for events, the event starts at or after t; for states, the state persists at or past t.

def Semantics.Tense.Modal.AtOperator.atEventForward {W : Type u_1} {Time : Type u_2} [LinearOrder Time] (P : Events.EventPred W Time) (w : W) (t : Time) : Prop

Event instantiated in the future of t: the event starts at or after t. Corresponds to AT([t,_), w, P) for eventive P.

Equations

• Semantics.Tense.Modal.AtOperator.atEventForward P w t = ∃ (e : Semantics.Events.Event Time), P w e ∧ t ≤ e.runtime.start

def Semantics.Tense.Modal.AtOperator.atStateForward {W : Type u_1} {Time : Type u_2} [LinearOrder Time] (P : Events.EventPred W Time) (w : W) (t : Time) : Prop

State instantiated through t: the state persists at or past t. Corresponds to AT([t,_), w, P) for stative P.

Equations

• Semantics.Tense.Modal.AtOperator.atStateForward P w t = ∃ (e : Semantics.Events.Event Time), P w e ∧ t ≤ e.runtime.finish

def Semantics.Tense.Modal.AtOperator.atForward {W : Type u_1} {Time : Type u_2} [LinearOrder Time] (sort : Features.Dynamicity) (P : Events.EventPred W Time) (w : W) (t : Time) : Prop

Forward AT, dispatching on sort.

Equations

• Semantics.Tense.Modal.AtOperator.atForward Features.Dynamicity.dynamic P w t = Semantics.Tense.Modal.AtOperator.atEventForward P w t
• Semantics.Tense.Modal.AtOperator.atForward Features.Dynamicity.stative P w t = Semantics.Tense.Modal.AtOperator.atStateForward P w t

@[simp]

theorem Semantics.Tense.Modal.AtOperator.atForward_dynamic {W : Type u_1} {Time : Type u_2} [LinearOrder Time] (P : Events.EventPred W Time) (w : W) (t : Time) : atForward Features.Dynamicity.dynamic P w t = atEventForward P w t

@[simp]

theorem Semantics.Tense.Modal.AtOperator.atForward_stative {W : Type u_1} {Time : Type u_2} [LinearOrder Time] (P : Events.EventPred W Time) (w : W) (t : Time) : atForward Features.Dynamicity.stative P w t = atStateForward P w t

theorem Semantics.Tense.Modal.AtOperator.atStateForward_of_atEventForward {W : Type u_1} {Time : Type u_2} [LinearOrder Time] (P : Events.EventPred W Time) (w : W) (t : Time) (h : atEventForward P w t) : atStateForward P w t

Forward stative is weaker than forward eventive: if the event starts at or after t, its finish is also at or after t.

Bridge to Klein's Aspect Operators

theorem Semantics.Tense.Modal.AtOperator.prfv_iff_atEvent {W : Type u_1} {Time : Type u_2} [LinearOrder Time] (P : Events.EventPred W Time) (w : W) (t : Core.Time.Interval Time) : Aspect.Core.PRFV P w t ↔ atEvent P w t

PRFV and atEvent check the same condition (conjunction is commuted).

theorem Semantics.Tense.Modal.AtOperator.impf_implies_atState {W : Type u_1} {Time : Type u_2} [LinearOrder Time] (P : Events.EventPred W Time) (w : W) (t : Core.Time.Interval Time) (h : Aspect.Core.IMPF P w t) : atState P w t

IMPF implies atState: if the reference interval is properly contained in the event runtime (IMPF), then the event runtime certainly overlaps the reference interval.

Monotonicity

theorem Semantics.Tense.Modal.AtOperator.atEvent_mono {W : Type u_1} {Time : Type u_2} [LinearOrder Time] {t₁ t₂ : Core.Time.Interval Time} (P : Events.EventPred W Time) (w : W) (hSub : t₁.subinterval t₂) (h : atEvent P w t₁) : atEvent P w t₂

atEvent is monotone in the reference interval: if a larger interval contains the smaller, eventive instantiation at the smaller implies instantiation at the larger.

theorem Semantics.Tense.Modal.AtOperator.atEventForward_of_atEvent_point {W : Type u_1} {Time : Type u_2} [LinearOrder Time] (P : Events.EventPred W Time) (w : W) (t : Time) (h : atEvent P w (Core.Time.Interval.point t)) : atEventForward P w t

atEvent at a point [t,t] implies atEventForward at t: if an event is instantiated at time t, it starts at or after t.

theorem Semantics.Tense.Modal.AtOperator.atStateForward_of_atState_point {W : Type u_1} {Time : Type u_2} [LinearOrder Time] (P : Events.EventPred W Time) (w : W) (t : Time) (h : atState P w (Core.Time.Interval.point t)) : atStateForward P w t

atState at a point [t,t] implies atStateForward at t: if a state overlaps time t, it persists at or past t.